let V be RealLinearSpace; :: thesis: for L being Linear_Combination of V
for A being Subset of V st A c= Carrier L holds
ex L1 being Linear_Combination of V st Carrier L1 = A
let L be Linear_Combination of V; :: thesis: for A being Subset of V st A c= Carrier L holds
ex L1 being Linear_Combination of V st Carrier L1 = A
let A be Subset of V; :: thesis: ( A c= Carrier L implies ex L1 being Linear_Combination of V st Carrier L1 = A )
assume A1: A c= Carrier L ; :: thesis: ex L1 being Linear_Combination of V st Carrier L1 = A
consider F being Function such that
A2: ( L = F & dom F = the carrier of V & rng F c= REAL ) by FUNCT_2:def 2;
defpred S₁[ set , set ] means ( ( $1 in A implies $2 = F . $1 ) & ( not $1 in A implies $2 = 0 ) );
A4: for x being set st x in the carrier of V holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in the carrier of V implies ex y being set st S₁[x,y] )
assume x in the carrier of V ; :: thesis: ex y being set st S₁[x,y]

now

per cases ( x in A or not x in A ) ;

suppose x in A ; :: thesis: ex y being set st S₁[x,y]

hence ex y being set st S₁[x,y] ; :: thesis: verum

end;

suppose not x in A ; :: thesis: ex y being set st S₁[x,y]

hence ex y being set st S₁[x,y] ; :: thesis: verum

end;

end;

end;

hence ex y being set st S₁[x,y] ; :: thesis: verum

end;

consider L1 being Function such that
A5: ( dom L1 = the carrier of V & ( for x being set st x in the carrier of V holds
S₁[x,L1 . x] ) ) from CLASSES1:sch 1(A4);
for y being set st y in rng L1 holds
y in REAL

proof

let y be set ; :: thesis: ( y in rng L1 implies y in REAL )
assume y in rng L1 ; :: thesis: y in REAL
then consider x being set such that
A6: ( x in dom L1 & y = L1 . x ) by FUNCT_1:def 5;
reconsider x = x as Element of V by A5, A6;

now

per cases ( x in A or not x in A ) ;

suppose x in A ; :: thesis: y in REAL

then A7: y = F . x by A5, A6;
F . x in rng F by A2, FUNCT_1:12;
hence y in REAL by A2, A7; :: thesis: verum

end;

suppose not x in A ; :: thesis: y in REAL

then L1 . x = 0 by A5;
hence y in REAL by A6; :: thesis: verum

end;

end;

end;

hence y in REAL ; :: thesis: verum

end;

then rng L1 c= REAL by TARSKI:def 3;
then A8: L1 is Element of Funcs the carrier of V,REAL by A5, FUNCT_2:def 2;
reconsider A = A as finite Subset of V by A1, FINSET_1:13;
for v being Element of V st not v in A holds
L1 . v = 0 by A5;
then reconsider L1 = L1 as Linear_Combination of V by A8, RLVECT_2:def 5;
for v being set st v in A holds
v in Carrier L1

proof

let v be set ; :: thesis: ( v in A implies v in Carrier L1 )
assume A9: v in A ; :: thesis: v in Carrier L1
then reconsider v = v as Element of V ;
A10: L1 . v = F . v by A5, A9;
L . v <> 0 by A1, A9, RLVECT_2:28;
hence v in Carrier L1 by A2, A10, RLVECT_2:28; :: thesis: verum

end;

then A11: A c= Carrier L1 by TARSKI:def 3;
for v being set st v in Carrier L1 holds
v in A

proof

let v be set ; :: thesis: ( v in Carrier L1 implies v in A )
assume A12: v in Carrier L1 ; :: thesis: v in A
then reconsider v = v as Element of V ;
L1 . v <> 0 by A12, RLVECT_2:28;
hence v in A by A5; :: thesis: verum

end;

then A13: Carrier L1 c= A by TARSKI:def 3;
take L1 ; :: thesis: Carrier L1 = A
thus Carrier L1 = A by A11, A13, XBOOLE_0:def 10; :: thesis: verum