:: RLVECT_X semantic presentation

begin

reconsider z0 = 0 as Real ;

deffunc H1( set ) ->  Element of NAT = 0 ;

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

theorem :: RLVECT_X:2
for X being RealLinearSpace
for R1, R2, R3 being FinSequence of X st len R1 = len R2 & R3 = R1 - R2 holds
Sum R3 = (Sum R1) - (Sum R2)
proof
let X be RealLinearSpace; ::_thesis: for R1, R2, R3 being FinSequence of X st len R1 = len R2 & R3 = R1 - R2 holds
Sum R3 = (Sum R1) - (Sum R2)
let R1, R2, R3 be FinSequence of X; ::_thesis: ( len R1 = len R2 & R3 = R1 - R2 implies Sum R3 = (Sum R1) - (Sum R2) )
assume A1: ( len R1 = len R2 & R3 = R1 - R2 ) ; ::_thesis: Sum R3 = (Sum R1) - (Sum 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 being Element of NAT st k in dom R1 holds
R3 . k = (R1 /. k) - (R2 /. k)
proof
let k be Element of NAT ; ::_thesis: ( k in dom R1 implies R3 . k = (R1 /. k) - (R2 /. k) )
assume A5: k in dom R1 ; ::_thesis: R3 . k = (R1 /. k) - (R2 /. k)
hence R3 . k = R3 /. k by A3, PARTFUN1:def_6
.= (R1 /. k) - (R2 /. k) by A1, A5, A3, VFUNCT_1:def_2 ;
::_thesis: verum
end;
hence  Sum R3 = (Sum R1) - (Sum R2) by A1, A4, RLVECT_2:5; ::_thesis: verum
end;

theorem Th3: :: RLVECT_X:3
for X being RealLinearSpace
for R1, R2 being FinSequence of X
for a being Element of REAL st R2 = a (#) R1 holds
Sum R2 = a * (Sum R1)
proof
let X be RealLinearSpace; ::_thesis: for R1, R2 being FinSequence of X
for a being Element of REAL st R2 = a (#) R1 holds
Sum R2 = a * (Sum R1)
let R1, R2 be FinSequence of X; ::_thesis: for a being Element of REAL st R2 = a (#) R1 holds
Sum R2 = a * (Sum R1)
let a be Element of REAL ; ::_thesis: ( R2 = a (#) R1 implies Sum R2 = a * (Sum R1) )
assume A1: R2 = a (#) R1 ; ::_thesis: Sum R2 = a * (Sum R1)
 dom R2 = dom R1 by A1, VFUNCT_1:def_4;
then A2: len R2 = len R1 by FINSEQ_3:29;
 for k being Element of NAT st k in dom R1 holds
R2 . k = a * (R1 /. k)
proof
let k be Element of NAT ; ::_thesis: ( k in dom R1 implies R2 . k = a * (R1 /. k) )
assume  k in dom R1 ; ::_thesis: R2 . k = a * (R1 /. k)
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 ;
::_thesis: verum
end;
hence  Sum R2 = a * (Sum R1) by A2, RLVECT_2:3; ::_thesis: verum
end;

begin


definition
let V be RealLinearSpace;
let i be Integer;
let L be Linear_Combination of V;
funci * L ->  Linear_Combination of V means :Def1: :: RLVECT_X:def 1
 for v being VECTOR of V holds it . v = i * (L . v);
existence
 ex b1 being Linear_Combination of V st
for v being VECTOR of V holds b1 . v = i * (L . v)
proof
deffunc H2( Element of V) ->  Element of REAL = 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 = H2(v) from FUNCT_2:sch_4();
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
now__::_thesis:_for_v_being_Element_of_V_st_not_v_in_Carrier_L_holds_
f_._v_=_0
let v be Element of V; ::_thesis: ( not v in Carrier L implies f . v = 0 )
assume  not v in Carrier L ; ::_thesis: f . v = 0
then  L . v = 0 ;
hence f . v = i * 0 by A1
.= 0 ;
::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3;
take  f ; ::_thesis: for v being VECTOR of V holds f . v = i * (L . v)
let v be VECTOR of V; ::_thesis: f . v = i * (L . v)
thus  f . v = i * (L . v) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Linear_Combination of V st ( for v being VECTOR of V holds b1 . v = i * (L . v) ) & ( for v being VECTOR of V holds b2 . v = i * (L . v) ) holds
b1 = b2
proof
let L1, L2 be Linear_Combination of V; ::_thesis: ( ( for v being VECTOR of V holds L1 . v = i * (L . v) ) & ( for v being VECTOR of V holds L2 . v = i * (L . v) ) implies L1 = L2 )
assume that
A2: for v being VECTOR of V holds L1 . v = i * (L . v) and
A3: for v being VECTOR of V holds L2 . v = i * (L . v) ; ::_thesis: L1 = L2
let v be VECTOR of V; :: according to RLVECT_2:def_9 ::_thesis: L1 . v = L2 . v
thus L1 . v = i * (L . v) by A2
.= L2 . v by A3 ; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines * RLVECT_X:def_1_:_
 for V being RealLinearSpace
for i being Integer
for L, b4 being Linear_Combination of V holds
( b4 = i * L iff for v being VECTOR of V holds b4 . v = i * (L . v) );

definition
let V be RealLinearSpace;
let A be Subset of V;
func Z_Lin A ->  Subset of V equals :: RLVECT_X:def 2
 {  (Sum l) where l is Linear_Combination of A : rng l c= INT  }  ;
correctness
coherence
{  (Sum l) where l is Linear_Combination of A : rng l c= INT  }  is Subset of V;
proof
set A1 =  {  (Sum l) where l is Linear_Combination of A : rng l c= INT  }  ;
  {  (Sum l) where l is Linear_Combination of A : rng l c= INT  }  c= the carrier of V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (Sum l) where l is Linear_Combination of A : rng l c= INT  }  or x in the carrier of V )
assume  x in  {  (Sum l) where l is Linear_Combination of A : rng l c= INT  }  ; ::_thesis: x in the carrier of V
then  ex l being Linear_Combination of A st
( x = Sum l & rng l c= INT ) ;
hence  x in the carrier of V ; ::_thesis: verum
end;
hence   {  (Sum l) where l is Linear_Combination of A : rng l c= INT  }  is Subset of V ; ::_thesis: verum
end;
end;

:: deftheorem  defines Z_Lin RLVECT_X:def_2_:_
 for V being RealLinearSpace
for A being Subset of V holds Z_Lin A =  {  (Sum l) where l is Linear_Combination of A : rng l c= INT  }  ;

theorem Th4: :: RLVECT_X:4
for a being Real
for i being Integer
for V being RealLinearSpace
for A being Subset of V
for l being Linear_Combination of A st a = i holds
a * l = i * l
proof
let a be Real; ::_thesis: for i being Integer
for V being RealLinearSpace
for A being Subset of V
for l being Linear_Combination of A st a = i holds
a * l = i * l
let i be Integer; ::_thesis: for V being RealLinearSpace
for A being Subset of V
for l being Linear_Combination of A st a = i holds
a * l = i * l
let V be RealLinearSpace; ::_thesis: for A being Subset of V
for l being Linear_Combination of A st a = i holds
a * l = i * l
let A be Subset of V; ::_thesis: for l being Linear_Combination of A st a = i holds
a * l = i * l
let l be Linear_Combination of A; ::_thesis: ( a = i implies a * l = i * l )
assume A1: a = i ; ::_thesis: a * l = i * l
 for v being VECTOR of V holds (i * l) . v = a * (l . v) by A1, Def1;
hence  a * l = i * l by RLVECT_2:def_11; ::_thesis: verum
end;

theorem Th5: :: RLVECT_X:5
for V being RealLinearSpace
for A being Subset of V
for l1, l2 being Linear_Combination of A st rng l1 c= INT & rng l2 c= INT holds
rng (l1 + l2) c= INT
proof
let V be RealLinearSpace; ::_thesis: for A being Subset of V
for l1, l2 being Linear_Combination of A st rng l1 c= INT & rng l2 c= INT holds
rng (l1 + l2) c= INT
let A be Subset of V; ::_thesis: for l1, l2 being Linear_Combination of A st rng l1 c= INT & rng l2 c= INT holds
rng (l1 + l2) c= INT
let l1, l2 be Linear_Combination of A; ::_thesis: ( rng l1 c= INT & rng l2 c= INT implies rng (l1 + l2) c= INT )
assume A1: ( rng l1 c= INT & rng l2 c= INT ) ; ::_thesis: rng (l1 + l2) c= INT
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (l1 + l2) or y in INT )
assume A2: y in rng (l1 + l2) ; ::_thesis: y in INT
consider x being 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; ::_thesis: verum
end;

theorem Th6: :: RLVECT_X:6
for i being Integer
for V being RealLinearSpace
for A being Subset of V
for l being Linear_Combination of A st rng l c= INT holds
rng (i * l) c= INT
proof
let i be Integer; ::_thesis: for V being RealLinearSpace
for A being Subset of V
for l being Linear_Combination of A st rng l c= INT holds
rng (i * l) c= INT
let V be RealLinearSpace; ::_thesis: for A being Subset of V
for l being Linear_Combination of A st rng l c= INT holds
rng (i * l) c= INT
let A be Subset of V; ::_thesis: for l being Linear_Combination of A st rng l c= INT holds
rng (i * l) c= INT
let l be Linear_Combination of A; ::_thesis: ( rng l c= INT implies rng (i * l) c= INT )
assume A1: rng l c= INT ; ::_thesis: rng (i * l) c= INT
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (i * l) or y in INT )
assume A2: y in rng (i * l) ; ::_thesis: y in INT
consider x being 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; ::_thesis: verum
end;

theorem Th7: :: RLVECT_X:7
for V being RealLinearSpace holds rng (ZeroLC V) c= INT
proof
let V be RealLinearSpace; ::_thesis: rng (ZeroLC V) c= INT
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (ZeroLC V) or y in INT )
assume A1: y in rng (ZeroLC V) ; ::_thesis: y in INT
consider x being 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; ::_thesis: verum
end;

theorem Th8: :: RLVECT_X:8
for V being RealLinearSpace
for A being Subset of V holds Z_Lin A c= the carrier of (Lin A)
proof
let V be RealLinearSpace; ::_thesis: for A being Subset of V holds Z_Lin A c= the carrier of (Lin A)
let A be Subset of V; ::_thesis: Z_Lin A c= the carrier of (Lin A)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Z_Lin A or x in the carrier of (Lin A) )
assume  x in Z_Lin A ; ::_thesis: x in the carrier of (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  x in the carrier of (Lin A) by STRUCT_0:def_5; ::_thesis: verum
end;

theorem Th9: :: RLVECT_X:9
for V being RealLinearSpace
for v, u being VECTOR of V
for A being Subset of V st v in Z_Lin A & u in Z_Lin A holds
v + u in Z_Lin A
proof
let V be RealLinearSpace; ::_thesis: for v, u being VECTOR of V
for A being Subset of V st v in Z_Lin A & u in Z_Lin A holds
v + u in Z_Lin A
let v, u be VECTOR of V; ::_thesis: for A being Subset of V st v in Z_Lin A & u in Z_Lin A holds
v + u in Z_Lin A
let A be Subset of V; ::_thesis: ( v in Z_Lin A & u in Z_Lin A implies v + u in Z_Lin A )
assume that
A1: v in Z_Lin A and
A2: u in Z_Lin A ; ::_thesis: v + 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  v + u in Z_Lin A by A5; ::_thesis: verum
end;

theorem Th10: :: RLVECT_X:10
for i being Integer
for V being RealLinearSpace
for v being VECTOR of V
for A being Subset of V st v in Z_Lin A holds
i * v in Z_Lin A
proof
let i be Integer; ::_thesis: for V being RealLinearSpace
for v being VECTOR of V
for A being Subset of V st v in Z_Lin A holds
i * v in Z_Lin A
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V
for A being Subset of V st v in Z_Lin A holds
i * v in Z_Lin A
let v be VECTOR of V; ::_thesis: for A being Subset of V st v in Z_Lin A holds
i * v in Z_Lin A
let A be Subset of V; ::_thesis: ( v in Z_Lin A implies i * v in Z_Lin A )
assume  v in Z_Lin A ; ::_thesis: i * v in Z_Lin A
then consider l being Linear_Combination of A 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  i * v in Z_Lin A by A3; ::_thesis: verum
end;

theorem Th11: :: RLVECT_X:11
for V being RealLinearSpace
for A being Subset of V holds 0. V in Z_Lin A
proof
let V be RealLinearSpace; ::_thesis: for A being Subset of V holds 0. V in Z_Lin A
let A be Subset of V; ::_thesis: 0. V in Z_Lin A
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  0. V in Z_Lin A by A1; ::_thesis: verum
end;

theorem Th12: :: RLVECT_X:12
for x being set
for V being RealLinearSpace
for A being Subset of V st x in A holds
x in Z_Lin A
proof
let x be set ; ::_thesis: for V being RealLinearSpace
for A being Subset of V st x in A holds
x in Z_Lin A
let V be RealLinearSpace; ::_thesis: for A being Subset of V st x in A holds
x in Z_Lin A
let A be Subset of V; ::_thesis: ( x in A implies x in Z_Lin A )
assume A1: x in A ; ::_thesis: x in Z_Lin 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 being VECTOR of V st u <> v holds
f . u = H1(u) from FUNCT_2:sch_6();
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
 ex T being finite Subset of V st
for u being VECTOR of V st not u in T holds
f . u = 0
proof
take T = {v}; ::_thesis: for u being VECTOR of V st not u in T holds
f . u = 0
let u be VECTOR of V; ::_thesis: ( not u in T implies f . u = 0 )
assume  not u in T ; ::_thesis: f . u = 0
then  u <> v by TARSKI:def_1;
hence  f . u = 0 by A3; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3;
A4: Carrier f c= {v}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v} )
assume  x in Carrier f ; ::_thesis: x in {v}
then consider u being VECTOR of V such that
A5: x = u and
A6: f . u <> 0 ;
 u = v by A3, A6;
