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 S1[ 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 S1[x,y]
proof
let x be object ; :: thesis: ( x in the carrier of V implies ex y being object st S1[x,y] )
assume x in the carrier of V ; :: thesis: ex y being object st S1[x,y]
now :: thesis: ex y being object st S1[x,y]
per cases ( x in A or not x in A ) ;
suppose x in A ; :: thesis: ex y being object st S1[x,y]
hence ex y being object st S1[x,y] ; :: thesis: verum
end;
suppose not x in A ; :: thesis: ex y being object st S1[x,y]
hence ex y being object st S1[x,y] ; :: thesis: verum
end;
end;
end;
hence ex y being object st S1[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
S1[x,L1 . x] ) ) from 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:
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:
per cases ( x in A or not x in A ) ;
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 ;
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 ;
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 ;
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 ;
hence v in Carrier L1 by ; :: thesis: verum
end;
then A c= Carrier L1 ;
hence Carrier L1 = A by ; :: thesis: verum