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 )
consider F being Function such that
A1: L = F and
A2: dom F = the carrier of V and
A3: rng F c= REAL by FUNCT_2:def 2;
defpred S₁[ object , object ] means ( ( $1 in A implies $2 = F . $1 ) & ( not $1 in A implies $2 = 0 ) );
A4: for x being object st x in the carrier of V holds
ex y being object st S₁[x,y]

proof

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

now :: thesis: ex y being object st S₁[x,y]

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

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

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

end;

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

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

end;

end;

end;

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

end;

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

proof

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

now :: thesis: y in REAL

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

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

A9: F . x in rng F by A2, FUNCT_1:3;
y = F . x by A5, A7, A8;
hence y in REAL by A3, A9; :: thesis: verum

end;

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

then L1 . x = In (0,REAL) by A5;
hence y in REAL by A7; :: thesis: verum

end;

end;

end;

hence y in REAL ; :: thesis: verum

end;

then rng L1 c= REAL ;
then A10: L1 is Element of Funcs ( the carrier of V,REAL) by A5, FUNCT_2:def 2;
assume A11: A c= Carrier L ; :: thesis: ex L1 being Linear_Combination of V st Carrier L1 = A
then reconsider A = A as finite Subset of V by FINSET_1:1;
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 A10, RLVECT_2:def 3;
for v being object st v in Carrier L1 holds
v in A

proof

let v be object ; :: 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:19;
hence v in A by A5; :: thesis: verum

end;

then A13: Carrier L1 c= A ;
take L1 ; :: thesis: Carrier L1 = A
for v being object st v in A holds
v in Carrier L1

proof

let v be object ; :: thesis: ( v in A implies v in Carrier L1 )
assume A14: v in A ; :: thesis: v in Carrier L1
then reconsider v = v as Element of V ;
( L1 . v = F . v & L . v <> 0 ) by A11, A5, A14, RLVECT_2:19;
hence v in Carrier L1 by A1, RLVECT_2:19; :: thesis: verum

end;

then A c= Carrier L1 ;
hence Carrier L1 = A by A13, XBOOLE_0:def 10; :: thesis: verum