:: Formalization of Integral Linear Space
::  by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received August 17, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies REAL_1, SUBSET_1, NUMBERS, RLVECT_1, RLSUB_1, FINSET_1, RLVECT_2,
      FINSEQ_1, STRUCT_0, FUNCT_1, XBOOLE_0, VALUED_1, ORDINAL4, ARYTM_3,
      RELAT_1, PARTFUN1, NAT_1, INT_1, CARD_3, CARD_1, SUPINF_2, TARSKI,
      FUNCT_2, ARYTM_1, RLVECT_3, RLVECT_X, XXREAL_0, VALUED_0, FUNCT_4,
      FUNCOP_1, FINSEQ_2;
 notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
      FUNCT_2, DOMAIN_1, FUNCOP_1, FUNCT_4, FINSET_1, CARD_1, NUMBERS,
      XXREAL_0, REAL_1, ORDINAL1, INT_1, VALUED_0, BINOP_2, FINSEQ_1, SEQ_1,
      FINSEQ_2, STRUCT_0, RLVECT_1, RLSUB_1, RLVECT_2, RLVECT_3, RUSUB_4,
      VFUNCT_1, BINOM;
 constructors REALSET1, RLVECT_2, RLVECT_3, FUNCT_4, RUSUB_4, BINOP_2, SEQ_1,
      FUNCSDOM, TOPREALB, VFUNCT_1, BINOM;
 registrations XBOOLE_0, FUNCT_1, RELSET_1, FINSET_1, NUMBERS, STRUCT_0,
      ORDINAL1, INT_1, XREAL_0, RLVECT_2, VALUED_0, FINSEQ_1, FINSEQ_2, CARD_1;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
 definitions RLVECT_2, TARSKI, RUSUB_4, FINSEQ_1;
 theorems FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, RLSUB_1,
      RLVECT_1, RLVECT_2, TARSKI, ZFMISC_1, RELAT_1, XBOOLE_0, XBOOLE_1,
      STRUCT_0, PARTFUN1, RLVECT_3, INT_1, NUMBERS, NAT_1, XREAL_0, XXREAL_0,
      ENUMSET1, RLVECT_4, VFUNCT_1, BINOM, FUNCOP_1, FINSEQ_5, FUNCT_4, CARD_1;
 schemes FINSEQ_1, NAT_1, FUNCT_2, RLVECT_4;

begin :: 1. Preliminaries

 reconsider z0=0 as Real;
 deffunc H(set)=0;

theorem
  for X be RealLinearSpace,
      R1, R2 be FinSequence of X
    st len R1 = len R2 holds Sum(R1+R2) = Sum(R1) + Sum(R2)
proof
  let X be RealLinearSpace,
      R1, R2 be FinSequence of X;
  assume len R1 = len R2; then
  dom R1 = dom R2 by FINSEQ_3:29;
  hence thesis by BINOM:7;
end;

theorem
  for X be RealLinearSpace,
      R1, R2, R3 be FinSequence of X
    st len R1 = len R2 & R3 = R1-R2 holds Sum(R3) = Sum(R1) - Sum(R2)
proof
  let X be RealLinearSpace,
      R1, R2, R3 be FinSequence of X;
  assume A1: len R1 = len R2 & R3 = R1 - R2; then
A2: dom R1 = dom R2 by FINSEQ_3:29;
A3: dom R3 = dom R1 /\ dom R2 by A1,VFUNCT_1:def 2
          .= dom R1 by A2; then
A4: len R3 = len R1 by FINSEQ_3:29;
  for k be Element of NAT st k in dom R1 holds R3.k = R1/.k - R2/.k
  proof
    let k be Element of NAT;
    assume A5: k in dom R1;
    hence R3.k = R3/.k by A3,PARTFUN1:def 6
             .= R1/.k - R2/.k by A1,A5,A3,VFUNCT_1:def 2;
  end;
  hence thesis by A1,A4,RLVECT_2:5;
end;

