let n be Nat; :: thesis: for Lv being Linear_Combination of RealVectSpace (Seg n)

for Lr being Linear_Combination of TOP-REAL n st Lr = Lv holds

Sum Lr = Sum Lv

set V = RealVectSpace (Seg n);

set T = TOP-REAL n;

let Lv be Linear_Combination of RealVectSpace (Seg n); :: thesis: for Lr being Linear_Combination of TOP-REAL n st Lr = Lv holds

Sum Lr = Sum Lv

let Lr be Linear_Combination of TOP-REAL n; :: thesis: ( Lr = Lv implies Sum Lr = Sum Lv )

assume A1: Lr = Lv ; :: thesis: Sum Lr = Sum Lv

consider F being FinSequence of the carrier of (TOP-REAL n) such that

A2: ( F is one-to-one & rng F = Carrier Lr ) and

A3: Sum Lr = Sum (Lr (#) F) by RLVECT_2:def 8;

reconsider F1 = F as FinSequence of the carrier of (RealVectSpace (Seg n)) by Lm1;

A4: Lr (#) F = Lv (#) F1 by A1, Th18;

thus Sum Lv = Sum (Lv (#) F1) by A1, A2, RLVECT_2:def 8

.= Sum Lr by A3, A4, Th19 ; :: thesis: verum

for Lr being Linear_Combination of TOP-REAL n st Lr = Lv holds

Sum Lr = Sum Lv

set V = RealVectSpace (Seg n);

set T = TOP-REAL n;

let Lv be Linear_Combination of RealVectSpace (Seg n); :: thesis: for Lr being Linear_Combination of TOP-REAL n st Lr = Lv holds

Sum Lr = Sum Lv

let Lr be Linear_Combination of TOP-REAL n; :: thesis: ( Lr = Lv implies Sum Lr = Sum Lv )

assume A1: Lr = Lv ; :: thesis: Sum Lr = Sum Lv

consider F being FinSequence of the carrier of (TOP-REAL n) such that

A2: ( F is one-to-one & rng F = Carrier Lr ) and

A3: Sum Lr = Sum (Lr (#) F) by RLVECT_2:def 8;

reconsider F1 = F as FinSequence of the carrier of (RealVectSpace (Seg n)) by Lm1;

A4: Lr (#) F = Lv (#) F1 by A1, Th18;

thus Sum Lv = Sum (Lv (#) F1) by A1, A2, RLVECT_2:def 8

.= Sum Lr by A3, A4, Th19 ; :: thesis: verum