let F be FinSequence of REAL ; for F1, F2 being real-valued FinSequence st F = addreal .: (F1,F2) holds
F = addreal .: (F2,F1)
let F1, F2 be real-valued FinSequence; ( F = addreal .: (F1,F2) implies F = addreal .: (F2,F1) )
assume A5:
F = addreal .: (F1,F2)
; F = addreal .: (F2,F1)
reconsider F1 = F1, F2 = F2 as FinSequence of REAL by Lm2;
A6:
dom addreal = [:REAL,REAL:]
by FUNCT_2:def 1;
then A7:
[:(rng F2),(rng F1):] c= dom addreal
by ZFMISC_1:96;
[:(rng F1),(rng F2):] c= dom addreal
by A6, ZFMISC_1:96;
then A8: dom (addreal .: (F1,F2)) =
(dom F1) /\ (dom F2)
by FUNCOP_1:69
.=
dom (addreal .: (F2,F1))
by A7, FUNCOP_1:69
;
for z being set st z in dom (addreal .: (F2,F1)) holds
F . z = addreal . ((F2 . z),(F1 . z))
hence
F = addreal .: (F2,F1)
by A5, A8, FUNCOP_1:21; verum