hence  x in {v} by A5, TARSKI:def_1; ::_thesis: verum
end;
then reconsider f = 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 = f as Linear_Combination of A by RLVECT_2:def_6;
 rng f c= INT
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in INT )
assume A8: y in rng f ; ::_thesis: y in INT
consider x being 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;
percases ( z <> v or z = v ) ;
suppose z <> v ; ::_thesis: y in INT
then  f . z = 0 by A3;
hence  y in INT by A9, NUMBERS:17, TARSKI:def_3; ::_thesis: verum
end;
suppose z = v ; ::_thesis: y in INT
hence  y in INT by A9, A2, NUMBERS:17, TARSKI:def_3; ::_thesis: verum
end;
end;
end;
hence  x in Z_Lin A by A7; ::_thesis: verum
end;

theorem Th13: :: RLVECT_X:13
for V being RealLinearSpace
for A, B being Subset of V st A c= B holds
Z_Lin A c= Z_Lin B
proof
let V be RealLinearSpace; ::_thesis: for A, B being Subset of V st A c= B holds
Z_Lin A c= Z_Lin B
let A, B be Subset of V; ::_thesis: ( A c= B implies Z_Lin A c= Z_Lin B )
assume A1: A c= B ; ::_thesis: Z_Lin A c= Z_Lin B
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in Z_Lin A or v in Z_Lin B )
assume  v in Z_Lin A ; ::_thesis: v in Z_Lin B
then consider l being Linear_Combination of A such that
A2: ( v = Sum l & rng l c= INT ) ;
reconsider l = l as Linear_Combination of B by A1, RLVECT_2:21;
 Sum l = v by A2;
hence  v in Z_Lin B by A2; ::_thesis: verum
end;

theorem :: RLVECT_X:14
for V being RealLinearSpace
for A, B being Subset of V holds Z_Lin (A \/ B) = (Z_Lin A) + (Z_Lin B)
proof
let V be RealLinearSpace; ::_thesis: for A, B being Subset of V holds Z_Lin (A \/ B) = (Z_Lin A) + (Z_Lin B)
let A, B be Subset of V; ::_thesis: Z_Lin (A \/ B) = (Z_Lin A) + (Z_Lin B)
now__::_thesis:_for_v_being_set_st_v_in_Z_Lin_(A_\/_B)_holds_
v_in_(Z_Lin_A)_+_(Z_Lin_B)
let v be set ; ::_thesis: ( v in Z_Lin (A \/ B) implies v in (Z_Lin A) + (Z_Lin B) )
assume  v in Z_Lin (A \/ B) ; ::_thesis: v in (Z_Lin A) + (Z_Lin B)
then consider l being Linear_Combination of A \/ B such that
A1: ( v = Sum l & rng l c= INT ) ;
deffunc H2( set ) ->  Element of REAL = l . $1;
set D = (Carrier l) \ A;
set C = (Carrier l) /\ A;
defpred S1[ set ] means $1 in (Carrier l) /\ A;
defpred S2[ set ] means $1 in (Carrier l) \ A;
A2: for x being set st x in the carrier of V holds
( ( S1[x] implies H2(x) in REAL ) & ( not S1[x] implies H1(x) in REAL ) ) ;
consider f being Function of the carrier of V,REAL such that
A3: for x being set st x in the carrier of V holds
( ( S1[x] implies f . x = H2(x) ) & ( not S1[x] implies f . x = H1(x) ) ) from FUNCT_2:sch_5(A2);
reconsider C = (Carrier l) /\ A as finite Subset of V ;
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
 for u being VECTOR of V st not u in C holds
f . u = 0 by A3;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3;
A4: rng f c= INT
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in INT )
assume A5: y in rng f ; ::_thesis: y in INT
consider x being 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;
percases ( not z in C or z in C ) ;
suppose not z in C ; ::_thesis: y in INT
then  f . z = 0 by A3;
hence  y in INT by A6, NUMBERS:17, TARSKI:def_3; ::_thesis: verum
end;
suppose z in C ; ::_thesis: y in INT
then  f . z = l . z by A3;
then  f . z in rng l by FUNCT_2:4;
hence  y in INT by A6, A1; ::_thesis: verum
end;
end;
end;
A7: Carrier f c= C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in C )
assume  x in Carrier f ; ::_thesis: x in C
then A8: ex u being VECTOR of V st
( x = u & f . u <> 0 ) ;
assume  not x in C ; ::_thesis: contradiction
hence  contradiction by A3, A8; ::_thesis: verum
end;
 C c= A by XBOOLE_1:17;
then  Carrier f c= A by A7, XBOOLE_1:1;
then reconsider f = f as Linear_Combination of A by RLVECT_2:def_6;
A9: for x being set st x in the carrier of V holds
( ( S2[x] implies H2(x) in REAL ) & ( not S2[x] implies H1(x) in REAL ) ) ;
consider g being Function of the carrier of V,REAL such that
A10: for x being set st x in the carrier of V holds
( ( S2[x] implies g . x = H2(x) ) & ( not S2[x] implies g . x = H1(x) ) ) from FUNCT_2:sch_5(A9);
reconsider D = (Carrier l) \ A as finite Subset of V ;
reconsider g = g as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
 for u being VECTOR of V st not u in D holds
g . u = 0 by A10;
then reconsider g = g as Linear_Combination of V by RLVECT_2:def_3;
A11: rng g c= INT
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in INT )
assume A12: y in rng g ; ::_thesis: y in INT
consider x being 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;
percases ( not z in D or z in D ) ;
suppose not z in D ; ::_thesis: y in INT
then  g . z = 0 by A10;
hence  y in INT by A13, NUMBERS:17, TARSKI:def_3; ::_thesis: verum
end;
suppose z in D ; ::_thesis: y in INT
then  g . z = l . z by A10;
then  g . z in rng l by FUNCT_2:4;
hence  y in INT by A13, A1; ::_thesis: verum
end;
end;
end;
A14: D c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in B )
assume  x in D ; ::_thesis: x in B
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  x in B by A15, XBOOLE_0:def_3; ::_thesis: verum
end;
 Carrier g c= D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier g or x in D )
