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 Lr being Linear_Combination of RNS2
for Lt being Linear_Combination of RNS1 st Lr = Lt holds
Sum Lr = Sum Lt )
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 Lr being Linear_Combination of RNS2
for Lt being Linear_Combination of RNS1 st Lr = Lt holds
Sum Lr = Sum Lt
let Lr be Linear_Combination of RNS2; :: thesis: for Lt being Linear_Combination of RNS1 st Lr = Lt holds
Sum Lr = Sum Lt
let Lt be Linear_Combination of RNS1; :: thesis: ( Lr = Lt implies Sum Lr = Sum Lt )
assume A2: Lr = Lt ; :: thesis: Sum Lr = Sum Lt
set R = RNS2;
set T = RNS1;
consider Ft being FinSequence of the carrier of RNS1 such that
A3: ( Ft is one-to-one & rng Ft = Carrier Lt ) and
A4: Sum Lt = Sum (Lt (#) Ft) by RLVECT_2:def 8;
reconsider FFr = Ft as FinSequence of the carrier of RNS2 by A1;
thus Sum Lt = Sum (Lr (#) FFr) by A2, Th12, A1, Th13, A4
.= Sum Lr by A3, A2, RLVECT_2:def 8 ; :: thesis: verum