theorem Th3:
  for X be RealLinearSpace,
      R1, R2 be FinSequence of X,
      a be Element of REAL st R2 = a(#)R1 holds Sum(R2) = a * Sum(R1)
proof
  let X be RealLinearSpace,
      R1, R2 be FinSequence of X,
      a be Element of REAL;
  assume A1: R2 = a(#)R1;
  dom R2 = dom R1 by A1,VFUNCT_1:def 4; then
A2: len R2 = len R1 by FINSEQ_3:29;
  for k be Element of NAT st k in dom R1 holds R2.k = a * R1/.k
  proof
    let k be Element of NAT;
    assume k in dom R1; then
A3: k in dom R2 by A1,VFUNCT_1:def 4;
    hence R2.k = R2/.k by PARTFUN1:def 6
             .= a * R1/.k by A3,A1,VFUNCT_1:def 4;
  end;
  hence thesis by A2,RLVECT_2:3;
end;

begin :: 2. Integral Linear Space

reserve x,y for set;
reserve a,b for Real;
reserve i,j for Integer;
reserve V for RealLinearSpace;
reserve W1,W2,W3 for Subspace of V;
reserve v,v1,v2,v3,u,w,w1,w2,w3 for VECTOR of V;
reserve A,B,C for Subset of V;
reserve L,L1,L2 for Linear_Combination of V;
reserve l,l1,l2 for Linear_Combination of A;

definition let V,i,L;
  func i * L -> Linear_Combination of V means  :Def1:
  for v holds it.v = i * L.v;
  existence
  proof
    deffunc F(Element of V)=i * L.$1;
    consider f being Function of the carrier of V, REAL such that
A1: for v being Element of V holds f.v = F(v) from FUNCT_2:sch 4;
    reconsider f as Element of Funcs(the carrier of V,REAL) by FUNCT_2:8;
    now
      let v be Element of V;
      assume not v in Carrier(L);
      then L.v = 0;
      hence f.v = i * 0 by A1
        .= 0;
    end;
    then reconsider f as Linear_Combination of V by RLVECT_2:def 3;
    take f;
    let v;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let L1,L2;
    assume that
A2: for v holds L1.v = i * L.v and
A3: for v holds L2.v = i * L.v;
    let v;
    thus L1.v = i * L.v by A2
      .= L2.v by A3;
  end;
end;

definition let V,A;
  func Z_Lin(A) -> Subset of V equals
  {Sum(l) : rng l c= INT};
  correctness
  proof
    set A1 = {Sum(l) : rng l c= INT};
    A1 c= the carrier of V
    proof
      let x;
      assume x in A1;
      then ex l st x = Sum(l) & rng l c= INT;
      hence thesis;
    end;
    hence thesis;
  end;
end;

theorem Th4:
  a = i implies a*l = i*l
proof
  assume A1:a=i;
  for v be VECTOR of V holds (i*l).v = a * l.v by A1,Def1;
  hence thesis by RLVECT_2:def 11;
end;

theorem Th5:
  rng l1 c= INT & rng l2 c= INT implies rng (l1+l2) c= INT
proof
  assume A1: rng l1 c= INT & rng l2 c= INT;
    let y be set;
    assume A2:y in rng (l1+l2);
    consider x be set such that
A3: x in the carrier of V & y=(l1+l2).x by A2,FUNCT_2:11;
    reconsider z=x as VECTOR of V by A3;
    l1.z in rng l1 by FUNCT_2:4; then
    reconsider z1=l1.z as Integer by A1;
    l2.z in rng l2 by FUNCT_2:4; then
    reconsider z2=l2.z as Integer by A1;
    (l1+l2).z = z1+ z2 by RLVECT_2:def 10;
    hence y in INT by A3;
end;

theorem Th6:
  rng l c= INT implies rng (i*l) c= INT
proof
  assume A1:rng l c= INT;
    let y be set;
    assume A2:y in rng (i*l);
    consider x be set such that
A3: x in the carrier of V & y=(i*l).x by A2,FUNCT_2:11;
    reconsider z=x as VECTOR of V by A3;
    reconsider ii=i as Real by XREAL_0:def 1;
    l.z in rng l by FUNCT_2:4; then
    reconsider z1=l.z as Integer by A1;
    (i*l).z = (ii*l).z by Th4
           .= i*z1 by RLVECT_2:def 11;
    hence y in INT by A3;
end;

theorem Th7:
  rng (ZeroLC(V)) c= INT
  proof
    let y be set;
    assume A1:y in rng (ZeroLC(V));
    consider x be set such that
A2: x in the carrier of V & y=(ZeroLC(V)).x by A1,FUNCT_2:11;
    reconsider z = x as VECTOR of V by A2;
    ZeroLC(V).z = 0 by RLVECT_2:20;
    hence y in INT by A2,NUMBERS:17,TARSKI:def 3;
  end;

theorem Th8:
  Z_Lin(A) c= the carrier of Lin(A)
proof
    let x be set;
    assume x in Z_Lin(A); then
    consider l1 being Linear_Combination of A such that
A1: x = Sum(l1) & rng l1 c= INT;
    x in Lin(A) by A1,RLVECT_3:14;
    hence thesis by STRUCT_0:def 5;
end;

theorem Th9:
  v in Z_Lin(A) & u in Z_Lin(A) implies v + u in Z_Lin(A)
  proof
    assume that
A1: v in Z_Lin(A) and
A2: u in Z_Lin(A);
    consider l1 being Linear_Combination of A such that
A3: v = Sum(l1) & rng l1 c= INT by A1;
    consider l2 being Linear_Combination of A such that
A4: u = Sum(l2) & rng l2 c= INT by A2;
    reconsider f = l1 + l2 as Linear_Combination of A by RLVECT_2:38;
A5: rng f c= INT by A3,A4,Th5;
    v + u = Sum(f) by A3,A4,RLVECT_3:1;
    hence thesis by A5;
  end;

theorem Th10:
  v in Z_Lin(A) implies i*v in Z_Lin(A)
  proof
    assume v in Z_Lin(A);
    then consider l such that
A1: v = Sum(l) & rng l c= INT;
    reconsider a=i as Real by XREAL_0:def 1;
A2: a*l=i*l by Th4; then
    reconsider f = i * l as Linear_Combination of A by RLVECT_2:44;
A3: i * v = Sum(f) by A1,A2,RLVECT_3:2;
    rng (i * l) c= INT by Th6,A1;
    hence thesis by A3;
  end;

theorem Th11:
  0.V in Z_Lin(A)
proof
  reconsider l = ZeroLC(V) as Linear_Combination of A by RLVECT_2:22;
A1: Sum(l) = 0.V by RLVECT_2:30;
  rng l c= INT by Th7;
  hence thesis by A1;
end;

theorem Th12:
  x in A implies x in Z_Lin(A)
proof
  assume
A1: x in A;
  then reconsider v = x as VECTOR of V;
  consider f being Function of the carrier of V, REAL such that
A2: f.v = 1 and
A3: for u st u <> v holds f.u = H(u) from FUNCT_2:sch 6;
  reconsider f as Element of Funcs(the carrier of V, REAL) by FUNCT_2:8;
  ex T being finite Subset of V st for u st not u in T holds f.u = 0
  proof
    take T = {v};
    let u;
    assume not u in T;
    then u <> v by TARSKI:def 1;
    hence thesis by A3;
  end;
  then reconsider f as Linear_Combination of V by RLVECT_2:def 3;
A4: Carrier(f) c= {v}
  proof
    let x;
    assume x in Carrier(f);
    then consider u such that
A5: x = u and
A6: f.u <> 0;
    u = v by A3,A6;
    hence thesis by A5,TARSKI:def 1;
  end;
  then reconsider f as Linear_Combination of {v} by RLVECT_2:def 6;
A7: Sum(f) = f.v * v by RLVECT_2:32
    .= v by A2,RLVECT_1:def 8;
  {v} c= A by A1,ZFMISC_1:31;
  then Carrier(f) c= A by A4,XBOOLE_1:1;
  then reconsider f as Linear_Combination of A by RLVECT_2:def 6;
  rng f c= INT
  proof
    let y be set;
    assume A8:y in rng f;
    consider x be set
    such that A9: x in the carrier of V & y=f.x by A8,FUNCT_2:11;
    reconsider z=x as VECTOR of V by A9;
    per cases;
    suppose z <> v; then
      f.z = 0 by A3;
      hence y in INT by A9,NUMBERS:17,TARSKI:def 3;
    end;
    suppose z = v;
      hence y in INT by A9,A2,NUMBERS:17,TARSKI:def 3;
    end;
  end;
  hence thesis by A7;
end;

theorem Th13:
  A c= B implies Z_Lin(A) c= Z_Lin(B)
proof
  assume
A1: A c= B;
  let v be set;
    assume v in Z_Lin(A);
    then consider l such that
A2: v = Sum(l) & rng l c= INT;
    reconsider l as Linear_Combination of B by A1,RLVECT_2:21;
    Sum(l) = v by A2;
    hence v in Z_Lin(B) by A2;
end;

theorem
  Z_Lin(A \/ B) = Z_Lin(A) + Z_Lin(B)
proof
  now
    let v be set;
    assume v in Z_Lin(A \/ B);
    then consider l being Linear_Combination of A \/ B such that
A1: v = Sum(l) & rng l c= INT;
    deffunc F(set)=l.$1;
    set D = Carrier(l) \ A;
    set C = Carrier(l) /\ A;
    defpred P[set] means $1 in C;
    defpred D[set] means $1 in D;
A2: for x st x in the carrier of V holds (P[x] implies F(x) in REAL) & (
    not P[x ] implies H(x) in REAL);
    consider f being Function of the carrier of V, REAL such that
A3: for x st x in the carrier of V holds (P[x] implies f.x = F(x)) &
    (not P[x] implies f.x = H(x)) from FUNCT_2:sch 5 (A2);
    reconsider C as finite Subset of V;
    reconsider f as Element of Funcs(the carrier of V, REAL) by FUNCT_2:8;
    for u holds not u in C implies f.u = 0 by A3;
    then reconsider f as Linear_Combination of V by RLVECT_2:def 3;
A4: rng f c= INT
    proof
      let y be set;
      assume A5:y in rng f;
      consider x be set such that
A6:   x in the carrier of V & y=f.x by A5,FUNCT_2:11;
       reconsider z=x as VECTOR of V by A6;
       per cases;
         suppose not z in C; then
         f.z = 0 by A3;
         hence y in INT by A6,NUMBERS:17,TARSKI:def 3;
        end;
         suppose z in C; then
         f.z = l.z by A3; then
         f.z in rng l by FUNCT_2:4;
         hence y in INT by A6,A1;
        end;
      end;
A7: Carrier(f) c= C
    proof
      let x;
      assume x in Carrier(f); then
A8:   ex u st x = u & f.u <> 0;
      assume not x in C;
      hence thesis by A3,A8;
    end;
    C c= A by XBOOLE_1:17;
    then Carrier(f) c= A by A7,XBOOLE_1:1;
    then reconsider f as Linear_Combination of A by RLVECT_2:def 6;
A9: for x st x in the carrier of V holds (D[x] implies F(x) in REAL) & (
    not D[x] implies H(x) in REAL);
    consider g being Function of the carrier of V, REAL such that
A10: for x st x in the carrier of V holds (D[x] implies g.x = F(x)) &
    (not D[x] implies g.x = H(x)) from FUNCT_2:sch 5(A9);
    reconsider D as finite Subset of V;
    reconsider g as Element of Funcs(the carrier of V, REAL) by FUNCT_2:8;
    for u holds not u in D implies g.u = 0 by A10;
    then reconsider g as Linear_Combination of V by RLVECT_2:def 3;
A11: rng g c= INT
   proof
       let y be set;
       assume A12:y in rng g;
       consider x be set
         such that A13: x in the carrier of V & y=g.x by A12,FUNCT_2:11;
       reconsider z=x as VECTOR of V by A13;
       per cases;
         suppose not z in D;
         then g.z = 0 by A10;
         hence y in INT by A13,NUMBERS:17,TARSKI:def 3;
        end;
         suppose z in D;
         then g.z = l.z by A10;
         then g.z in rng l by FUNCT_2:4;
         hence y in INT by A13,A1;
        end;
      end;
A14: D c= B
    proof
      let x;
      assume x in D; then
A15:   x in Carrier(l) & not x in A by XBOOLE_0:def 5;
      Carrier(l) c= A \/ B by RLVECT_2:def 6;
      hence thesis by A15,XBOOLE_0:def 3;
    end;
    Carrier(g) c= D
    proof
      let x;
      assume x in Carrier(g); then
A16:  ex u st x = u & g.u <> 0;
      assume not x in D;
      hence thesis by A10,A16;
    end;
    then Carrier(g) c= B by A14,XBOOLE_1:1;
    then reconsider g as Linear_Combination of B by RLVECT_2:def 6;
    l = f + g
    proof
      let v;
      now
        per cases;
        suppose
A17:      v in C;
A18:      now
            assume v in D;
            then not v in A by XBOOLE_0:def 5;
            hence contradiction by A17,XBOOLE_0:def 4;
          end;
          thus (f + g).v = f.v + g.v by RLVECT_2:def 10
            .= l.v + g.v by A3,A17
            .= l.v + z0 by A10,A18
            .= l.v;
        end;
        suppose
A19:      not v in C;
          now
            per cases;
            suppose
A20:          v in Carrier(l);
A21:          now
                assume not v in D;
                then not v in Carrier(l) or v in A by XBOOLE_0:def 5;
                hence contradiction by A19,A20,XBOOLE_0:def 4;
              end;
              thus (f + g). v = f.v + g.v by RLVECT_2:def 10
                .= z0 + g.v by A3,A19
                .= l.v by A10,A21;
            end;
            suppose
A22:          not v in Carrier(l); then
A23:          not v in D by XBOOLE_0:def 5;
A24:          not v in C by A22,XBOOLE_0:def 4;
              thus (f + g).v = f.v + g.v by RLVECT_2:def 10
                .= z0 + g.v by A3,A24
                .= z0 + z0 by A10,A23
                .= l.v by A22;
            end;
          end;
          hence thesis;
        end;
      end;
      hence thesis;
    end;
    then
A25: v = Sum(f) + Sum(g) by A1,RLVECT_3:1;
    Sum(f) in Z_Lin(A) & Sum(g) in Z_Lin(B) by A4,A11;
    hence v in Z_Lin(A) + Z_Lin(B) by A25;
  end;
  then
A26: Z_Lin(A \/ B) c= Z_Lin(A) + Z_Lin(B) by TARSKI:def 3;
A27: Z_Lin(A) c=Z_Lin(A \/ B) & Z_Lin(B) c= Z_Lin(A \/ B) by Th13,XBOOLE_1:7;
 now let x be set;
   assume x in Z_Lin(A) + Z_Lin(B); then
   consider u,v be Element of V such that
A28:x=u+v & u in Z_Lin(A) & v in Z_Lin(B);
    thus x in Z_Lin(A \/ B) by A28,A27,Th9;
 end; then
    Z_Lin(A) + Z_Lin(B) c= Z_Lin(A \/ B) by TARSKI:def 3;
  hence thesis by A26,XBOOLE_0:def 10;
end;

theorem
  Z_Lin(A /\ B) c= Z_Lin(A) /\ Z_Lin(B)
proof
  Z_Lin(A /\ B) c=Z_Lin(A) & Z_Lin(A /\ B) c=Z_Lin(B) by Th13,XBOOLE_1:17;
  hence thesis by XBOOLE_1:19;
end;

theorem Th16:
  x in Z_Lin{v} iff ex a be Integer st x = a * v
proof
  thus x in Z_Lin{v} implies ex a be Integer st x = a * v
  proof
    assume x in Z_Lin{v};
    then consider l being Linear_Combination of {v} such that
A1: x = Sum(l) & rng l c= INT;
A2: Sum(l) = l.v * v by RLVECT_2:32;
        ex f being Function st l = f & dom f = the carrier of V
              & rng f c= REAL by FUNCT_2:def 2; then
        l.v in rng l by FUNCT_1:3;
    hence thesis by A1,A2;
  end;
  given a0 be Integer such that
A3: x = a0 * v;
  reconsider a=a0 as Real by XREAL_0:def 1;
  consider f being Function of the carrier of V, REAL such that
A4: f.v = a and
A5: for z being VECTOR of V st z <> v holds f.z = H(z) from FUNCT_2:sch 6;
  reconsider f as Element of Funcs(the carrier of V,REAL) by FUNCT_2:8;
A6:now
    let z be VECTOR of V;
    assume not z in {v};
    then z <> v by TARSKI:def 1;
    hence f.z = 0 by A5;
  end;
  then reconsider f as Linear_Combination of V by RLVECT_2:def 3;
  Carrier f c= {v}
  proof
    let x;
    assume
A7: x in Carrier f;
    then f.x <> 0 by RLVECT_2:19;
    then x = v by A5,A7;
    hence thesis by TARSKI:def 1;
  end;
  then reconsider f as Linear_Combination of {v} by RLVECT_2:def 6;
A8:Sum(f) = x by A3,A4,RLVECT_2:32;
   rng f c= INT
      proof
       let y be set;
       assume A9:y in rng f;
       consider x be set
         such that A10: x in the carrier of V & y=f.x by A9,FUNCT_2:11;
       reconsider z=x as VECTOR of V by A10;
       per cases;
         suppose not z in {v}; then
         f.z = 0 by A6;
         hence y in INT by A10,NUMBERS:17,TARSKI:def 3;
        end;
         suppose z in {v}; then
         f.z = a0 by A4,TARSKI:def 1;
         hence y in INT by A10,INT_1:def 2;
        end;
      end;
  hence thesis by A8;
end;

theorem
  v in Z_Lin{v}
proof
  v in {v} by TARSKI:def 1;
  hence thesis by Th12;
end;

theorem
  x in v + Z_Lin{w} iff ex a be Integer st x = v + a * w
proof
  thus x in v + Z_Lin{w} implies ex a be Integer st x = v + a * w
  proof
    assume x in v + Z_Lin{w};
    then consider u being VECTOR of V such that
A1: x = v + u and
A2: u in Z_Lin{w};
    ex a be Integer st u = a * w by A2,Th16;
    hence thesis by A1;
  end;
  given a0 be Integer such that
A3: x = v + a0 * w;
  a0 * w in Z_Lin{w} by Th16;
  hence thesis by A3;
end;

theorem Th19:
  x in Z_Lin{w1,w2} iff ex a,b be Integer st x = a * w1 + b * w2
proof
  thus x in Z_Lin{w1,w2} implies ex a,b be Integer
    st x = a * w1 + b * w2
  proof
    assume
A1: x in Z_Lin{w1,w2};
    now
      per cases;
      suppose
        w1 = w2;
        then {w1,w2} = {w1} by ENUMSET1:29;
        then consider a be Integer such that
A2:     x = a * w1 by A1,Th16;
        consider b be Integer such that
A3:     b = 0;
        x = a * w1 + 0.V by A2,RLVECT_1:4;
        then x = a * w1 + b * w2 by A3,RLVECT_1:10;
        hence thesis;
      end;
      suppose
A4:     w1 <> w2;
        consider l being Linear_Combination of {w1,w2} such that
A5:     x = Sum(l) & rng l c= INT by A1;
A6:     x = l.w1 * w1 + l.w2 * w2 by A4,A5,RLVECT_2:33;
        ex f being Function st l = f & dom f = the carrier of V
              & rng f c= REAL by FUNCT_2:def 2; then
        l.w1 in rng l & l.w2 in rng l by FUNCT_1:3;
        hence thesis by A5,A6;
      end;
    end;
    hence thesis;
  end;
  given a0,b0 be Integer such that
A7: x = a0 * w1 + b0 * w2;
  reconsider a=a0,b=b0 as Real by XREAL_0:def 1;
  now
    per cases;
    suppose
A8:   w1 = w2;
      then x = (a + b) * w1 by A7,RLVECT_1:def 6;
      then x in Z_Lin{w1} by Th16;
      hence thesis by A8,ENUMSET1:29;
    end;
    suppose
A9:   w1 <> w2;
      consider f being Function of the carrier of V, REAL such that
A10:   f.w1 = a & f.w2 = b and
A11:   for u st u <> w1 & u <> w2 holds f.u = H(u) from FUNCT_2:sch 7(A9);
      reconsider f as Element of Funcs(the carrier of V,REAL) by FUNCT_2:8;
A12:  now
        let u;
        assume not u in {w1,w2};
        then u <> w1 & u <> w2 by TARSKI:def 2;
        hence f.u = 0 by A11;
      end;
      then reconsider f as Linear_Combination of V by RLVECT_2:def 3;
      Carrier f c= {w1,w2}
      proof
        let x;
        assume that
A13:    x in Carrier f and
A14:    not x in {w1,w2};
        x <> w1 & x <> w2 by A14,TARSKI:def 2;
        then f.x = 0 by A11,A13;
        hence contradiction by A13,RLVECT_2:19;
      end;
      then reconsider f as Linear_Combination of {w1,w2} by RLVECT_2:def 6;
A15:  x = Sum(f) by A7,A9,A10,RLVECT_2:33;
      rng f c= INT
      proof
       let y be set;
       assume A16:y in rng f;
       consider x be set
         such that A17: x in the carrier of V & y=f.x by A16,FUNCT_2:11;
       reconsider v=x as VECTOR of V by A17;
       per cases;
         suppose not v in {w1,w2}; then
         f.v = 0 by A12;
         hence y in INT by A17,NUMBERS:17,TARSKI:def 3;
        end;
         suppose v in {w1,w2}; then
         f.v = a0 or f.v = b0 by A10,TARSKI:def 2;
         hence y in INT by A17,INT_1:def 2;
        end;
      end;
      hence thesis by A15;
    end;
  end;
  hence thesis;
end;

theorem
  w1 in Z_Lin{w1,w2}
proof
  w1 in {w1,w2} by TARSKI:def 2;
  hence thesis by Th12;
end;

theorem
  x in v + Z_Lin{w1,w2} iff ex a,b be Integer
    st x = v + a * w1 + b * w2
proof
  thus x in v + Z_Lin{w1,w2} implies
    ex a,b be Integer st x = v + a * w1 + b * w2
  proof
    assume x in v + Z_Lin{w1,w2};
    then consider u such that
A1: x = v + u and
A2: u in Z_Lin{w1,w2};
    consider a,b be Integer such that
A3: u = a * w1 + b * w2 by A2,Th19;
    take a,b;
    thus thesis by A1,A3,RLVECT_1:def 3;
  end;
  given a,b be Integer such that
A4: x = v + a * w1 + b * w2;
  a * w1 + b * w2 in Z_Lin{w1,w2} by Th19;
  then v + (a * w1 + b * w2) in v + Z_Lin{w1,w2};
  hence thesis by A4,RLVECT_1:def 3;
end;

theorem Th22:
  x in Z_Lin{v1,v2,v3} iff ex a,b,c be Integer
   st x = a * v1 + b * v2 + c * v3
proof
  thus x in Z_Lin{v1,v2,v3} implies ex a,b,c be Integer
   st x = a * v1 + b * v2 + c * v3
  proof
    assume
A1: x in Z_Lin{v1,v2,v3};
    now
      per cases;
      suppose
A2:     v1 <> v2 & v1 <> v3 & v2 <> v3;
        consider l being Linear_Combination of {v1,v2,v3} such that
A3:     x = Sum(l) & rng l c= INT by A1;
A4:     x = l.v1 * v1 + l.v2 * v2 + l.v3 * v3 by A2,A3,RLVECT_4:6;
        ex f being Function st l = f & dom f = the carrier of V
              & rng f c= REAL by FUNCT_2:def 2; then
        l.v1 in rng l & l.v2 in rng l & l.v3 in rng l by FUNCT_1:3;
        hence thesis by A3,A4;
      end;
      suppose
        v1 = v2 or v1 = v3 or v2 = v3; then
A5:     {v1,v2,v3} = {v1,v3} or {v1,v2,v3} = {v1,v1,v2} or {v1,v2,v3} = {
        v3,v3,v1} by ENUMSET1:30,59;
        now
          per cases by A5,ENUMSET1:30;
          suppose
            {v1,v2,v3} = {v1,v2};
            then consider a,b be Integer such that
A6:         x = a * v1 + b * v2 by A1,Th19;
            consider c be Integer such that
A7:         c = 0;
            x = a * v1 + b * v2 + 0.V by A6,RLVECT_1:4
              .= a * v1 + b * v2 + c * v3 by A7,RLVECT_1:10;
            hence thesis;
          end;
          suppose
            {v1,v2,v3} = {v1,v3};
            then consider a,b be Integer such that
A8:         x = a * v1 + b * v3 by A1,Th19;
            consider c be Integer such that
A9:         c = 0;
            x = a * v1 + 0.V + b * v3 by A8,RLVECT_1:4
              .= a * v1 + c * v2 + b * v3 by A9,RLVECT_1:10;
            hence thesis;
          end;
        end;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
  given a0,b0,c0 be Integer such that
A10: x = a0 * v1 + b0 * v2 + c0 * v3;
  reconsider a=a0, b=b0, c = c0 as Real by XREAL_0:def 1;
  now
    per cases;
    suppose
A11:   v1 = v2 or v1 = v3 or v2 = v3;
      now
        per cases by A11;
        suppose v1 = v2;
          then {v1,v2,v3} = {v1,v3} & x = (a + b) * v1 + c * v3 by A10,
ENUMSET1:30,RLVECT_1:def 6;
          hence thesis by Th19;
        end;
        suppose
A12:       v1 = v3; then
A13:      {v1,v2,v3} = {v1,v1,v2} by ENUMSET1:57
            .= {v2,v1} by ENUMSET1:30;
          x = b * v2 + (a * v1 + c * v1) by A10,A12,RLVECT_1:def 3
            .= b * v2 + (a + c) * v1 by RLVECT_1:def 6;
          hence thesis by A13,Th19;
        end;
        suppose
A14:      v2 = v3;
          then
A15:      {v1,v2,v3} = {v2,v2,v1} by ENUMSET1:59
            .= {v1,v2} by ENUMSET1:30;
          x = a * v1 + (b * v2 + c * v2) by A10,A14,RLVECT_1:def 3
            .= a * v1 + (b + c) * v2 by RLVECT_1:def 6;
          hence thesis by A15,Th19;
        end;
      end;
      hence thesis;
    end;
    suppose
A16:  v1 <> v2 & v1 <> v3 & v2 <> v3;
A17:  v1 <> v3 by A16;
A18:  v2 <> v3 by A16;
A19:  v1 <> v2 by A16;
      consider f being Function of the carrier of V,REAL such that
A20:  f.v1 = a & f.v2 = b & f.v3 = c and
A21:  for v st v <> v1 & v <> v2 & v <> v3 holds f.v = H(v) from
      RLVECT_4:sch 1(A19,A17, A18);
      reconsider f as Element of Funcs(the carrier of V,REAL) by FUNCT_2:8;
A22:   now
        let v;
        assume
A23:    not v in {v1,v2,v3};
        then
A24:    v <> v3 by ENUMSET1:def 1;
        v <> v1 & v <> v2 by A23,ENUMSET1:def 1;
        hence f.v = 0 by A21,A24;
      end;
      then reconsider f as Linear_Combination of V by RLVECT_2:def 3;
      Carrier f c= {v1,v2,v3}
      proof
        let x;
        assume that
A25:    x in Carrier f and
A26:    not x in {v1,v2,v3};
A27:    x <> v3 by A26,ENUMSET1:def 1;
        x <> v1 & x <> v2 by A26,ENUMSET1:def 1;
        then f.x = 0 by A21,A25,A27;
        hence thesis by A25,RLVECT_2:19;
      end;
      then reconsider f as Linear_Combination of {v1,v2,v3} by RLVECT_2:def 6;
A28:  x = Sum(f) by A10,A16,A20,RLVECT_4:6;
     rng f c= INT
      proof
       let y be set;
       assume A29:y in rng f;
       consider x be set
         such that A30: x in the carrier of V & y=f.x by A29,FUNCT_2:11;
       reconsider v=x as VECTOR of V by A30;
       per cases;
         suppose not v in {v1,v2,v3};
         then f.v = 0 by A22;
         hence y in INT by A30,NUMBERS:17,TARSKI:def 3;
        end;
         suppose v in {v1,v2,v3}; then
         f.v = a0 or f.v = b0 or f.v = c0 by A20,ENUMSET1:def 1;
         hence y in INT by A30,INT_1:def 2;
        end;
      end;
      hence thesis by A28;
    end;
  end;
  hence thesis;
end;

theorem
  w1 in Z_Lin{w1,w2,w3} & w2 in Z_Lin{w1,w2,w3} & w3 in Z_Lin{w1,w2,w3}
proof
A1: w3 in {w1,w2,w3} by ENUMSET1:def 1;
  w1 in {w1,w2,w3} & w2 in {w1,w2,w3} by ENUMSET1:def 1;
  hence thesis by A1,Th12;
end;

theorem
  x in v + Z_Lin{w1,w2,w3}
   iff ex a,b,c be Integer st x = v + a * w1 + b * w2 + c * w3
proof
  thus x in v + Z_Lin{w1,w2,w3} implies ex a,b,c be Integer
    st x = v + a * w1 + b * w2 + c * w3
  proof
    assume x in v + Z_Lin{w1,w2,w3};
    then consider u such that
A1: x = v + u and
A2: u in Z_Lin{w1,w2,w3};
    consider a,b,c be Integer such that
A3: u = a * w1 + b * w2 + c * w3 by A2,Th22;
    take a,b,c;
    x = v + (a * w1 + b * w2) + c * w3 by A1,A3,RLVECT_1:def 3;
    hence thesis by RLVECT_1:def 3;
  end;
  given a,b,c be Integer such that
A4: x = v + a * w1 + b * w2 + c * w3;
  a * w1 + b * w2 + c * w3 in Z_Lin{w1,w2,w3} by Th22;
  then v + (a * w1 + b * w2 + c * w3) in v + Z_Lin{w1,w2,w3};
  then v + (a * w1 + b * w2) + c * w3 in v + Z_Lin{w1,w2,w3}
    by RLVECT_1:def 3;
  hence thesis by A4,RLVECT_1:def 3;
end;

Lm1:
 for RS be RealLinearSpace,
     X be Subset of RS,
     g1,h1 be FinSequence of RS,
        a1 be INT-valued FinSequence st
       rng g1 c= X & len g1 =len h1 & len g1 = len a1 &
       for i be Nat
         st i in Seg (len g1) holds
           h1/.i=(a1.i)*(g1/.i)
 holds Sum(h1) in Z_Lin(X)
  proof
    let RS be RealLinearSpace, X be Subset of RS;
    defpred P[Nat] means
    for g,h be FinSequence of RS,
     s be INT-valued FinSequence st
            rng g c= X &
            len g = $1 & len g = len h & len g = len s &
            for i be Nat st i in Seg (len g) holds
              h/.i=(s.i)*(g/.i) holds
  Sum(h) in Z_Lin(X);
A1: P[0]
proof
 let g,h be FinSequence of RS, s be INT-valued FinSequence;
 set x = Sum(h);
 assume A2:rng g c= X &
    len g = 0 & len g = len h & len g = len s &
    for i be Nat st i in Seg (len g) holds h/.i=(s.i)*(g/.i);
  Sum(h) = Sum(<*> the carrier of RS) by A2,FINSEQ_1:20
      .=0.RS by RLVECT_1:43;
  hence x in Z_Lin(X) by Th11;
end;
A3: now let n be Nat;
    assume A4: P[n];
   now let g,h be FinSequence of RS,
     s be INT-valued FinSequence, x be set;
     assume A5: x=Sum(h) & rng g c= X &
            len g = n+1 & len g = len h & len g = len s &
            for i be Nat st i in Seg (len g) holds h/.i=(s.i)*(g/.i);
     reconsider gn = g|n as FinSequence of RS;
     reconsider hn = h|n as FinSequence of RS;
     reconsider sn = s|n as real-valued FinSequence;
     rng gn c= X & len gn = n & len gn = len hn & len gn = len sn &
            for i be Nat st i in Seg (len gn) holds
              hn/.i=(sn.i)*(gn/.i)
     proof
       rng gn c= rng g by RELAT_1:70;
       then A6: rng gn c= X by A5,XBOOLE_1:1;
       A7: n <= len g by A5,NAT_1:11;
       A8: n <= len h by A5,NAT_1:11;
       A9: len hn = n by A5,FINSEQ_1:59,NAT_1:11;
       A10: len sn = n by A5,FINSEQ_1:59,NAT_1:11;
       for i be Nat st i in Seg (len gn) holds
       hn/.i=(sn.i)*(gn/.i)
       proof
         per cases;
         suppose n = 0;
           hence thesis;
         end;
         suppose n <> 0;
           then A11: n >= 1 by NAT_1:14;
           let i be Nat;
           assume i in Seg (len gn);
           then A12: i in Seg (n) by A5,FINSEQ_1:59,NAT_1:11;
           n in Seg (len g) by A7,A11,FINSEQ_1:1;
           then n in dom g by FINSEQ_1:def 3;
           then A13: gn/.i = g/.i by A12,FINSEQ_4:71;
           n in Seg (len h) by A8,A11,FINSEQ_1:1;
           then n in dom h by FINSEQ_1:def 3;
           then A14: hn/.i = h/.i by A12,FINSEQ_4:71;
           i <= n by A12,FINSEQ_1:1;
           then sn.i = s.i by FINSEQ_3:112;
           hence thesis by A5,A12,A13,A14,FINSEQ_2:8;
         end;
       end;
       hence thesis by A6,A9,A10,A5,FINSEQ_1:59,NAT_1:11;
     end; then
     A15:Sum(hn) in Z_Lin(X) by A4;
     A16: n+1 in Seg (len g) by A5,FINSEQ_1:4;
     A17: h/.(n+1) = s.(n+1)*g/.(n+1) by A5,FINSEQ_1:4;
     A18: h = hn ^ <* s.(n+1)*g/.(n+1) *> by A5,A17,FINSEQ_5:21;
     A19: n+1 in dom g by A16,FINSEQ_1:def 3;
     then g/.(n+1) = g.(n+1) by PARTFUN1:def 6;
     then g/.(n+1) in rng g by A19,FUNCT_1:3;
     then g/.(n+1) in Z_Lin(X) by A5,Th12; then
     A20: s.(n+1)*(g/.(n+1)) in Z_Lin(X) by Th10;
     Sum(h) = Sum(hn)+Sum(<* s.(n+1)*g/.(n+1) *>) by A18,RLVECT_1:41
           .= Sum(hn)+ s.(n+1)*(g/.(n+1)) by RLVECT_1:44;
     hence x in Z_Lin(X) by A5,A15,A20,Th9;
    end;
    hence P[n+1];
end;
for n be Nat holds P[n] from NAT_1:sch 2(A1,A3);
hence thesis;
end;

Lm2:
for x be set st x in Z_Lin(A) holds
    ex g1,h1 be FinSequence of V,
        a1 be INT-valued FinSequence
   st x=Sum(h1) &
       rng g1 c= A & len g1 =len h1 & len g1 = len a1 &
       for i be Nat st i in Seg (len g1) holds h1/.i=(a1.i)*(g1/.i)
proof
let x be set;
assume x in Z_Lin(A); then
  consider z be Linear_Combination of A such that
   A1: x=Sum(z) & rng z c= INT;
   consider F be FinSequence of V such that
   A2:  F is one-to-one & rng F = Carrier(z) & Sum(z)
      = Sum(z (#) F) by RLVECT_2:def 8;
A3: len (z (#) F) = len F &
      for i be Nat st i in dom (z (#) F)
     holds (z (#) F).i = z.(F/.i) * F/.i by RLVECT_2:def 7;
  defpred P0[Nat,set] means $2=z.(F/.$1);
  A4: now let k be Nat;
      assume k in Seg (len F);
      z.(F/.k) in rng z by FUNCT_2:4;
      hence ex x being Element of INT st P0[k,x] by A1;
  end;
consider u be FinSequence of INT such that
  A5: dom u = Seg (len F)
  & for i be Nat st i in Seg (len F) holds P0[i,u.i]
     from FINSEQ_1:sch 5(A4);
 A6: rng F c= A by A2,RLVECT_2:def 6;
 A7: len F = len (z (#) F) by RLVECT_2:def 7;
 A8: len F = len u by A5,FINSEQ_1:def 3;
   now
     let i be Nat;
     assume A9: i in Seg (len F); then
A10: i in dom (z (#) F) by A3,FINSEQ_1:def 3;
     hence (z (#) F)/.i = (z (#) F).i by PARTFUN1:def 6
                    .= z.(F/.i) * F/.i by A10,RLVECT_2:def 7
                    .=u.i * F/.i by A5,A9;
    end;
   hence thesis by A6,A7,A8,A1,A2;
end;

theorem
  for x be set holds x in Z_Lin(A) iff
    ex g1,h1 be FinSequence of V,
        a1 be INT-valued FinSequence
   st x=Sum(h1) &
       rng g1 c= A & len g1 =len h1 & len g1 = len a1 &
       for i be Nat
        st i in Seg (len g1) holds
           h1/.i=(a1.i)*(g1/.i) by Lm1,Lm2;

registration
  let D be non empty set, n be Nat;
  cluster n-element D-valued for FinSequence;
  existence
  proof
    take n |-> the Element of D;
    thus thesis;
  end;
end;

definition
  let RS be RealLinearSpace;
  let f be FinSequence of RS;
  func Z_Lin(f) -> Subset of RS equals
    {Sum(g) where g is (len f)-element FinSequence of RS :
    ex a be (len f)-element INT-valued FinSequence
     st for i be Nat st i in Seg (len f) holds g/.i=(a.i)*(f/.i)};
correctness
proof
now let x be set;
  assume x in {Sum(g) where g is (len f)-element FinSequence of RS :
  ex a be (len f)-element INT-valued FinSequence
   st for i be Nat
       st i in Seg (len f) holds
     g/.i=(a.i)*(f/.i)}; then
  ex g be (len f)-element FinSequence of RS st
  x=Sum(g) & ex a be (len f)-element INT-valued FinSequence
   st for i be Nat st i in Seg (len f) holds g/.i=(a.i)*(f/.i);
  hence x in the carrier of RS;
end;
hence thesis by TARSKI:def 3;
end;
end;

theorem Th26:
for RS be RealLinearSpace,
      f be FinSequence of RS,
      x be set holds
   x in Z_Lin(f) iff
     ex g be (len f)-element FinSequence of RS,
          a be (len f)-element INT-valued FinSequence st
          x=Sum(g) & for i be Nat st i in Seg (len f) holds
          g/.i=(a.i)*(f/.i)
proof
let RS be RealLinearSpace,
      f be FinSequence of RS,
      x be set;
 hereby assume x in Z_Lin(f); then
consider g be (len f)-element FinSequence of RS such that
A1: x=Sum(g) & ex s be (len f)-element INT-valued FinSequence
          st for i be Nat st i in Seg (len f) holds
          g/.i=(s.i)*(f/.i);
consider s be (len f)-element INT-valued FinSequence such that
A2: for i be Nat st i in Seg (len f) holds g/.i=(s.i)*(f/.i) by A1;
take g,s;
thus x=Sum(g) & for i be Nat st i in Seg (len f) holds
          g/.i=(s.i)*(f/.i) by A1,A2;
end;
assume ex g be (len f)-element FinSequence of RS,
          a be (len f)-element INT-valued FinSequence st
          x=Sum(g) & for i be Nat st i in Seg (len f) holds
          g/.i=(a.i)*(f/.i);
hence x in Z_Lin(f);
end;

theorem Th27:
for RS be RealLinearSpace,
      f be FinSequence of RS,
      x, y being Element of RS,
      a, b being Element of INT
    st x in Z_Lin(f) & y in Z_Lin(f) holds
(a * x) + (b * y) in Z_Lin(f)
proof
let RS be RealLinearSpace;
let f be FinSequence of RS;
let x, y be Element of RS;
let a, b be Element of INT;
 assume A1:x in Z_Lin(f) & y in Z_Lin(f);
consider g be (len f)-element FinSequence of RS,
          s be (len f)-element INT-valued FinSequence such that
A2:     x=Sum(g) &
          for i be Nat st i in Seg (len f) holds
          g/.i=(s.i)*(f/.i) by A1,Th26;
consider h be (len f)-element FinSequence of RS,
         t be (len f)-element INT-valued FinSequence such that
A3:    y=Sum(h) & for i be Nat st i in Seg (len f) holds
          h/.i=(t.i)*(f/.i) by A1,Th26;
defpred P0[Nat,set] means $2=a*(s.$1) + b*(t.$1);
A4: for k be Nat st k in Seg (len f) holds
      ex x being Element of INT st P0[k,x];
consider u be FinSequence of INT such that
A5: dom u = Seg (len f)
  & for i be Nat st i in Seg (len f) holds P0[i,u.i] from FINSEQ_1:sch 5(A4);
 len u = len f by A5,FINSEQ_1:def 3;
 then
 reconsider u as (len f)-element INT-valued FinSequence by CARD_1:def 7;
defpred P1[Nat,set] means $2=a*g/.$1 + b*h/.$1;
A6: for k be Nat st k in Seg (len f) holds
            ex x being Element of RS st P1[k,x];
consider w be FinSequence of RS such that
A7: dom w = Seg (len f)
  & for i be Nat st i in Seg (len f) holds P1[i,w.i]
         from FINSEQ_1:sch 5(A6);
len w = len f by A7,FINSEQ_1:def 3; then
 reconsider w as (len f)-element FinSequence of RS by CARD_1:def 7;
A8: now let i be Nat;
   assume A9: i in Seg (len f);
     hence w/.i=w.i by A7,PARTFUN1:def 6
        .=a*g/.i + b*h/.i by A7,A9;
end;
reconsider a0=a as Element of REAL by NUMBERS:15,TARSKI:def 3;
reconsider b0=b as Element of REAL by NUMBERS:15,TARSKI:def 3;
dom (a0(#)g) = dom g by VFUNCT_1:def 4
             .= Seg (len g) by FINSEQ_1:def 3;
then
A10: a0(#)g is FinSequence-like by FINSEQ_1:def 2;
rng (a0(#)g) c= the carrier of RS; then
reconsider ag = a0(#)g as FinSequence of RS by A10,FINSEQ_1:def 4;
dom (b0(#)h) = dom h by VFUNCT_1:def 4
             .= Seg (len h) by FINSEQ_1:def 3;
then
A11: b0(#)h is FinSequence-like by FINSEQ_1:def 2;
rng (b0(#)h) c= the carrier of RS;
then
reconsider bh = b0(#)h as FinSequence of RS by A11,FINSEQ_1:def 4;
A12: dom (a0(#)g) = dom g by VFUNCT_1:def 4
                 .=Seg (len g) by FINSEQ_1:def 3
                 .=Seg (len f) by CARD_1:def 7; then
A13: len ag = len f by FINSEQ_1:def 3;
A14: dom (b0(#)h) = dom h by VFUNCT_1:def 4
                 .=Seg (len h) by FINSEQ_1:def 3
                 .=Seg (len f) by CARD_1:def 7;
A15:now let i be Element of NAT;
   assume A16:i in dom ag;
   hence w.i = a*g/.i + b*h/.i by A7,A12
    .= ag/.i + b*h/.i by A16,VFUNCT_1:def 4
    .= ag/.i + bh/.i by A16,A14,A12,VFUNCT_1:def 4;
end;
A17: len ag = len bh & len ag = len w by A7,A13,A14,FINSEQ_1:def 3;
A18:  for i be Nat st i in Seg (len f) holds
          w/.i=(u.i)*(f/.i)
proof
 let i be Nat;
   assume A19:i in Seg (len f);
   hence w/.i=a*g/.i + b*h/.i by A8
       .=a*((s.i)*(f/.i)) + b*h/.i by A19,A2
       .=a*((s.i)*(f/.i)) + b*((t.i)*(f/.i)) by A19,A3
       .=(a*(s.i))*(f/.i) + b*((t.i)*(f/.i)) by RLVECT_1:def 7
       .=(a*(s.i))*(f/.i) + (b*(t.i))*(f/.i) by RLVECT_1:def 7
       .= (a*(s.i) + b*(t.i))* (f/.i) by RLVECT_1:def 6
       .= (u.i)*(f/.i) by A19,A5;
end;
(a * x) + (b * y) = Sum(ag) + (b * Sum(h)) by A2,A3,Th3
 .= Sum(ag) + Sum(bh) by Th3
 .= Sum(w) by A15,A17,RLVECT_2:2;
hence (a * x) + (b * y) in Z_Lin(f) by A18;
end;

theorem Th28:
  for RS be RealLinearSpace,
      f be FinSequence of RS st f = (Seg len f) --> 0.RS
    holds Sum(f)=0.RS
proof
  let RS be RealLinearSpace, f be FinSequence of RS;
  assume A1:f = (Seg len f) --> 0.RS;
A2:now let k be Element of NAT, v be Element of RS;
     assume A3: k in dom f & v = f.k; then
     k in Seg (len f) by FINSEQ_1:def 3; then
     f.k = 0.RS by A1,FUNCOP_1:7;
     hence f.k = -v by A3,RLVECT_1:12;
   end;
   len f = len f;
   then Sum(f) = -Sum(f) by A2,RLVECT_1:40;
   hence thesis by RLVECT_1:19;
end;

theorem Th29:
for RS be RealLinearSpace,
      f be FinSequence of RS,
      v be Element of RS ,i be Nat st i in Seg (len f)
    & f = ( (Seg (len f)) --> 0.RS) +* ( {i} --> v)
holds Sum(f)=v
proof
  let RS be RealLinearSpace, f be FinSequence of RS;
  let v be Element of RS, i be Nat;
  defpred P[Nat] means for g be FinSequence of RS
   st len g = $1 & i in Seg (len g) &
   g = ( (Seg (len g)) --> 0.RS) +* ( {i} --> v) holds Sum(g)=v;
A1: P[0];
A2: now let n be Nat;
    assume A3: P[n];
     now let f be FinSequence of RS;
     assume A4: len f = n+1 & i in Seg (len f) &
     f = ((Seg len f) --> 0.RS) +* ( {i} --> v);
     reconsider g = f|n as FinSequence of RS;
     n+1 in Seg (n+1) by FINSEQ_1:4; then
     A5: n+1 in dom f by A4,FINSEQ_1:def 3;
     A6: len g = n by A4,FINSEQ_1:59,NAT_1:11;
     f = (f|n) ^<*f.(n+1)*> by A4,FINSEQ_3:55
          .=g ^<*f/.(n+1)*> by A5,PARTFUN1:def 6;
    then
    A7: Sum(f)=Sum(g)+Sum(<*f/.(n+1)*>) by RLVECT_1:41;
    A8: dom ( {i} --> v) = {i} by FUNCOP_1:13;
    let f1 be Function such that A9: f1 = (( Seg (len f)) --> 0.RS);
    let f2 be Function such that A10: f2 = ( {i} --> v);
    per cases;
    suppose A11: i = n+1;
      then dom f2 = {n+1} by A10,FUNCOP_1:13;
      then g = f1|Seg(n) by A4,A9,A10,FINSEQ_3:14,FUNCT_4:72
      .= ( ( Seg(len f) /\ Seg(n)) --> 0.RS) by A9,FUNCOP_1:12;
      then A12: g = ( ( Seg (n)) --> 0.RS) by A4,FINSEQ_1:7,NAT_1:11;
      A13: n+1 in {n+1} by ZFMISC_1:31;
      then n+1 in dom f2 by A10,A11,FUNCOP_1:13;
      then f.(n+1) = f2.(n+1) by A4,A10,FUNCT_4:13
      .= v by A10,A11,A13,FUNCOP_1:7;
      then A14: f/.(n+1) = v by A5,PARTFUN1:def 6;
      Sum(g) = 0.RS by A6,A12,Th28;
      hence Sum(f) = 0.RS + v by A7,A14,RLVECT_1:44
             .= v by RLVECT_1:4;
     end;
    suppose A15: i <> n+1;
     then i < n+1 or i > n+1 by XXREAL_0:1;
     then 1 <= i & i <= n by A4,FINSEQ_1:1,NAT_1:13; then
     A16: i in Seg (len g) by A6,FINSEQ_1:1;
     g = f1|Seg(n) +* f2|Seg(n) by A4,A9,A10,FUNCT_4:71
     .= ( ( Seg(len f) /\ Seg(n)) --> 0.RS) +* f2|Seg(n) by A9,FUNCOP_1:12
     .= ( ( Seg len g) --> 0.RS) +* f2|Seg(n) by A4,A6,FINSEQ_1:7,NAT_1:11
     .= ( ( Seg len g) --> 0.RS) +*
({i} /\ Seg (n) --> v) by A10,FUNCOP_1:12; then
     A17: g = ( (Seg (len g)) --> 0.RS)
+* ( {i} --> v) by A6,A16,ZFMISC_1:46;
     not {n+1} c= dom f2 by A8,A10,A15,ZFMISC_1:3;
     then not n+1 in dom f2 by ZFMISC_1:31;
     then f.(n+1) = f1.(n+1) by A4,A9,A10,FUNCT_4:11
     .= 0.RS by A4,A9,FINSEQ_1:4,FUNCOP_1:7;
     then A18: f/.(n+1) = 0.RS by A5,PARTFUN1:def 6;
     Sum(g) = v by A16,A17,A6,A3;
     hence Sum(f) = v + 0.RS by A7,A18,RLVECT_1:44
             .= v by RLVECT_1:4;
    end;
end;
hence P[n+1];
end;
for n be Nat holds P[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;

theorem Th30:
for RS be RealLinearSpace,
      f be FinSequence of RS,
       i be Nat st i in Seg (len f) holds f/.i in Z_Lin(f)
proof
  let RS be RealLinearSpace, f be FinSequence of RS;
  let i be Nat;
  assume A1: i in Seg (len f);
  set s = ( (Seg len f) --> 0) +* ( {i} --> 1);
A2:dom s = Seg len f
  proof
  dom s = dom ((Seg (len f)) --> 0) \/ dom( {i} -->1) by FUNCT_4:def 1
  .= (Seg (len f)) \/ dom( {i} -->1) by FUNCOP_1:13
  .= (Seg (len f)) \/ {i} by FUNCOP_1:13;
  hence thesis by A1,ZFMISC_1:40;
end; then
A3: s is FinSequence-like by FINSEQ_1:def 2;
rng s c= INT
proof
  rng s c= rng ( (Seg (len f)) --> 0) \/ rng ( {i} --> 1) by FUNCT_4:17;
  hence thesis by XBOOLE_1:1;
end; then
reconsider s as FinSequence of INT by A3,FINSEQ_1:def 4;
  len s = len f by A2,FINSEQ_1:def 3; then
 reconsider s as (len f)-element INT-valued FinSequence by CARD_1:def 7;
  defpred Q[Nat,set] means $2=s.$1*f/.$1;
A6: for k be Nat st k in Seg (len f) holds
      ex x being Element of RS st Q[k,x];
  consider w be FinSequence of RS such that
A7: dom w = Seg len f & for i be Nat st i in Seg (len f) holds
          Q[i,w.i] from FINSEQ_1:sch 5(A6);
A8:len w = len f by A7,FINSEQ_1:def 3;
 then reconsider w as (len f)-element FinSequence of RS by CARD_1:def 7;
now let i be Nat;
   assume A9: i in Seg len f;
     hence w/.i=w.i by A7,PARTFUN1:def 6
        .=s.i*f/.i by A7,A9;
end; then
A10:Sum(w) in Z_Lin(f);
A11:w = ( (Seg (len w)) --> 0.RS) +* ( {i} --> f/.i)
proof
  consider w1 be Function such that A12: w1 = (( Seg (len f)) --> 0.RS);
  A13: dom w1 = Seg (len f) by A12,FUNCOP_1:13;
  consider w2 be Function such that A14: w2 = ( {i} --> f/.i);
  A15: dom w2 = {i} by A14,FUNCOP_1:13;
  consider ww be Function such that A16: ww = w1 +* w2;
  A17: dom ww = Seg (len f) \/ {i} by A13,A15,A16,FUNCT_4:def 1
  .= Seg (len f) by A1,ZFMISC_1:40; then
  reconsider ww as FinSequence by FINSEQ_1:def 2;
  rng w1 c= {0.RS} by A12,FUNCOP_1:13;
  then A18: rng w1 c= (the carrier of RS) by XBOOLE_1:1;
  rng w2 c= {f/.i} by A14,FUNCOP_1:13;
  then A19: rng w2 c= (the carrier of RS) by XBOOLE_1:1;
  A20: rng ww c= rng w1 \/ rng w2 by A16,FUNCT_4:17;
  rng w1 \/ rng w2 c= (the carrier of RS) by A18,A19,XBOOLE_1:8;
  then rng ww c= (the carrier of RS) by A20,XBOOLE_1:1;
  then
  reconsider ww as FinSequence of RS by FINSEQ_1:def 4;
  for j being Nat st j in dom w holds w/.j = ww/.j
  proof
    let j be Nat such that A21: j in dom w;
    A22: dom({i} --> 1) ={i} by FUNCOP_1:13;
    per cases;
    suppose A23: j in dom w2;
      then A24: j = i by A15,TARSKI:def 1;
      then w/.j = w.i by A21,PARTFUN1:def 6;
      then A25: w/.j = s.i*f/.i by A7,A21,A24;
      A26:i in {i} by TARSKI:def 1;
      then A27: s.i = ({i} --> 1).i by A22,FUNCT_4:13
      .= 1 by A26,FUNCOP_1:7;
      ww/.j = ww.j by A7,A17,A21,PARTFUN1:def 6
      .= w2.j by A16,A23,FUNCT_4:13
      .= f/.i by A14,A15,A23,FUNCOP_1:7;
      hence thesis by A25,A27,RLVECT_1:def 8;
    end;
    suppose A28: not j in dom w2;
      w/.j = w.j by A21,PARTFUN1:def 6;
      then A29: w/.j = s.j*f/.j by A7,A21;
      not j in dom({i} --> 1) by A15,A28;
      then A30: s.j = ( (Seg (len f)) --> 0).j by FUNCT_4:11
      .= 0 by A7,A21,FUNCOP_1:7;
      ww/.j = ww.j by A7,A17,A21,PARTFUN1:def 6
      .= w1.j by A16,A28,FUNCT_4:11
      .= 0.RS by A7,A12,A21,FUNCOP_1:7;
      hence thesis by A29,A30,RLVECT_1:10;
    end;
  end;
  hence thesis by A7,A8,A12,A14,A16,A17,FINSEQ_5:12;
end;
i in Seg (len w) by A7,A1,FINSEQ_1:def 3;
hence f/.i in Z_Lin(f) by A10,A11,Th29;
end;

theorem Th31:
  for RS be RealLinearSpace,
      f be FinSequence of RS holds
    rng f c= Z_Lin(f)
proof
  let RS be RealLinearSpace, f be FinSequence of RS;
  let y be set;
    assume y in rng f; then
    consider x be set such that
A1: x in dom f & y=f.x by FUNCT_1:def 3;
A2: x in Seg len f by A1,FINSEQ_1:def 3;
    reconsider i=x as Nat by A1;
    y=f/.i by A1,PARTFUN1:def 6;
    hence y in Z_Lin(f) by A2,Th30;
end;

theorem Th32:
for RS be RealLinearSpace,
      f be non empty FinSequence of RS,
     g,h be FinSequence of RS,
     s be INT-valued FinSequence
        st rng g c= Z_Lin(f) &
            len g = len s & len g = len h &
            for i be Nat st i in Seg (len g) holds
              h/.i=(s.i)*(g/.i) holds
  Sum(h) in Z_Lin(f)
proof
let RS be RealLinearSpace,
    f be non empty FinSequence of RS;
1<=1 & 1 <= len f by FINSEQ_1:20; then
1 in Seg (len f); then
A1:f/.1 in Z_Lin(f) by Th30;
reconsider z0=0 as Element of INT by NUMBERS:17,TARSKI:def 3;
reconsider z1=1 as Element of INT by NUMBERS:17,TARSKI:def 3;
z0 * (f/.1) + z0 * (f/.1) in Z_Lin(f) by Th27,A1; then
z0 * (f/.1) + 0.RS in Z_Lin(f) by RLVECT_1:10; then
A2: 0.RS + 0.RS in Z_Lin(f) by RLVECT_1:10;
defpred P[Nat] means
for g,h be FinSequence of RS,
     s be INT-valued FinSequence
        st rng g c= Z_Lin(f) &
            len g = $1 & len g = len s & len g = len h &
            for i be Nat st i in Seg (len g) holds
              h/.i=(s.i)*(g/.i) holds
  Sum(h) in Z_Lin(f);
A3: P[0]
proof
let g,h be FinSequence of RS, s be INT-valued FinSequence;
 assume A4:rng g c= Z_Lin(f) &
            len g = 0 & len g = len s & len g = len h &
            for i be Nat st i in Seg (len g) holds
              h/.i=(s.i)*(g/.i);
Sum(h)= Sum(<*> the carrier of RS) by A4,FINSEQ_1:20
      .=0.RS by RLVECT_1:43;
hence Sum(h) in Z_Lin(f) by A2,RLVECT_1:4;
end;
A5:now let n be Nat;
    assume A6: P[n];
   now let g,h be FinSequence of RS,
     s be INT-valued FinSequence;
     assume A7:rng g c= Z_Lin(f) &
            len g = n+1 & len g = len s & len g = len h &
            for i be Nat st i in Seg (len g) holds h/.i=(s.i)*(g/.i);
     reconsider gn = g|n as FinSequence of RS;
     reconsider hn = h|n as FinSequence of RS;
     reconsider sn = s|n as INT-valued FinSequence;
     A8:rng gn c= Z_Lin(f) &
            len gn = n & len gn = len sn & len gn = len hn &
            for i be Nat st i in Seg (len gn) holds
              hn/.i=(sn.i)*(gn/.i)
     proof
       A9: rng gn c= rng g by RELAT_1:70;
       A10: n <= len g by A7,NAT_1:11;
       A11: n <= len h by A7,NAT_1:11;
       A12: len hn = n by A7,FINSEQ_1:59,NAT_1:11;
       A13: len sn = n by A7,FINSEQ_1:59,NAT_1:11;
       for i be Nat st i in Seg (len gn) holds hn/.i=(sn.i)*(gn/.i)
       proof
         per cases;
         suppose n = 0;
           hence thesis;
         end;
         suppose n <> 0;
           then A14: n >= 1 by NAT_1:14;
           let i be Nat;
           assume i in Seg (len gn);
           then A15: i in Seg (n) by A7,FINSEQ_1:59,NAT_1:11;
           n in Seg (len g) by A10,A14,FINSEQ_1:1;
           then n in dom g by FINSEQ_1:def 3;
           then A16: gn/.i = g/.i by A15,FINSEQ_4:71;
           n in Seg (len h) by A11,A14,FINSEQ_1:1;
           then n in dom h by FINSEQ_1:def 3;
           then A17: hn/.i = h/.i by A15,FINSEQ_4:71;
           i <= n by A15,FINSEQ_1:1;
           then sn.i = s.i by FINSEQ_3:112;
           hence thesis by A7,A15,A16,A17,FINSEQ_2:8;
         end;
       end;
       hence thesis by A9,A10,A12,A13,A7,FINSEQ_1:59,XBOOLE_1:1;
     end;
     A18:Sum(hn) in Z_Lin(f) by A8,A6;
     A19: n+1 in Seg (len g) by A7,FINSEQ_1:4;
     A20: h/.(n+1) = s.(n+1)*g/.(n+1) by A7,FINSEQ_1:4;
     A21: h = hn ^ <* s.(n+1)*g/.(n+1) *> by A7,A20,FINSEQ_5:21;
     A22: n+1 in dom g by A19,FINSEQ_1:def 3;
     then g/.(n+1) = g.(n+1) by PARTFUN1:def 6;
     then g/.(n+1) in rng g by A22,FUNCT_1:3;
     then
     z1*s.(n+1)*(g/.(n+1)) + z0 * (g/.(n+1)) in Z_Lin(f) by A7,Th27;
     then z1*s.(n+1)*(g/.(n+1)) + 0.RS in Z_Lin(f) by RLVECT_1:10;
     then z1*s.(n+1)*(g/.(n+1)) in Z_Lin(f) by RLVECT_1:4;
     then z1*Sum(hn)+z1* (s.(n+1)*(g/.(n+1))) in Z_Lin(f) by A18,Th27;
     then
     A23: z1*Sum(hn)+s.(n+1)*(g/.(n+1)) in Z_Lin(f) by RLVECT_1:def 8;
     Sum(h) =Sum(hn)+Sum(<* s.(n+1)*(g/.(n+1)) *>) by A21,RLVECT_1:41
            .=Sum(hn)+ s.(n+1)*(g/.(n+1)) by RLVECT_1:44;
     hence Sum(h) in Z_Lin(f) by A23,RLVECT_1:def 8;
    end;
    hence P[n+1];
end;
for n be Nat holds P[n] from NAT_1:sch 2(A3,A5);
hence thesis;
end;

theorem
  for RS be RealLinearSpace,
      f be non empty FinSequence of RS holds
    Z_Lin (rng f) = Z_Lin f
proof
let RS be RealLinearSpace,
    f be non empty FinSequence of RS;
 for x be set holds x in Z_Lin (rng f) iff x in Z_Lin f
proof
  let x be set;
  hereby assume x in Z_Lin (rng f); then
    consider g,h be FinSequence of RS,
        a be INT-valued FinSequence such that
A1:x=Sum(h) & rng g c= rng f & len g =len h & len g = len a &
     for i be Nat st i in Seg (len g) holds
     h/.i=(a.i)*(g/.i) by Lm2;
  rng f c= Z_Lin f by Th31;
  hence x in Z_Lin f by A1,Th32,XBOOLE_1:1;
end;
assume x in Z_Lin f;
then consider g be (len f)-element FinSequence of RS,
       a be (len f)-element INT-valued FinSequence such that
  A2:  x=Sum(g) & for i be Nat st i in Seg (len f) holds
          g/.i=(a.i)*(f/.i) by Th26;
  len f =len g & len a = len f by CARD_1:def 7;
  hence x in Z_Lin (rng f) by A2,Lm1;
end;
hence thesis by TARSKI:1;
end;

theorem Th34:
  Lin Z_Lin A = Lin A
proof
  for x be set st x in A holds x in Z_Lin(A) by Th12; then
  A c= Z_Lin(A) by TARSKI:def 3; then
A1: Lin(A) is Subspace of Lin(Z_Lin(A)) by RLVECT_3:20;
  reconsider W = the carrier of Lin(A) as Subset of V by RLSUB_1:def 2;
  Lin(Z_Lin A) is Subspace of Lin(W) by Th8,RLVECT_3:20; then
  Lin(Z_Lin A) is Subspace of Lin(A) by RLVECT_3:18;
  hence thesis by A1,RLSUB_1:26;
end;

theorem Th35:
  for x be set, g1,h1 be FinSequence of V,
      a1 be INT-valued FinSequence st x=Sum(h1) &
    rng g1 c= Z_Lin(A) & len g1 =len h1 & len g1 = len a1 &
    for i be Nat st i in Seg (len g1) holds
        h1/.i=(a1.i)*(g1/.i) holds x in Z_Lin(A)
proof
  reconsider z0=0 as Element of INT by NUMBERS:17,TARSKI:def 3;
  reconsider z1=1 as Element of INT by NUMBERS:17,TARSKI:def 3;
  defpred P[Nat] means for x be set, g1,h1 be FinSequence of V,
  a1 be INT-valued FinSequence st x = Sum(h1) &
  rng g1 c= Z_Lin(A) & len g1 = $1 & len g1 =len h1 & len g1 = len a1 &
  for i be Nat st i in Seg (len g1) holds
  h1/.i=(a1.i)*(g1/.i) holds x in Z_Lin(A);
  A1: P[0]
  proof
    let x be set, g1,h1 be FinSequence of V,
    a1 be INT-valued FinSequence;
    assume A2: x = Sum(h1) &
    rng g1 c= Z_Lin(A) & len g1 = 0 & len g1 =len h1 & len g1 = len a1 &
    for i be Nat st i in Seg (len g1) holds h1/.i=(a1.i)*(g1/.i);
    Sum(h1) = Sum(<*> the carrier of V) by A2,FINSEQ_1:20
    .= 0.V by RLVECT_1:43;
    hence x in Z_Lin(A) by A2,Th11;
  end;
A3: now let n be Nat;
    assume A4: P[n];
    now let x be set, g1,h1 be FinSequence of V,
      a1 be INT-valued FinSequence;
      assume A5: x = Sum(h1) &
      rng g1 c= Z_Lin(A) & len g1 = n+1 & len g1 =len h1 & len g1 = len a1 &
      for i be Nat st i in Seg (len g1) holds h1/.i=(a1.i)*(g1/.i);
      reconsider gn = g1|n as FinSequence of V;
      reconsider hn = h1|n as FinSequence of V;
      reconsider an = a1|n as INT-valued FinSequence;
      A6:rng gn c= Z_Lin(A) &
            len gn = n & len gn = len an & len gn = len hn &
            for i be Nat st i in Seg (len gn) holds
              hn/.i=(an.i)*(gn/.i)
      proof
        A7: rng gn c= rng g1 by RELAT_1:70;
        A8: n <= len g1 by A5,NAT_1:11;
        A9: n <= len h1 by A5,NAT_1:11;
        A10: len hn = n by A5,FINSEQ_1:59,NAT_1:11;
        A11: len an = n by A5,FINSEQ_1:59,NAT_1:11;
        for i be Nat st i in Seg (len gn) holds
        hn/.i=(an.i)*(gn/.i)
        proof
          per cases;
          suppose n = 0;
            hence thesis;
          end;
          suppose n <> 0;
            then A12: n >= 1 by NAT_1:14;
            let i be Nat;
            assume i in Seg (len gn);
            then A13: i in Seg (n) by A5,FINSEQ_1:59,NAT_1:11;
            n in Seg (len g1) by A8,A12,FINSEQ_1:1;
            then n in dom g1 by FINSEQ_1:def 3;
            then A14: gn/.i = g1/.i by A13,FINSEQ_4:71;
            n in Seg (len h1) by A9,A12,FINSEQ_1:1;
            then n in dom h1 by FINSEQ_1:def 3;
            then A15: hn/.i = h1/.i by A13,FINSEQ_4:71;
            i <= n by A13,FINSEQ_1:1;
            then an.i = a1.i by FINSEQ_3:112;
            hence thesis by A5,A13,A14,A15,FINSEQ_2:8;
          end;
        end;
        hence thesis by A5,A7,A8,A10,A11,FINSEQ_1:59,XBOOLE_1:1;
      end;
      A16: n+1 in Seg (len g1) by A5,FINSEQ_1:4;
      A17: h1/.(n+1) = a1.(n+1)*g1/.(n+1) by A5,FINSEQ_1:4;
      A18: h1 = hn ^ <* a1.(n+1)*g1/.(n+1) *> by A5,A17,FINSEQ_5:21;
      A19: n+1 in dom g1 by A16,FINSEQ_1:def 3; then
      g1/.(n+1) = g1.(n+1) by PARTFUN1:def 6; then
      g1/.(n+1) in rng g1 by A19,FUNCT_1:3; then
      z1*a1.(n+1)*(g1/.(n+1)) in Z_Lin(A) &
      z0*(g1/.(n+1)) in Z_Lin(A) by A5,Th10; then
      z1*a1.(n+1)*(g1/.(n+1)) + z0*(g1/.(n+1)) in Z_Lin(A) by Th9; then
      z1*a1.(n+1)*(g1/.(n+1)) + 0.V in Z_Lin(A) by RLVECT_1:10; then
      A20: z1*(a1.(n+1))*(g1/.(n+1)) in Z_Lin(A) by RLVECT_1:4;
      z1*Sum(hn) in Z_Lin(A) by A4,A6,Th10;
      then A21: z1*Sum(hn)+z1*(a1.(n+1))*(g1/.(n+1)) in Z_Lin(A) by A20,Th9;
      Sum(h1) =Sum(hn)+Sum(<* a1.(n+1)*(g1/.(n+1)) *>) by A18,RLVECT_1:41
      .=Sum(hn)+ a1.(n+1)*(g1/.(n+1)) by RLVECT_1:44;
      hence Sum(h1)in Z_Lin(A) by A21,RLVECT_1:def 8;
    end;
    hence P[n+1];
  end;
  for n be Nat holds P[n] from NAT_1:sch 2(A1,A3);
  hence thesis;
end;

theorem
  Z_Lin Z_Lin A = Z_Lin A
proof
  for x be set st x in A holds x in Z_Lin(A) by Th12;
  then A c= Z_Lin(A) by TARSKI:def 3; then
A1: Z_Lin(A) c= Z_Lin( Z_Lin(A)) by Th13;
  Z_Lin Z_Lin A c= Z_Lin(A)
  proof
    let x be set;
    assume x in Z_Lin( Z_Lin(A));
    then consider g1,h1 be FinSequence of V,
    a1 be INT-valued FinSequence such that
A2: x=Sum(h1) &
    rng g1 c= Z_Lin(A) & len g1 = len h1 & len g1 = len a1 &
    for i be Nat st i in Seg (len g1) holds h1/.i=(a1.i)*(g1/.i) by Lm2;
    thus x in Z_Lin(A) by A2,Th35;
  end;
  hence thesis by A1,XBOOLE_0:def 10;
end;

theorem
  Z_Lin(A) = Z_Lin(B) implies Lin(A) = Lin(B)
proof
  assume Z_Lin(A) = Z_Lin(B);
  hence Lin(A) = Lin( Z_Lin(B)) by Th34
            .= Lin(B) by Th34;
end;