assume  x in Carrier g ; ::_thesis: x in D
then A16: ex u being VECTOR of V st
( x = u & g . u <> 0 ) ;
assume  not x in D ; ::_thesis: contradiction
hence  contradiction by A10, A16; ::_thesis: verum
end;
then  Carrier g c= B by A14, XBOOLE_1:1;
then reconsider g = g as Linear_Combination of B by RLVECT_2:def_6;
 l = f + g
proof
let v be VECTOR of V; :: according to RLVECT_2:def_9 ::_thesis: l . v = (f + g) . v
now__::_thesis:_(f_+_g)_._v_=_l_._v
percases ( v in C or not v in C ) ;
supposeA17: v in C ; ::_thesis: (f + g) . v = l . v
A18: now__::_thesis:_not_v_in_D
assume  v in D ; ::_thesis: contradiction
then  not v in A by XBOOLE_0:def_5;
hence  contradiction by A17, XBOOLE_0:def_4; ::_thesis: verum
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 ; ::_thesis: verum
end;
supposeA19: not v in C ; ::_thesis: l . v = (f + g) . v
now__::_thesis:_(f_+_g)_._v_=_l_._v
percases ( v in Carrier l or not v in Carrier l ) ;
supposeA20: v in Carrier l ; ::_thesis: (f + g) . v = l . v
A21: now__::_thesis:_v_in_D
assume  not v in D ; ::_thesis: contradiction
then  ( not v in Carrier l or v in A ) by XBOOLE_0:def_5;
hence  contradiction by A19, A20, XBOOLE_0:def_4; ::_thesis: verum
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 ; ::_thesis: verum
end;
supposeA22: not v in Carrier l ; ::_thesis: (f + g) . v = l . v
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 ; ::_thesis: verum
end;
end;
end;
hence  l . v = (f + g) . v ; ::_thesis: verum
end;
end;
end;
hence  l . v = (f + g) . v ; ::_thesis: verum
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; ::_thesis: verum
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__::_thesis:_for_x_being_set_st_x_in_(Z_Lin_A)_+_(Z_Lin_B)_holds_
x_in_Z_Lin_(A_\/_B)
let x be set ; ::_thesis: ( x in (Z_Lin A) + (Z_Lin B) implies x in Z_Lin (A \/ B) )
assume  x in (Z_Lin A) + (Z_Lin B) ; ::_thesis: x in Z_Lin (A \/ B)
then consider u, v being 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; ::_thesis: verum
end;
then  (Z_Lin A) + (Z_Lin B) c= Z_Lin (A \/ B) by TARSKI:def_3;
hence  Z_Lin (A \/ B) = (Z_Lin A) + (Z_Lin B) by A26, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: RLVECT_X:15
for V being RealLinearSpace
for A, B being Subset of V holds Z_Lin (A /\ B) c= (Z_Lin A) /\ (Z_Lin B)
proof
let V be RealLinearSpace; ::_thesis: for A, B being Subset of V holds Z_Lin (A /\ B) c= (Z_Lin A) /\ (Z_Lin B)
let A, B be Subset of V; ::_thesis: Z_Lin (A /\ B) c= (Z_Lin A) /\ (Z_Lin B)
 ( Z_Lin (A /\ B) c= Z_Lin A & Z_Lin (A /\ B) c= Z_Lin B ) by Th13, XBOOLE_1:17;
hence  Z_Lin (A /\ B) c= (Z_Lin A) /\ (Z_Lin B) by XBOOLE_1:19; ::_thesis: verum
end;

theorem Th16: :: RLVECT_X:16
for x being set
for V being RealLinearSpace
for v being VECTOR of V holds
( x in Z_Lin {v} iff ex a being Integer st x = a * v )
proof
let x be set ; ::_thesis: for V being RealLinearSpace
for v being VECTOR of V holds
( x in Z_Lin {v} iff ex a being Integer st x = a * v )
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V holds
( x in Z_Lin {v} iff ex a being Integer st x = a * v )
let v be VECTOR of V; ::_thesis: ( x in Z_Lin {v} iff ex a being Integer st x = a * v )
thus  ( x in Z_Lin {v} implies ex a being Integer st x = a * v ) ::_thesis: ( ex a being Integer st x = a * v implies x in Z_Lin {v} )
proof
assume  x in Z_Lin {v} ; ::_thesis: ex a being Integer st x = a * 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  ex a being Integer st x = a * v by A1, A2; ::_thesis: verum
end;
given a0 being Integer such that A3: x = a0 * v ; ::_thesis: x in Z_Lin {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 = H1(z) from FUNCT_2:sch_6();
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
A6: now__::_thesis:_for_z_being_VECTOR_of_V_st_not_z_in_{v}_holds_
f_._z_=_0
let z be VECTOR of V; ::_thesis: ( not z in {v} implies f . z = 0 )
assume  not z in {v} ; ::_thesis: f . z = 0
then  z <> v by TARSKI:def_1;
hence  f . z = 0 by A5; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3;
 Carrier f c= {v}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v} )
assume A7: x in Carrier f ; ::_thesis: x in {v}
then  f . x <> 0 by RLVECT_2:19;
then  x = v by A5, A7;
hence  x in {v} by TARSKI:def_1; ::_thesis: verum
end;
then reconsider f = 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 ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in INT )
assume A9: y in rng f ; ::_thesis: y in INT
consider x being 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;
percases ( not z in {v} or z in {v} ) ;
suppose not z in {v} ; ::_thesis: y in INT
then  f . z = 0 by A6;
hence  y in INT by A10, NUMBERS:17, TARSKI:def_3; ::_thesis: verum
end;
suppose z in {v} ; ::_thesis: y in INT
then  f . z = a0 by A4, TARSKI:def_1;
hence  y in INT by A10, INT_1:def_2; ::_thesis: verum
end;
end;
end;
hence  x in Z_Lin {v} by A8; ::_thesis: verum
end;

theorem :: RLVECT_X:17
for V being RealLinearSpace
for v being VECTOR of V holds v in Z_Lin {v}
proof
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V holds v in Z_Lin {v}
let v be VECTOR of V; ::_thesis: v in Z_Lin {v}
 v in {v} by TARSKI:def_1;
hence  v in Z_Lin {v} by Th12; ::_thesis: verum
end;

theorem :: RLVECT_X:18
for x being set
for V being RealLinearSpace
for v, w being VECTOR of V holds
( x in v + (Z_Lin {w}) iff ex a being Integer st x = v + (a * w) )
proof
let x be set ; ::_thesis: for V being RealLinearSpace
for v, w being VECTOR of V holds
( x in v + (Z_Lin {w}) iff ex a being Integer st x = v + (a * w) )
let V be RealLinearSpace; ::_thesis: for v, w being VECTOR of V holds
( x in v + (Z_Lin {w}) iff ex a being Integer st x = v + (a * w) )
let v, w be VECTOR of V; ::_thesis: ( x in v + (Z_Lin {w}) iff ex a being Integer st x = v + (a * w) )
thus  ( x in v + (Z_Lin {w}) implies ex a being Integer st x = v + (a * w) ) ::_thesis: ( ex a being Integer st x = v + (a * w) implies x in v + (Z_Lin {w}) )
proof
assume  x in v + (Z_Lin {w}) ; ::_thesis: ex a being Integer st x = v + (a * w)
then consider u being VECTOR of V such that
A1: x = v + u and
A2: u in Z_Lin {w} ;
 ex a being Integer st u = a * w by A2, Th16;
hence  ex a being Integer st x = v + (a * w) by A1; ::_thesis: verum
end;
given a0 being Integer such that A3: x = v + (a0 * w) ; ::_thesis: x in v + (Z_Lin {w})
 a0 * w in Z_Lin {w} by Th16;
hence  x in v + (Z_Lin {w}) by A3; ::_thesis: verum
end;

theorem Th19: :: RLVECT_X:19
for x being set
for V being RealLinearSpace
for w1, w2 being VECTOR of V holds
( x in Z_Lin {w1,w2} iff ex a, b being Integer st x = (a * w1) + (b * w2) )
proof
let x be set ; ::_thesis: for V being RealLinearSpace
for w1, w2 being VECTOR of V holds
( x in Z_Lin {w1,w2} iff ex a, b being Integer st x = (a * w1) + (b * w2) )
let V be RealLinearSpace; ::_thesis: for w1, w2 being VECTOR of V holds
( x in Z_Lin {w1,w2} iff ex a, b being Integer st x = (a * w1) + (b * w2) )
let w1, w2 be VECTOR of V; ::_thesis: ( x in Z_Lin {w1,w2} iff ex a, b being Integer st x = (a * w1) + (b * w2) )
thus  ( x in Z_Lin {w1,w2} implies ex a, b being Integer st x = (a * w1) + (b * w2) ) ::_thesis: ( ex a, b being Integer st x = (a * w1) + (b * w2) implies x in Z_Lin {w1,w2} )
proof
assume A1: x in Z_Lin {w1,w2} ; ::_thesis: ex a, b being Integer st x = (a * w1) + (b * w2)
now__::_thesis:_ex_a,_b_being_Integer_st_x_=_(a_*_w1)_+_(b_*_w2)
percases ( w1 = w2 or w1 <> w2 ) ;
suppose w1 = w2 ; ::_thesis: ex a, b being Integer st x = (a * w1) + (b * w2)
then  {w1,w2} = {w1} by ENUMSET1:29;
then consider a being Integer such that
A2: x = a * w1 by A1, Th16;
consider b being 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  ex a, b being Integer st x = (a * w1) + (b * w2) ; ::_thesis: verum
end;
supposeA4: w1 <> w2 ; ::_thesis: ex a, b being Integer st x = (a * w1) + (b * 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  ex a, b being Integer st x = (a * w1) + (b * w2) by A5, A6; ::_thesis: verum
end;
end;
end;
hence  ex a, b being Integer st x = (a * w1) + (b * w2) ; ::_thesis: verum
end;
given a0, b0 being Integer such that A7: x = (a0 * w1) + (b0 * w2) ; ::_thesis: x in Z_Lin {w1,w2}
reconsider a = a0, b = b0 as Real by XREAL_0:def_1;
now__::_thesis:_x_in_Z_Lin_{w1,w2}
percases ( w1 = w2 or w1 <> w2 ) ;
supposeA8: w1 = w2 ; ::_thesis: x in Z_Lin {w1,w2}
then  x = (a + b) * w1 by A7, RLVECT_1:def_6;
then  x in Z_Lin {w1} by Th16;
hence  x in Z_Lin {w1,w2} by A8, ENUMSET1:29; ::_thesis: verum
end;
supposeA9: w1 <> w2 ; ::_thesis: x in Z_Lin {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 being VECTOR of V st u <> w1 & u <> w2 holds
f . u = H1(u) from FUNCT_2:sch_7(A9);
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
A12: now__::_thesis:_for_u_being_VECTOR_of_V_st_not_u_in_{w1,w2}_holds_
f_._u_=_0
let u be VECTOR of V; ::_thesis: ( not u in {w1,w2} implies f . u = 0 )
assume  not u in {w1,w2} ; ::_thesis: f . u = 0
then  ( u <> w1 & u <> w2 ) by TARSKI:def_2;
hence  f . u = 0 by A11; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3;
 Carrier f c= {w1,w2}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {w1,w2} )
assume that
A13: x in Carrier f and
A14: not x in {w1,w2} ; ::_thesis: contradiction
 ( x <> w1 & x <> w2 ) by A14, TARSKI:def_2;
then  f . x = 0 by A11, A13;
hence  contradiction by A13, RLVECT_2:19; ::_thesis: verum
end;
then reconsider f = 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 ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in INT )
assume A16: y in rng f ; ::_thesis: y in INT
consider x being 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;
percases ( not v in {w1,w2} or v in {w1,w2} ) ;
suppose not v in {w1,w2} ; ::_thesis: y in INT
then  f . v = 0 by A12;
hence  y in INT by A17, NUMBERS:17, TARSKI:def_3; ::_thesis: verum
end;
suppose v in {w1,w2} ; ::_thesis: y in INT
then  ( f . v = a0 or f . v = b0 ) by A10, TARSKI:def_2;
hence  y in INT by A17, INT_1:def_2; ::_thesis: verum
end;
end;
end;
hence  x in Z_Lin {w1,w2} by A15; ::_thesis: verum
end;
end;
end;
hence  x in Z_Lin {w1,w2} ; ::_thesis: verum
end;

