let RNS1, RNS2 be RealLinearSpace; :: thesis: ( RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #) = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #) implies for L being Linear_Combination of RNS2
for S being Linear_Combination of RNS1 st L = S holds
Sum L = Sum S )
assume A1: RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #) = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #) ; :: thesis: for L being Linear_Combination of RNS2
for S being Linear_Combination of RNS1 st L = S holds
Sum L = Sum S
let L be Linear_Combination of RNS2; :: thesis: for S being Linear_Combination of RNS1 st L = S holds
Sum L = Sum S
let S be Linear_Combination of RNS1; :: thesis: ( L = S implies Sum L = Sum S )
assume A2: L = S ; :: thesis: Sum L = Sum S
consider F being FinSequence of RNS2 such that
A3: ( F is one-to-one & rng F = Carrier L & Sum L = Sum (L (#) F) ) by RLVECT_2:def 8;
reconsider E = F as FinSequence of RNS1 by A1;
A4: Sum (L (#) F) = Sum (S (#) E) by A2, A1, Th12, Th13;
reconsider SS = Sum L as Element of RNS1 by A1;
thus Sum L = Sum S by RLVECT_2:def 8, A2, A3, A4; :: thesis: verum