let seq be Complex_Sequence; :: thesis: for h being PartFunc of COMPLEX,COMPLEX st rng seq c= dom h holds
- (h /* seq) = (- h) /* seq
let h be PartFunc of COMPLEX,COMPLEX; :: thesis: ( rng seq c= dom h implies - (h /* seq) = (- h) /* seq )
assume A1: rng seq c= dom h ; :: thesis: - (h /* seq) = (- h) /* seq
thus - (h /* seq) = (- 1r) (#) (h /* seq) by COMSEQ_1:11
.= ((- 1r) (#) h) /* seq by A1, Th19
.= (- h) /* seq by CFUNCT_1:31 ; :: thesis: verum