set g = compcomplex * z;
dom compcomplex = COMPLEX by FUNCT_2:def 1;
then rng z c= dom compcomplex ;
then A1: dom (compcomplex * z) = dom z by RELAT_1:27;
A2: dom (- z) = dom z by VALUED_1:8;

now :: thesis: for x being object st x in dom (- z) holds
(- z) . x = (compcomplex * z) . x

let x be object ; :: thesis: ( x in dom (- z) implies (- z) . x = (compcomplex * z) . x )
assume A3: x in dom (- z) ; :: thesis: (- z) . x = (compcomplex * z) . x
thus (- z) . x = - (z . x) by VALUED_1:8
.= compcomplex . (z . x) by BINOP_2:def 1
.= (compcomplex * z) . x by A2, A1, A3, FUNCT_1:12 ; :: thesis: verum

end;

hence for b₁ being FinSequence of COMPLEX holds
( b₁ = - z iff b₁ = compcomplex * z ) by A1, FUNCT_1:2, VALUED_1:8; :: thesis: verum