let V be RealLinearSpace; :: thesis: for L being Linear_Combination of V

for A being Subset of V st Carrier L c= the carrier of (Lin A) holds

ex K being Linear_Combination of A st Sum L = Sum K

let L be Linear_Combination of V; :: thesis: for A being Subset of V st Carrier L c= the carrier of (Lin A) holds

ex K being Linear_Combination of A st Sum L = Sum K

let A be Subset of V; :: thesis: ( Carrier L c= the carrier of (Lin A) implies ex K being Linear_Combination of A st Sum L = Sum K )

consider F being FinSequence of the carrier of V such that

F is one-to-one and

A1: rng F = Carrier L and

A2: Sum L = Sum (L (#) F) by RLVECT_2:def 8;

assume Carrier L c= the carrier of (Lin A) ; :: thesis: ex K being Linear_Combination of A st Sum L = Sum K

then consider K being Linear_Combination of A such that

A3: Sum (L (#) F) = Sum K by A1, Th8;

take K ; :: thesis: Sum L = Sum K

thus Sum L = Sum K by A2, A3; :: thesis: verum

for A being Subset of V st Carrier L c= the carrier of (Lin A) holds

ex K being Linear_Combination of A st Sum L = Sum K

let L be Linear_Combination of V; :: thesis: for A being Subset of V st Carrier L c= the carrier of (Lin A) holds

ex K being Linear_Combination of A st Sum L = Sum K

let A be Subset of V; :: thesis: ( Carrier L c= the carrier of (Lin A) implies ex K being Linear_Combination of A st Sum L = Sum K )

consider F being FinSequence of the carrier of V such that

F is one-to-one and

A1: rng F = Carrier L and

A2: Sum L = Sum (L (#) F) by RLVECT_2:def 8;

assume Carrier L c= the carrier of (Lin A) ; :: thesis: ex K being Linear_Combination of A st Sum L = Sum K

then consider K being Linear_Combination of A such that

A3: Sum (L (#) F) = Sum K by A1, Th8;

take K ; :: thesis: Sum L = Sum K

thus Sum L = Sum K by A2, A3; :: thesis: verum