let RNS1, RNS2 be RealLinearSpace; :: thesis:
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:
let FFr be FinSequence of RNS1; :: thesis:
let fr be Function of RNS1,REAL; :: thesis:
let Fv be FinSequence of RNS2; :: thesis:
let fv be Function of RNS2,REAL; :: thesis:
assume A2: ( fr = fv & FFr = Fv ) ; :: thesis:
then A3: len (fv (#) Fv) = len FFr by RLVECT_2:def 7;
for i being Nat st i in dom (fv (#) Fv) holds
(fv (#) Fv) . i = (fr . (FFr /. i)) * (FFr /. i)

let i be Nat; :: thesis:
assume i in dom (fv (#) Fv) ; :: thesis:
hence (fv (#) Fv) . i = (fv . (Fv /. i)) * (Fv /. i) by RLVECT_2:def 7
.= (fr . (FFr /. i)) * (FFr /. i) by A2, A1 ;
:: thesis:

end;