let F1, F2 be FinSequence of REAL ; :: thesis: ( len F1 = len F2 & F1 - F2 = 0* (len F1) implies F1 = F2 )
set n = len F1;
assume len F1 = len F2 ; :: thesis: ( not F1 - F2 = 0* (len F1) or F1 = F2 )
then reconsider R1 = F1, R2 = F2 as Element of (len F1) -tuples_on REAL by FINSEQ_2:92;
( R1 - R2 = (len F1) |-> 0 implies R1 = R2 ) by RVSUM_1:38;
hence ( not F1 - F2 = 0* (len F1) or F1 = F2 ) by EUCLID:def 4; :: thesis: verum