theorem :: RLVECT_X:20
for V being RealLinearSpace
for w1, w2 being VECTOR of V holds w1 in Z_Lin {w1,w2}
proof
let V be RealLinearSpace; ::_thesis: for w1, w2 being VECTOR of V holds w1 in Z_Lin {w1,w2}
let w1, w2 be VECTOR of V; ::_thesis: w1 in Z_Lin {w1,w2}
 w1 in {w1,w2} by TARSKI:def_2;
hence  w1 in Z_Lin {w1,w2} by Th12; ::_thesis: verum
end;

theorem :: RLVECT_X:21
for x being set
for V being RealLinearSpace
for v, w1, w2 being VECTOR of V holds
( x in v + (Z_Lin {w1,w2}) iff ex a, b being Integer st x = (v + (a * w1)) + (b * w2) )
proof
let x be set ; ::_thesis: for V being RealLinearSpace
for v, w1, w2 being VECTOR of V holds
( x in v + (Z_Lin {w1,w2}) iff ex a, b being Integer st x = (v + (a * w1)) + (b * w2) )
let V be RealLinearSpace; ::_thesis: for v, w1, w2 being VECTOR of V holds
( x in v + (Z_Lin {w1,w2}) iff ex a, b being Integer st x = (v + (a * w1)) + (b * w2) )
let v, w1, w2 be VECTOR of V; ::_thesis: ( x in v + (Z_Lin {w1,w2}) iff ex a, b being Integer st x = (v + (a * w1)) + (b * w2) )
thus  ( x in v + (Z_Lin {w1,w2}) implies ex a, b being Integer st x = (v + (a * w1)) + (b * w2) ) ::_thesis: ( ex a, b being Integer st x = (v + (a * w1)) + (b * w2) implies x in v + (Z_Lin {w1,w2}) )
proof
assume  x in v + (Z_Lin {w1,w2}) ; ::_thesis: ex a, b being Integer st x = (v + (a * w1)) + (b * w2)
then consider u being VECTOR of V such that
A1: x = v + u and
A2: u in Z_Lin {w1,w2} ;
consider a, b being Integer such that
A3: u = (a * w1) + (b * w2) by A2, Th19;
take  a ; ::_thesis: ex b being Integer st x = (v + (a * w1)) + (b * w2)
take  b ; ::_thesis: x = (v + (a * w1)) + (b * w2)
thus  x = (v + (a * w1)) + (b * w2) by A1, A3, RLVECT_1:def_3; ::_thesis: verum
end;
given a, b being Integer such that A4: x = (v + (a * w1)) + (b * w2) ; ::_thesis: x in v + (Z_Lin {w1,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  x in v + (Z_Lin {w1,w2}) by A4, RLVECT_1:def_3; ::_thesis: verum
end;

theorem Th22: :: RLVECT_X:22
for x being set
for V being RealLinearSpace
for v1, v2, v3 being VECTOR of V holds
( x in Z_Lin {v1,v2,v3} iff ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3) )
proof
let x be set ; ::_thesis: for V being RealLinearSpace
for v1, v2, v3 being VECTOR of V holds
( x in Z_Lin {v1,v2,v3} iff ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3) )
let V be RealLinearSpace; ::_thesis: for v1, v2, v3 being VECTOR of V holds
( x in Z_Lin {v1,v2,v3} iff ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3) )
let v1, v2, v3 be VECTOR of V; ::_thesis: ( x in Z_Lin {v1,v2,v3} iff ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3) )
thus  ( x in Z_Lin {v1,v2,v3} implies ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3) ) ::_thesis: ( ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3) implies x in Z_Lin {v1,v2,v3} )
proof
assume A1: x in Z_Lin {v1,v2,v3} ; ::_thesis: ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3)
now__::_thesis:_ex_a,_b,_c_being_Integer_st_x_=_((a_*_v1)_+_(b_*_v2))_+_(c_*_v3)
percases ( ( v1 <> v2 & v1 <> v3 & v2 <> v3 ) or v1 = v2 or v1 = v3 or v2 = v3 ) ;
supposeA2: ( v1 <> v2 & v1 <> v3 & v2 <> v3 ) ; ::_thesis: ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * 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  ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3) by A3, A4; ::_thesis: verum
end;
suppose ( v1 = v2 or v1 = v3 or v2 = v3 ) ; ::_thesis: ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * 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, ENUMSET1:59;
now__::_thesis:_ex_a,_b,_c_being_Integer_st_x_=_((a_*_v1)_+_(b_*_v2))_+_(c_*_v3)
percases ( {v1,v2,v3} = {v1,v2} or {v1,v2,v3} = {v1,v3} ) by A5, ENUMSET1:30;
suppose {v1,v2,v3} = {v1,v2} ; ::_thesis: ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3)
then consider a, b being Integer such that
A6: x = (a * v1) + (b * v2) by A1, Th19;
consider c being 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  ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3) ; ::_thesis: verum
end;
suppose {v1,v2,v3} = {v1,v3} ; ::_thesis: ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3)
then consider a, b being Integer such that
A8: x = (a * v1) + (b * v3) by A1, Th19;
consider c being 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  ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3) ; ::_thesis: verum
end;
end;
end;
hence  ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3) ; ::_thesis: verum
end;
end;
end;
hence  ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3) ; ::_thesis: verum
end;
given a0, b0, c0 being Integer such that A10: x = ((a0 * v1) + (b0 * v2)) + (c0 * v3) ; ::_thesis: x in Z_Lin {v1,v2,v3}
reconsider a = a0, b = b0, c = c0 as Real by XREAL_0:def_1;
now__::_thesis:_x_in_Z_Lin_{v1,v2,v3}
percases ( v1 = v2 or v1 = v3 or v2 = v3 or ( v1 <> v2 & v1 <> v3 & v2 <> v3 ) ) ;
supposeA11: ( v1 = v2 or v1 = v3 or v2 = v3 ) ; ::_thesis: x in Z_Lin {v1,v2,v3}
now__::_thesis:_x_in_Z_Lin_{v1,v2,v3}
percases ( v1 = v2 or v1 = v3 or v2 = v3 ) by A11;
suppose v1 = v2 ; ::_thesis: x in Z_Lin {v1,v2,v3}
then  ( {v1,v2,v3} = {v1,v3} & x = ((a + b) * v1) + (c * v3) ) by A10, ENUMSET1:30, RLVECT_1:def_6;
hence  x in Z_Lin {v1,v2,v3} by Th19; ::_thesis: verum
end;
supposeA12: v1 = v3 ; ::_thesis: x in Z_Lin {v1,v2,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  x in Z_Lin {v1,v2,v3} by A13, Th19; ::_thesis: verum
end;
supposeA14: v2 = v3 ; ::_thesis: x in Z_Lin {v1,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  x in Z_Lin {v1,v2,v3} by A15, Th19; ::_thesis: verum
end;
end;
end;
hence  x in Z_Lin {v1,v2,v3} ; ::_thesis: verum
end;
supposeA16: ( v1 <> v2 & v1 <> v3 & v2 <> v3 ) ; ::_thesis: x in Z_Lin {v1,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 being VECTOR of V st v <> v1 & v <> v2 & v <> v3 holds
f . v = H1(v) from RLVECT_4:sch_1(A19, A17, A18);
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
A22: now__::_thesis:_for_v_being_VECTOR_of_V_st_not_v_in_{v1,v2,v3}_holds_
f_._v_=_0
let v be VECTOR of V; ::_thesis: ( not v in {v1,v2,v3} implies f . v = 0 )
assume A23: not v in {v1,v2,v3} ; ::_thesis: f . v = 0
then A24: v <> v3 by ENUMSET1:def_1;
 ( v <> v1 & v <> v2 ) by A23, ENUMSET1:def_1;
hence  f . v = 0 by A21, A24; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3;
 Carrier f c= {v1,v2,v3}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v1,v2,v3} )
assume that
A25: x in Carrier f and
A26: not x in {v1,v2,v3} ; ::_thesis: contradiction
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  contradiction by A25, RLVECT_2:19; ::_thesis: verum
end;
then reconsider f = 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 ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in INT )
assume A29: y in rng f ; ::_thesis: y in INT
consider x being 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;
percases ( not v in {v1,v2,v3} or v in {v1,v2,v3} ) ;
suppose not v in {v1,v2,v3} ; ::_thesis: y in INT
then  f . v = 0 by A22;
hence  y in INT by A30, NUMBERS:17, TARSKI:def_3; ::_thesis: verum
end;
suppose v in {v1,v2,v3} ; ::_thesis: y in INT
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; ::_thesis: verum
end;
end;
end;
hence  x in Z_Lin {v1,v2,v3} by A28; ::_thesis: verum
end;
end;
end;
hence  x in Z_Lin {v1,v2,v3} ; ::_thesis: verum
end;

