set g = diffcomplex .: z1,z2;
dom diffcomplex = [:COMPLEX ,COMPLEX :] by FUNCT_2:def 1;
then [:(rng z1),(rng z2):] c= dom diffcomplex by ZFMISC_1:119;
then A4: dom (diffcomplex .: z1,z2) = (dom z1) /\ (dom z2) by FUNCOP_1:84;
A5: dom (z1 - z2) = (dom z1) /\ (dom z2) by VALUED_1:12;

now

let x be set ; :: thesis: ( x in dom (z1 - z2) implies (z1 - z2) . x = (diffcomplex .: z1,z2) . x )
assume A7: x in dom (z1 - z2) ; :: thesis: (z1 - z2) . x = (diffcomplex .: z1,z2) . x
hence (z1 - z2) . x = (z1 . x) - (z2 . x) by VALUED_1:13
.= diffcomplex . (z1 . x),(z2 . x) by BINOP_2:def 4
.= (diffcomplex .: z1,z2) . x by A5, A4, A7, FUNCOP_1:28 ;
:: thesis: verum

end;

hence for b₁ being FinSequence of COMPLEX holds
( b₁ = z1 - z2 iff b₁ = diffcomplex .: z1,z2 ) by A4, FUNCT_1:9, VALUED_1:12; :: thesis: verum