let F1, F2 be FinSequence of REAL ; :: thesis: for j being Nat st len F1 = len F2 holds
(F1 - F2) . j = (F1 . j) - (F2 . j)
let j be Nat; :: thesis: ( len F1 = len F2 implies (F1 - F2) . j = (F1 . j) - (F2 . j) )
reconsider n = len F1 as Element of NAT ;
reconsider G1 = F1 as Element of n -tuples_on REAL by FINSEQ_2:92;
assume len F1 = len F2 ; :: thesis: (F1 - F2) . j = (F1 . j) - (F2 . j)
then reconsider G2 = F2 as Element of n -tuples_on REAL by FINSEQ_2:92;
(G1 - G2) . j = (G1 . j) - (G2 . j) by RVSUM_1:27;
hence (F1 - F2) . j = (F1 . j) - (F2 . j) ; :: thesis: verum