theorem :: RLVECT_X:23
for V being RealLinearSpace
for w1, w2, w3 being VECTOR of V holds
( w1 in Z_Lin {w1,w2,w3} & w2 in Z_Lin {w1,w2,w3} & w3 in Z_Lin {w1,w2,w3} )
proof
let V be RealLinearSpace; ::_thesis: for w1, w2, w3 being VECTOR of V holds
( w1 in Z_Lin {w1,w2,w3} & w2 in Z_Lin {w1,w2,w3} & w3 in Z_Lin {w1,w2,w3} )
let w1, w2, w3 be VECTOR of V; ::_thesis: ( w1 in Z_Lin {w1,w2,w3} & w2 in Z_Lin {w1,w2,w3} & w3 in Z_Lin {w1,w2,w3} )
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  ( w1 in Z_Lin {w1,w2,w3} & w2 in Z_Lin {w1,w2,w3} & w3 in Z_Lin {w1,w2,w3} ) by A1, Th12; ::_thesis: verum
end;

theorem :: RLVECT_X:24
for x being set
for V being RealLinearSpace
for v, w1, w2, w3 being VECTOR of V holds
( x in v + (Z_Lin {w1,w2,w3}) iff ex a, b, c being Integer st x = ((v + (a * w1)) + (b * w2)) + (c * w3) )
proof
let x be set ; ::_thesis: for V being RealLinearSpace
for v, w1, w2, w3 being VECTOR of V holds
( x in v + (Z_Lin {w1,w2,w3}) iff ex a, b, c being Integer st x = ((v + (a * w1)) + (b * w2)) + (c * w3) )
let V be RealLinearSpace; ::_thesis: for v, w1, w2, w3 being VECTOR of V holds
( x in v + (Z_Lin {w1,w2,w3}) iff ex a, b, c being Integer st x = ((v + (a * w1)) + (b * w2)) + (c * w3) )
let v, w1, w2, w3 be VECTOR of V; ::_thesis: ( x in v + (Z_Lin {w1,w2,w3}) iff ex a, b, c being Integer st x = ((v + (a * w1)) + (b * w2)) + (c * w3) )
thus  ( x in v + (Z_Lin {w1,w2,w3}) implies ex a, b, c being Integer st x = ((v + (a * w1)) + (b * w2)) + (c * w3) ) ::_thesis: ( ex a, b, c being Integer st x = ((v + (a * w1)) + (b * w2)) + (c * w3) implies x in v + (Z_Lin {w1,w2,w3}) )
proof
assume  x in v + (Z_Lin {w1,w2,w3}) ; ::_thesis: ex a, b, c being Integer st x = ((v + (a * w1)) + (b * w2)) + (c * w3)
then consider u being VECTOR of V such that
A1: x = v + u and
A2: u in Z_Lin {w1,w2,w3} ;
consider a, b, c being Integer such that
A3: u = ((a * w1) + (b * w2)) + (c * w3) by A2, Th22;
take  a ; ::_thesis: ex b, c being Integer st x = ((v + (a * w1)) + (b * w2)) + (c * w3)
take  b ; ::_thesis: ex c being Integer st x = ((v + (a * w1)) + (b * w2)) + (c * w3)
take  c ; ::_thesis: x = ((v + (a * w1)) + (b * w2)) + (c * w3)
 x = (v + ((a * w1) + (b * w2))) + (c * w3) by A1, A3, RLVECT_1:def_3;
hence  x = ((v + (a * w1)) + (b * w2)) + (c * w3) by RLVECT_1:def_3; ::_thesis: verum
end;
given a, b, c being Integer such that A4: x = ((v + (a * w1)) + (b * w2)) + (c * w3) ; ::_thesis: x in v + (Z_Lin {w1,w2,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  x in v + (Z_Lin {w1,w2,w3}) by A4, RLVECT_1:def_3; ::_thesis: verum
end;

Lm1:  for RS being RealLinearSpace
for X being Subset of RS
for g1, h1 being FinSequence of RS
for a1 being INT -valued FinSequence st rng g1 c= X & len g1 = len h1 & len g1 = len a1 & ( for i being 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; ::_thesis: for X being Subset of RS
for g1, h1 being FinSequence of RS
for a1 being INT -valued FinSequence st rng g1 c= X & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) holds
Sum h1 in Z_Lin X
let X be Subset of RS; ::_thesis: for g1, h1 being FinSequence of RS
for a1 being INT -valued FinSequence st rng g1 c= X & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) holds
Sum h1 in Z_Lin X
defpred S1[ Nat] means  for g, h being FinSequence of RS
for s being INT -valued FinSequence st rng g c= X & len g = $1 & len g = len h & len g = len s & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) holds
Sum h in Z_Lin X;
A1: S1[ 0 ]
proof
let g, h be FinSequence of RS; ::_thesis: for s being INT -valued FinSequence st rng g c= X & len g = 0 & len g = len h & len g = len s & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) holds
Sum h in Z_Lin X
let s be INT -valued FinSequence; ::_thesis: ( rng g c= X & len g = 0 & len g = len h & len g = len s & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) implies Sum h in Z_Lin X )
set x = Sum h;
assume A2: ( rng g c= X & len g = 0 & len g = len h & len g = len s & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) ) ; ::_thesis: Sum h in Z_Lin X
Sum h = Sum (<*> the carrier of RS) by A2, FINSEQ_1:20
.= 0. RS by RLVECT_1:43 ;
hence  Sum h in Z_Lin X by Th11; ::_thesis: verum
end;
A3: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; ::_thesis: S1[n + 1]
now__::_thesis:_for_g,_h_being_FinSequence_of_RS
for_s_being_INT_-valued_FinSequence
for_x_being_set_st_x_=_Sum_h_&_rng_g_c=_X_&_len_g_=_n_+_1_&_len_g_=_len_h_&_len_g_=_len_s_&_(_for_i_being_Nat_st_i_in_Seg_(len_g)_holds_
h_/._i_=_(s_._i)_*_(g_/._i)_)_holds_
x_in_Z_Lin_X
let g, h be FinSequence of RS; ::_thesis: for s being INT -valued FinSequence
for x being set st x = Sum h & rng g c= X & len g = n + 1 & len g = len h & len g = len s & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) holds
x in Z_Lin X
let s be INT -valued FinSequence; ::_thesis: for x being set st x = Sum h & rng g c= X & len g = n + 1 & len g = len h & len g = len s & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) holds
x in Z_Lin X
let x be set ; ::_thesis: ( x = Sum h & rng g c= X & len g = n + 1 & len g = len h & len g = len s & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) implies x in Z_Lin X )
assume A5: ( x = Sum h & rng g c= X & len g = n + 1 & len g = len h & len g = len s & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) ) ; ::_thesis: x in Z_Lin X
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 being 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 being Nat st i in Seg (len gn) holds
hn /. i = (sn . i) * (gn /. i)
proof
percases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; ::_thesis: for i being Nat st i in Seg (len gn) holds
hn /. i = (sn . i) * (gn /. i)
hence  for i being Nat st i in Seg (len gn) holds
hn /. i = (sn . i) * (gn /. i) ; ::_thesis: verum
end;
suppose n <> 0 ; ::_thesis: for i being Nat st i in Seg (len gn) holds
hn /. i = (sn . i) * (gn /. i)
then A11: n >= 1 by NAT_1:14;
let i be Nat; ::_thesis: ( i in Seg (len gn) implies hn /. i = (sn . i) * (gn /. i) )
assume  i in Seg (len gn) ; ::_thesis: hn /. i = (sn . i) * (gn /. i)
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  hn /. i = (sn . i) * (gn /. i) by A5, A12, A13, A14, FINSEQ_2:8; ::_thesis: verum
end;
end;
end;
hence  ( rng gn c= X & len gn = n & len gn = len hn & len gn = len sn & ( for i being Nat st i in Seg (len gn) holds
hn /. i = (sn . i) * (gn /. i) ) ) by A6, A9, A10, A5, FINSEQ_1:59, NAT_1:11; ::_thesis: verum
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; ::_thesis: verum
end;
hence  S1[n + 1] ; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A1, A3);
hence  for g1, h1 being FinSequence of RS
for a1 being INT -valued FinSequence st rng g1 c= X & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) holds
Sum h1 in Z_Lin X ; ::_thesis: verum
end;

