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 F be FinSequence of RNS1; :: thesis:
let Fv be FinSequence of RNS2; :: thesis:
assume A2: F = Fv ; :: thesis:
set T = RNS1;
set V = RNS2;
consider f being sequence of the carrier of RNS1 such that
A3: Sum F = f . (len F) and
A4: f . 0 = 0. RNS1 and
A5: for j being Nat
for v being Element of RNS1 st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v by RLVECT_1:def 12;
consider fv being sequence of the carrier of RNS2 such that
A6: Sum Fv = fv . (len Fv) and
A7: fv . 0 = 0. RNS2 and
A8: for j being Nat
for v being Element of RNS2 st j < len Fv & v = Fv . (j + 1) holds
fv . (j + 1) = (fv . j) + v by RLVECT_1:def 12;
defpred S₁[ Nat] means ( $1 <= len F implies f . $1 = fv . $1 );
A9: for i being Nat st S₁[i] holds
S₁[i + 1]

end;