let V be RealUnitarySpace; :: 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 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, Th16;
take K ; :: thesis: Sum L = Sum K
thus Sum L = Sum K by A2, A3; :: thesis: verum