set g = addcomplex .: z1,z2;
dom addcomplex = [:COMPLEX ,COMPLEX :] by FUNCT_2:def 1;
then [:(rng z1),(rng z2):] c= dom addcomplex by ZFMISC_1:119;
then A1: ( dom (z1 + z2) = (dom z1) /\ (dom z2) & dom (addcomplex .: z1,z2) = (dom z1) /\ (dom z2) ) by FUNCOP_1:84, VALUED_1:def 1;

now

let x be set ; :: thesis: ( x in dom (z1 + z2) implies (z1 + z2) . x = (addcomplex .: z1,z2) . x )
A2: ( z1 . x is Element of COMPLEX & z2 . x is Element of COMPLEX ) by XCMPLX_0:def 2;
assume A3: x in dom (z1 + z2) ; :: thesis: (z1 + z2) . x = (addcomplex .: z1,z2) . x
hence (z1 + z2) . x = (z1 . x) + (z2 . x) by VALUED_1:def 1
.= addcomplex . (z1 . x),(z2 . x) by A2, BINOP_2:def 3
.= (addcomplex .: z1,z2) . x by A1, A3, FUNCOP_1:28 ;
:: thesis: verum

end;

hence for b₁ being FinSequence of COMPLEX holds
( b₁ = z1 + z2 iff b₁ = addcomplex .: z1,z2 ) by A1, FUNCT_1:9; :: thesis: verum