Lm2:  for V being RealLinearSpace
for A being Subset of V
for x being set st x in Z_Lin A holds
ex g1, h1 being FinSequence of V ex a1 being INT -valued FinSequence st
( x = Sum h1 & rng g1 c= A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) )
proof
let V be RealLinearSpace; ::_thesis: for A being Subset of V
for x being set st x in Z_Lin A holds
ex g1, h1 being FinSequence of V ex a1 being INT -valued FinSequence st
( x = Sum h1 & rng g1 c= A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) )
let A be Subset of V; ::_thesis: for x being set st x in Z_Lin A holds
ex g1, h1 being FinSequence of V ex a1 being INT -valued FinSequence st
( x = Sum h1 & rng g1 c= A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) )
let x be set ; ::_thesis: ( x in Z_Lin A implies ex g1, h1 being FinSequence of V ex a1 being INT -valued FinSequence st
( x = Sum h1 & rng g1 c= A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) ) )
assume  x in Z_Lin A ; ::_thesis: ex g1, h1 being FinSequence of V ex a1 being INT -valued FinSequence st
( x = Sum h1 & rng g1 c= A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) )
then consider z being Linear_Combination of A such that
A1: ( x = Sum z & rng z c= INT ) ;
consider F being 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 being Nat st i in dom (z (#) F) holds
(z (#) F) . i = (z . (F /. i)) * (F /. i) ) ) by RLVECT_2:def_7;
defpred S1[ Nat, set ] means $2 = z . (F /. $1);
A4: now__::_thesis:_for_k_being_Nat_st_k_in_Seg_(len_F)_holds_
ex_x_being_Element_of_INT_st_S1[k,x]
let k be Nat; ::_thesis: ( k in Seg (len F) implies ex x being Element of INT st S1[k,x] )
assume  k in Seg (len F) ; ::_thesis: ex x being Element of INT st S1[k,x]
 z . (F /. k) in rng z by FUNCT_2:4;
hence  ex x being Element of INT st S1[k,x] by A1; ::_thesis: verum
end;
consider u being FinSequence of INT  such that
A5: ( dom u = Seg (len F) & ( for i being Nat st i in Seg (len F) holds
S1[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__::_thesis:_for_i_being_Nat_st_i_in_Seg_(len_F)_holds_
(z_(#)_F)_/._i_=_(u_._i)_*_(F_/._i)
let i be Nat; ::_thesis: ( i in Seg (len F) implies (z (#) F) /. i = (u . i) * (F /. i) )
assume A9: i in Seg (len F) ; ::_thesis: (z (#) F) /. i = (u . i) * (F /. i)
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 ;
::_thesis: verum
end;
hence  ex g1, h1 being FinSequence of V ex a1 being INT -valued FinSequence st
( x = Sum h1 & rng g1 c= A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) ) by A6, A7, A8, A1, A2; ::_thesis: verum
end;

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

registration
let D be non empty set ;
let n be Nat;
cluster Relation-like NAT -defined D -valued Function-like finite n -element FinSequence-like FinSubsequence-like for set ;
existence
 ex b1 being FinSequence st
( b1 is n -element & b1 is D -valued )
proof
take  n |-> the Element of D ; ::_thesis: ( n |-> the Element of D is n -element & n |-> the Element of D is D -valued )
thus  ( n |-> the Element of D is n -element & n |-> the Element of D is D -valued ) ; ::_thesis: verum
end;
end;

definition
let RS be RealLinearSpace;
let f be FinSequence of RS;
func Z_Lin f ->  Subset of RS equals :: RLVECT_X:def 3
 {  (Sum g) where g is len f -element FinSequence of RS : ex a being INT -valued len f -element FinSequence st
for i being Nat st i in Seg (len f) holds
g /. i = (a . i) * (f /. i)  }  ;
correctness
coherence
{  (Sum g) where g is len f -element FinSequence of RS : ex a being INT -valued len f -element FinSequence st
for i being Nat st i in Seg (len f) holds
g /. i = (a . i) * (f /. i)  }  is Subset of RS;
proof
now__::_thesis:_for_x_being_set_st_x_in__{__(Sum_g)_where_g_is_len_f_-element_FinSequence_of_RS_:_ex_a_being_INT_-valued_len_f_-element_FinSequence_st_
for_i_being_Nat_st_i_in_Seg_(len_f)_holds_
g_/._i_=_(a_._i)_*_(f_/._i)__}__holds_
x_in_the_carrier_of_RS
let x be set ; ::_thesis: ( x in  {  (Sum g) where g is len f -element FinSequence of RS : ex a being INT -valued len f -element FinSequence st
for i being Nat st i in Seg (len f) holds
g /. i = (a . i) * (f /. i)  }  implies x in the carrier of RS )
assume  x in  {  (Sum g) where g is len f -element FinSequence of RS : ex a being INT -valued len f -element FinSequence st
for i being Nat st i in Seg (len f) holds
g /. i = (a . i) * (f /. i)  }  ; ::_thesis: x in the carrier of RS
then  ex g being len f -element FinSequence of RS st
( x = Sum g & ex a being INT -valued len f -element FinSequence st
for i being Nat st i in Seg (len f) holds
g /. i = (a . i) * (f /. i) ) ;
hence  x in the carrier of RS ; ::_thesis: verum
end;
hence   {  (Sum g) where g is len f -element FinSequence of RS : ex a being INT -valued len f -element FinSequence st
for i being Nat st i in Seg (len f) holds
g /. i = (a . i) * (f /. i)  }  is Subset of RS by TARSKI:def_3; ::_thesis: verum
end;
end;

:: deftheorem  defines Z_Lin RLVECT_X:def_3_:_
 for RS being RealLinearSpace
for f being FinSequence of RS holds Z_Lin f =  {  (Sum g) where g is len b2 -element FinSequence of RS : ex a being INT -valued len b2 -element FinSequence st
for i being Nat st i in Seg (len f) holds
g /. i = (a . i) * (f /. i)  }  ;

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

theorem Th27: :: RLVECT_X:27
for RS being RealLinearSpace
for f being FinSequence of RS
for x, y being Element of RS
for 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; ::_thesis: for f being FinSequence of RS
for x, y being Element of RS
for 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
let f be FinSequence of RS; ::_thesis: for x, y being Element of RS
for 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
let x, y be Element of RS; ::_thesis: for 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
let a, b be Element of INT ; ::_thesis: ( x in Z_Lin f & y in Z_Lin f implies (a * x) + (b * y) in Z_Lin f )
assume A1: ( x in Z_Lin f & y in Z_Lin f ) ; ::_thesis: (a * x) + (b * y) in Z_Lin f
consider g being len f -element FinSequence of RS, s being INT -valued len f -element FinSequence such that
A2: ( x = Sum g & ( for i being Nat st i in Seg (len f) holds
g /. i = (s . i) * (f /. i) ) ) by A1, Th26;
consider h being len f -element FinSequence of RS, t being INT -valued len f -element FinSequence such that
A3: ( y = Sum h & ( for i being Nat st i in Seg (len f) holds
h /. i = (t . i) * (f /. i) ) ) by A1, Th26;
defpred S1[ Nat, set ] means $2 = (a * (s . $1)) + (b * (t . $1));
A4: for k being Nat st k in Seg (len f) holds
ex x being Element of INT st S1[k,x] ;
consider u being FinSequence of INT  such that
A5: ( dom u = Seg (len f) & ( for i being Nat st i in Seg (len f) holds
S1[i,u . i] ) ) from FINSEQ_1:sch_5(A4);
 len u = len f by A5, FINSEQ_1:def_3;
then reconsider u = u as INT -valued len f -element FinSequence by CARD_1:def_7;
defpred S2[ Nat, set ] means $2 = (a * (g /. $1)) + (b * (h /. $1));
A6: for k being Nat st k in Seg (len f) holds
ex x being Element of RS st S2[k,x] ;
consider w being FinSequence of RS such that
A7: ( dom w = Seg (len f) & ( for i being Nat st i in Seg (len f) holds
S2[i,w . i] ) ) from FINSEQ_1:sch_5(A6);
 len w = len f by A7, FINSEQ_1:def_3;
then reconsider w = w as len f -element FinSequence of RS by CARD_1:def_7;
A8: now__::_thesis:_for_i_being_Nat_st_i_in_Seg_(len_f)_holds_
w_/._i_=_(a_*_(g_/._i))_+_(b_*_(h_/._i))
let i be Nat; ::_thesis: ( i in Seg (len f) implies w /. i = (a * (g /. i)) + (b * (h /. i)) )
assume A9: i in Seg (len f) ; ::_thesis: w /. i = (a * (g /. i)) + (b * (h /. i))
hence w /. i = w . i by A7, PARTFUN1:def_6
.= (a * (g /. i)) + (b * (h /. i)) by A7, A9 ;
::_thesis: verum
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__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_ag_holds_
w_._i_=_(ag_/._i)_+_(bh_/._i)
let i be Element of NAT ; ::_thesis: ( i in dom ag implies w . i = (ag /. i) + (bh /. i) )
assume A16: i in dom ag ; ::_thesis: w . i = (ag /. i) + (bh /. i)
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 ;
::_thesis: verum
end;
A17: ( len ag = len bh & len ag = len w ) by A7, A13, A14, FINSEQ_1:def_3;
A18: for i being Nat st i in Seg (len f) holds
w /. i = (u . i) * (f /. i)
proof
let i be Nat; ::_thesis: ( i in Seg (len f) implies w /. i = (u . i) * (f /. i) )
assume A19: i in Seg (len f) ; ::_thesis: w /. i = (u . i) * (f /. i)
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 ;
::_thesis: verum
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; ::_thesis: verum
end;

theorem Th28: :: RLVECT_X:28
for RS being RealLinearSpace
for f being FinSequence of RS st f = (Seg (len f)) --> (0. RS) holds
Sum f = 0. RS
proof
let RS be RealLinearSpace; ::_thesis: for f being FinSequence of RS st f = (Seg (len f)) --> (0. RS) holds
Sum f = 0. RS
let f be FinSequence of RS; ::_thesis: ( f = (Seg (len f)) --> (0. RS) implies Sum f = 0. RS )
assume A1: f = (Seg (len f)) --> (0. RS) ; ::_thesis: Sum f = 0. RS
A2: now__::_thesis:_for_k_being_Element_of_NAT_
for_v_being_Element_of_RS_st_k_in_dom_f_&_v_=_f_._k_holds_
f_._k_=_-_v
let k be Element of NAT ; ::_thesis: for v being Element of RS st k in dom f & v = f . k holds
f . k = - v
let v be Element of RS; ::_thesis: ( k in dom f & v = f . k implies f . k = - v )
assume A3: ( k in dom f & v = f . k ) ; ::_thesis: f . k = - v
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; ::_thesis: verum
end;
 len f = len f ;
then  Sum f = - (Sum f) by A2, RLVECT_1:40;
hence  Sum f = 0. RS by RLVECT_1:19; ::_thesis: verum
end;

theorem Th29: :: RLVECT_X:29
for RS being RealLinearSpace
for f being FinSequence of RS
for v being Element of RS
for i being Nat st i in Seg (len f) & f = ((Seg (len f)) --> (0. RS)) +* ({i} --> v) holds
Sum f = v
proof
let RS be RealLinearSpace; ::_thesis: for f being FinSequence of RS
for v being Element of RS
for i being Nat st i in Seg (len f) & f = ((Seg (len f)) --> (0. RS)) +* ({i} --> v) holds
Sum f = v
let f be FinSequence of RS; ::_thesis: for v being Element of RS
for i being Nat st i in Seg (len f) & f = ((Seg (len f)) --> (0. RS)) +* ({i} --> v) holds
Sum f = v
let v be Element of RS; ::_thesis: for i being Nat st i in Seg (len f) & f = ((Seg (len f)) --> (0. RS)) +* ({i} --> v) holds
Sum f = v
let i be Nat; ::_thesis: ( i in Seg (len f) & f = ((Seg (len f)) --> (0. RS)) +* ({i} --> v) implies Sum f = v )
defpred S1[ Nat] means  for g being 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: S1[ 0 ] ;
A2: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A3: S1[n] ; ::_thesis: S1[n + 1]
now__::_thesis:_for_f_being_FinSequence_of_RS_st_len_f_=_n_+_1_&_i_in_Seg_(len_f)_&_f_=_((Seg_(len_f))_-->_(0._RS))_+*_({i}_-->_v)_holds_
for_f1_being_Function_st_f1_=_(Seg_(len_f))_-->_(0._RS)_holds_
for_f2_being_Function_st_f2_=_{i}_-->_v_holds_
Sum_f_=_v
let f be FinSequence of RS; ::_thesis: ( len f = n + 1 & i in Seg (len f) & f = ((Seg (len f)) --> (0. RS)) +* ({i} --> v) implies for f1 being Function st f1 = (Seg (len f)) --> (0. RS) holds
for f2 being Function st f2 = {i} --> v holds
Sum b3 = v )
assume A4: ( len f = n + 1 & i in Seg (len f) & f = ((Seg (len f)) --> (0. RS)) +* ({i} --> v) ) ; ::_thesis: for f1 being Function st f1 = (Seg (len f)) --> (0. RS) holds
for f2 being Function st f2 = {i} --> v holds
Sum b3 = 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; ::_thesis: ( f1 = (Seg (len f)) --> (0. RS) implies for f2 being Function st f2 = {i} --> v holds
Sum b2 = v )
assume A9: f1 = (Seg (len f)) --> (0. RS) ; ::_thesis: for f2 being Function st f2 = {i} --> v holds
Sum b2 = v
let f2 be Function; ::_thesis: ( f2 = {i} --> v implies Sum b1 = v )
assume A10: f2 = {i} --> v ; ::_thesis: Sum b1 = v
percases ( i = n + 1 or i <> n + 1 ) ;
supposeA11: i = n + 1 ; ::_thesis: Sum b1 = v
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 ;
::_thesis: verum
end;
supposeA15: i <> n + 1 ; ::_thesis: Sum b1 = v
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 ;
::_thesis: verum
end;
end;
end;
hence  S1[n + 1] ; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2);
hence  ( i in Seg (len f) & f = ((Seg (len f)) --> (0. RS)) +* ({i} --> v) implies Sum f = v ) ; ::_thesis: verum
end;

theorem Th30: :: RLVECT_X:30
for RS being RealLinearSpace
for f being FinSequence of RS
for i being Nat st i in Seg (len f) holds
f /. i in Z_Lin f
proof
let RS be RealLinearSpace; ::_thesis: for f being FinSequence of RS
for i being Nat st i in Seg (len f) holds
f /. i in Z_Lin f
let f be FinSequence of RS; ::_thesis: for i being Nat st i in Seg (len f) holds
f /. i in Z_Lin f
let i be Nat; ::_thesis: ( i in Seg (len f) implies f /. i in Z_Lin f )
assume A1: i in Seg (len f) ; ::_thesis: f /. i in Z_Lin f
set s = ((Seg (len f)) --> 0) +* ({i} --> 1);
A2: dom (((Seg (len f)) --> 0) +* ({i} --> 1)) = Seg (len f)
proof
dom (((Seg (len f)) --> 0) +* ({i} --> 1)) = (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  dom (((Seg (len f)) --> 0) +* ({i} --> 1)) = Seg (len f) by A1, ZFMISC_1:40; ::_thesis: verum
end;
then A3: ((Seg (len f)) --> 0) +* ({i} --> 1) is FinSequence-like by FINSEQ_1:def_2;
 rng (((Seg (len f)) --> 0) +* ({i} --> 1)) c= INT
proof
 rng (((Seg (len f)) --> 0) +* ({i} --> 1)) c= (rng ((Seg (len f)) --> 0)) \/ (rng ({i} --> 1)) by FUNCT_4:17;
hence  rng (((Seg (len f)) --> 0) +* ({i} --> 1)) c= INT by XBOOLE_1:1; ::_thesis: verum
end;
then reconsider s = ((Seg (len f)) --> 0) +* ({i} --> 1) as FinSequence of INT by A3, FINSEQ_1:def_4;
 len s = len f by A2, FINSEQ_1:def_3;
then reconsider s = s as INT -valued len f -element FinSequence by CARD_1:def_7;
defpred S1[ Nat, set ] means $2 = (s . $1) * (f /. $1);
A6: for k being Nat st k in Seg (len f) holds
ex x being Element of RS st S1[k,x] ;
consider w being FinSequence of RS such that
A7: ( dom w = Seg (len f) & ( for i being Nat st i in Seg (len f) holds
S1[i,w . i] ) ) from FINSEQ_1:sch_5(A6);
A8: len w = len f by A7, FINSEQ_1:def_3;
then reconsider w = w as len f -element FinSequence of RS by CARD_1:def_7;
now__::_thesis:_for_i_being_Nat_st_i_in_Seg_(len_f)_holds_
w_/._i_=_(s_._i)_*_(f_/._i)
let i be Nat; ::_thesis: ( i in Seg (len f) implies w /. i = (s . i) * (f /. i) )
assume A9: i in Seg (len f) ; ::_thesis: w /. i = (s . i) * (f /. i)
hence w /. i = w . i by A7, PARTFUN1:def_6
.= (s . i) * (f /. i) by A7, A9 ;
::_thesis: verum
end;
then A10: Sum w in Z_Lin f ;
A11: w = ((Seg (len w)) --> (0. RS)) +* ({i} --> (f /. i))
proof
consider w1 being Function such that
A12: w1 = (Seg (len f)) --> (0. RS) ;
A13: dom w1 = Seg (len f) by A12, FUNCOP_1:13;
consider w2 being Function such that
A14: w2 = {i} --> (f /. i) ;
A15: dom w2 = {i} by A14, FUNCOP_1:13;
consider ww being 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 = 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 = 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; ::_thesis: ( j in dom w implies w /. j = ww /. j )
assume A21: j in dom w ; ::_thesis: w /. j = ww /. j
A22: dom ({i} --> 1) = {i} by FUNCOP_1:13;
percases ( j in dom w2 or not j in dom w2 ) ;
supposeA23: j in dom w2 ; ::_thesis: w /. j = ww /. j
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  w /. j = ww /. j by A25, A27, RLVECT_1:def_8; ::_thesis: verum
end;
supposeA28: not j in dom w2 ; ::_thesis: w /. j = ww /. j
 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  w /. j = ww /. j by A29, A30, RLVECT_1:10; ::_thesis: verum
end;
end;
end;
hence  w = ((Seg (len w)) --> (0. RS)) +* ({i} --> (f /. i)) by A7, A8, A12, A14, A16, A17, FINSEQ_5:12; ::_thesis: verum
end;
 i in Seg (len w) by A7, A1, FINSEQ_1:def_3;
hence  f /. i in Z_Lin f by A10, A11, Th29; ::_thesis: verum
end;

theorem Th31: :: RLVECT_X:31
for RS being RealLinearSpace
for f being FinSequence of RS holds rng f c= Z_Lin f
proof
let RS be RealLinearSpace; ::_thesis: for f being FinSequence of RS holds rng f c= Z_Lin f
let f be FinSequence of RS; ::_thesis: rng f c= Z_Lin f
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in Z_Lin f )
assume  y in rng f ; ::_thesis: y in Z_Lin f
then consider x being 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; ::_thesis: verum
end;

theorem Th32: :: RLVECT_X:32
for RS being RealLinearSpace
for f being non empty FinSequence of RS
for g, h being FinSequence of RS
for s being INT -valued FinSequence st rng g c= Z_Lin f & len g = len s & len g = len h & ( for i being 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; ::_thesis: for f being non empty FinSequence of RS
for g, h being FinSequence of RS
for s being INT -valued FinSequence st rng g c= Z_Lin f & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) holds
Sum h in Z_Lin f
let f be non empty FinSequence of RS; ::_thesis: for g, h being FinSequence of RS
for s being INT -valued FinSequence st rng g c= Z_Lin f & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) holds
Sum h in Z_Lin f
 ( 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 S1[ Nat] means  for g, h being FinSequence of RS
for s being INT -valued FinSequence st rng g c= Z_Lin f & len g = $1 & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) holds
Sum h in Z_Lin f;
A3: S1[ 0 ]
proof
let g, h be FinSequence of RS; ::_thesis: for s being INT -valued FinSequence st rng g c= Z_Lin f & len g = 0 & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) holds
Sum h in Z_Lin f
let s be INT -valued FinSequence; ::_thesis: ( rng g c= Z_Lin f & len g = 0 & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) implies Sum h in Z_Lin f )
assume A4: ( rng g c= Z_Lin f & len g = 0 & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) ) ; ::_thesis: Sum h in Z_Lin f
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; ::_thesis: verum
end;
A5: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A6: S1[n] ; ::_thesis: S1[n + 1]
now__::_thesis:_for_g,_h_being_FinSequence_of_RS
for_s_being_INT_-valued_FinSequence_st_rng_g_c=_Z_Lin_f_&_len_g_=_n_+_1_&_len_g_=_len_s_&_len_g_=_len_h_&_(_for_i_being_Nat_st_i_in_Seg_(len_g)_holds_
h_/._i_=_(s_._i)_*_(g_/._i)_)_holds_
Sum_h_in_Z_Lin_f
let g, h be FinSequence of RS; ::_thesis: for s being INT -valued FinSequence st rng g c= Z_Lin f & len g = n + 1 & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) holds
Sum h in Z_Lin f
let s be INT -valued FinSequence; ::_thesis: ( rng g c= Z_Lin f & len g = n + 1 & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) implies Sum h in Z_Lin f )
assume A7: ( rng g c= Z_Lin f & len g = n + 1 & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) ) ; ::_thesis: Sum h in Z_Lin f
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 being 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 being Nat st i in Seg (len gn) holds
hn /. i = (sn . i) * (gn /. i)
proof
percases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; ::_thesis: for i being Nat st i in Seg (len gn) holds
hn /. i = (sn . i) * (gn /. i)
hence  for i being Nat st i in Seg (len gn) holds
hn /. i = (sn . i) * (gn /. i) ; ::_thesis: verum
end;
suppose n <> 0 ; ::_thesis: for i being Nat st i in Seg (len gn) holds
hn /. i = (sn . i) * (gn /. i)
then A14: n >= 1 by NAT_1:14;
let i be Nat; ::_thesis: ( i in Seg (len gn) implies hn /. i = (sn . i) * (gn /. i) )
assume  i in Seg (len gn) ; ::_thesis: hn /. i = (sn . i) * (gn /. i)
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  hn /. i = (sn . i) * (gn /. i) by A7, A15, A16, A17, FINSEQ_2:8; ::_thesis: verum
end;
end;
end;
hence  ( rng gn c= Z_Lin f & len gn = n & len gn = len sn & len gn = len hn & ( for i being Nat st i in Seg (len gn) holds
hn /. i = (sn . i) * (gn /. i) ) ) by A9, A10, A12, A13, A7, FINSEQ_1:59, XBOOLE_1:1; ::_thesis: verum
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; ::_thesis: verum
end;
hence  S1[n + 1] ; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A3, A5);
hence  for g, h being FinSequence of RS
for s being INT -valued FinSequence st rng g c= Z_Lin f & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) holds
Sum h in Z_Lin f ; ::_thesis: verum
end;

theorem :: RLVECT_X:33
for RS being RealLinearSpace
for f being non empty FinSequence of RS holds Z_Lin (rng f) = Z_Lin f
proof
let RS be RealLinearSpace; ::_thesis: for f being non empty FinSequence of RS holds Z_Lin (rng f) = Z_Lin f
let f be non empty FinSequence of RS; ::_thesis: Z_Lin (rng f) = Z_Lin f
 for x being set holds
( x in Z_Lin (rng f) iff x in Z_Lin f )
proof
let x be set ; ::_thesis: ( x in Z_Lin (rng f) iff x in Z_Lin f )
hereby  ::_thesis: ( x in Z_Lin f implies x in Z_Lin (rng f) )
assume  x in Z_Lin (rng f) ; ::_thesis: x in Z_Lin f
then consider g, h being FinSequence of RS, a being INT -valued FinSequence such that
A1: ( x = Sum h & rng g c= rng f & len g = len h & len g = len a & ( for i being 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; ::_thesis: verum
end;
assume  x in Z_Lin f ; ::_thesis: x in Z_Lin (rng f)
then consider g being len f -element FinSequence of RS, a being INT -valued len f -element FinSequence such that
A2: ( x = Sum g & ( for i being 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; ::_thesis: verum
end;
hence  Z_Lin (rng f) = Z_Lin f by TARSKI:1; ::_thesis: verum
end;

theorem Th34: :: RLVECT_X:34
for V being RealLinearSpace
for A being Subset of V holds Lin (Z_Lin A) = Lin A
proof
let V be RealLinearSpace; ::_thesis: for A being Subset of V holds Lin (Z_Lin A) = Lin A
let A be Subset of V; ::_thesis: Lin (Z_Lin A) = Lin A
 for x being 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  Lin (Z_Lin A) = Lin A by A1, RLSUB_1:26; ::_thesis: verum
end;

theorem Th35: :: RLVECT_X:35
for V being RealLinearSpace
for A being Subset of V
for x being set
for g1, h1 being FinSequence of V
for a1 being INT -valued FinSequence st x = Sum h1 & rng g1 c= Z_Lin A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) holds
x in Z_Lin A
proof
let V be RealLinearSpace; ::_thesis: for A being Subset of V
for x being set
for g1, h1 being FinSequence of V
for a1 being INT -valued FinSequence st x = Sum h1 & rng g1 c= Z_Lin A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) holds
x in Z_Lin A
let A be Subset of V; ::_thesis: for x being set
for g1, h1 being FinSequence of V
for a1 being INT -valued FinSequence st x = Sum h1 & rng g1 c= Z_Lin A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) holds
x in Z_Lin A
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 S1[ Nat] means  for x being set
for g1, h1 being FinSequence of V
for a1 being 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 being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) holds
x in Z_Lin A;
A1: S1[ 0 ]
proof
let x be set ; ::_thesis: for g1, h1 being FinSequence of V
for a1 being INT -valued FinSequence st x = Sum h1 & rng g1 c= Z_Lin A & len g1 = 0 & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) holds
x in Z_Lin A
let g1, h1 be FinSequence of V; ::_thesis: for a1 being INT -valued FinSequence st x = Sum h1 & rng g1 c= Z_Lin A & len g1 = 0 & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) holds
x in Z_Lin A
let a1 be INT -valued FinSequence; ::_thesis: ( x = Sum h1 & rng g1 c= Z_Lin A & len g1 = 0 & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) implies x in Z_Lin A )
assume A2: ( x = Sum h1 & rng g1 c= Z_Lin A & len g1 = 0 & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) ) ; ::_thesis: x in Z_Lin A
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; ::_thesis: verum
end;
A3: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; ::_thesis: S1[n + 1]
now__::_thesis:_for_x_being_set_
for_g1,_h1_being_FinSequence_of_V
for_a1_being_INT_-valued_FinSequence_st_x_=_Sum_h1_&_rng_g1_c=_Z_Lin_A_&_len_g1_=_n_+_1_&_len_g1_=_len_h1_&_len_g1_=_len_a1_&_(_for_i_being_Nat_st_i_in_Seg_(len_g1)_holds_
h1_/._i_=_(a1_._i)_*_(g1_/._i)_)_holds_
Sum_h1_in_Z_Lin_A
let x be set ; ::_thesis: for g1, h1 being FinSequence of V
for a1 being INT -valued FinSequence st x = Sum h1 & rng g1 c= Z_Lin A & len g1 = n + 1 & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) holds
Sum h1 in Z_Lin A
let g1, h1 be FinSequence of V; ::_thesis: for a1 being INT -valued FinSequence st x = Sum h1 & rng g1 c= Z_Lin A & len g1 = n + 1 & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) holds
Sum h1 in Z_Lin A
let a1 be INT -valued FinSequence; ::_thesis: ( x = Sum h1 & rng g1 c= Z_Lin A & len g1 = n + 1 & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) implies Sum h1 in Z_Lin A )
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 being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) ) ; ::_thesis: Sum h1 in Z_Lin A
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 being 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 being Nat st i in Seg (len gn) holds
hn /. i = (an . i) * (gn /. i)
proof
percases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; ::_thesis: for i being Nat st i in Seg (len gn) holds
hn /. i = (an . i) * (gn /. i)
hence  for i being Nat st i in Seg (len gn) holds
hn /. i = (an . i) * (gn /. i) ; ::_thesis: verum
end;
suppose n <> 0 ; ::_thesis: for i being Nat st i in Seg (len gn) holds
hn /. i = (an . i) * (gn /. i)
then A12: n >= 1 by NAT_1:14;
let i be Nat; ::_thesis: ( i in Seg (len gn) implies hn /. i = (an . i) * (gn /. i) )
assume  i in Seg (len gn) ; ::_thesis: hn /. i = (an . i) * (gn /. i)
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  hn /. i = (an . i) * (gn /. i) by A5, A13, A14, A15, FINSEQ_2:8; ::_thesis: verum
end;
end;
end;
hence  ( rng gn c= Z_Lin A & len gn = n & len gn = len an & len gn = len hn & ( for i being Nat st i in Seg (len gn) holds
hn /. i = (an . i) * (gn /. i) ) ) by A5, A7, A8, A10, A11, FINSEQ_1:59, XBOOLE_1:1; ::_thesis: verum
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; ::_thesis: verum
end;
hence  S1[n + 1] ; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A1, A3);
hence  for x being set
for g1, h1 being FinSequence of V
for a1 being INT -valued FinSequence st x = Sum h1 & rng g1 c= Z_Lin A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) holds
x in Z_Lin A ; ::_thesis: verum
end;

