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_{1}[ 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_{1}[x,y]

A5: ( dom L1 = the carrier of V & ( for x being object st x in the carrier of V holds

S_{1}[x,L1 . x] ) )
from CLASSES1:sch 1(A4);

for y being object st y in rng L1 holds

y in 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

take L1 ; :: thesis: Carrier L1 = A

for v being object st v in A holds

v in Carrier L1

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

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

A4: for x being object st x in the carrier of V holds

ex y being object st S

proof

consider L1 being Function such that
let x be object ; :: thesis: ( x in the carrier of V implies ex y being object st S_{1}[x,y] )

assume x in the carrier of V ; :: thesis: ex y being object st S_{1}[x,y]

_{1}[x,y]
; :: thesis: verum

end;assume x in the carrier of V ; :: thesis: ex y being object st S

now :: thesis: ex y being object st S_{1}[x,y]

hence
ex y being object st Send;

A5: ( dom L1 = the carrier of V & ( for x being object st x in the carrier of V holds

S

for y being object st y in rng L1 holds

y in REAL

proof

then
rng L1 c= REAL
;
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;

end;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

hence
y in REAL
; :: thesis: verumend;

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

then A13:
Carrier L1 c= A
;
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;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

take L1 ; :: thesis: Carrier L1 = A

for v being object st v in A holds

v in Carrier L1

proof

then
A c= Carrier L1
;
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;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

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