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:96;
then A3: dom (diffcomplex .: (z1,z2)) = (dom z1) /\ (dom z2) by FUNCOP_1:69;
A4: dom (z1 - z2) = (dom z1) /\ (dom z2) by VALUED_1:12;

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

let x be object ; :: thesis: ( x in dom (z1 - z2) implies (z1 - z2) . x = (diffcomplex .: (z1,z2)) . x )
assume A5: 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 A4, A3, A5, FUNCOP_1:22 ;
:: thesis: verum

end;

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