theorem :: RLVECT_X:36
for V being RealLinearSpace
for A being Subset of V holds Z_Lin (Z_Lin A) = Z_Lin A
proof
let V be RealLinearSpace; ::_thesis: for A being Subset of V holds Z_Lin (Z_Lin A) = Z_Lin A
let A be Subset of V; ::_thesis: Z_Lin (Z_Lin A) = Z_Lin A
 for x being 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 ; :: according to TARSKI:def_3 ::_thesis: ( not x in Z_Lin (Z_Lin A) or x in Z_Lin A )
assume  x in Z_Lin (Z_Lin A) ; ::_thesis: x in Z_Lin A
then consider g1, h1 being FinSequence of V, a1 being 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 being 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; ::_thesis: verum
end;
hence  Z_Lin (Z_Lin A) = Z_Lin A by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: RLVECT_X:37
for V being RealLinearSpace
for A, B being Subset of V st Z_Lin A = Z_Lin B holds
Lin A = Lin B
proof
let V be RealLinearSpace; ::_thesis: for A, B being Subset of V st Z_Lin A = Z_Lin B holds
Lin A = Lin B
let A, B be Subset of V; ::_thesis: ( Z_Lin A = Z_Lin B implies Lin A = Lin B )
assume  Z_Lin A = Z_Lin B ; ::_thesis: Lin A = Lin B
hence  Lin A = Lin (Z_Lin B) by Th34
.= Lin B by Th34 ;
::_thesis: verum
end;