reconsider F3 = F1, F4 = F2 as FinSequence of REAL by Lm2;
let F be FinSequence of REAL ; ( F = F1 - F2 iff F = diffreal .: (F1,F2) )
A1:
dom (F1 - F2) = (dom F1) /\ (dom F2)
by VALUED_1:12;
dom diffreal = [:REAL,REAL:]
by FUNCT_2:def 1;
then A2:
[:(rng F3),(rng F4):] c= dom diffreal
by ZFMISC_1:96;
then A3:
dom (diffreal .: (F1,F2)) = (dom F1) /\ (dom F2)
by FUNCOP_1:69;
thus
( F = F1 - F2 implies F = diffreal .: (F1,F2) )
( F = diffreal .: (F1,F2) implies F = F1 - F2 )
assume A5:
F = diffreal .: (F1,F2)
; F = F1 - F2
hence
F = F1 - F2
by A1, A2, A5, FUNCOP_1:69, VALUED_1:14; verum