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

proof

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

end;

hence F = addcomplex .: (F2,F1) by A5, A8, FUNCOP_1:21; :: thesis: verum