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

proof

let z be set ; :: thesis: ( z in dom (addreal .: F2,F1) implies F . z = addreal . (F2 . z),(F1 . z) )
assume z in dom (addreal .: F2,F1) ; :: thesis: F . z = addreal . (F2 . z),(F1 . z)
hence F . z = addreal . (F1 . z),(F2 . z) by A5, A8, FUNCOP_1:28
.= (F1 . z) + (F2 . z) by BINOP_2:def 9
.= addreal . (F2 . z),(F1 . z) by BINOP_2:def 9 ;
:: thesis: verum

end;

hence F = addreal .: F2,F1 by A5, A8, FUNCOP_1:27; :: thesis: verum