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:96;
then A1: ( dom (z1 + z2) = (dom z1) /\ (dom z2) & dom (addcomplex .: (z1,z2)) = (dom z1) /\ (dom z2) ) by FUNCOP_1:69, VALUED_1:def 1;

now :: thesis: for x being object st x in dom (z1 + z2) holds
(z1 + z2) . x = (addcomplex .: (z1,z2)) . x

let x be object ; :: thesis: ( x in dom (z1 + z2) implies (z1 + z2) . x = (addcomplex .: (z1,z2)) . x )
assume A2: 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 BINOP_2:def 3
.= (addcomplex .: (z1,z2)) . x by A1, A2, FUNCOP_1:22 ;
:: thesis: verum

end;

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