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:14
.= ((- 1r ) (#) h) /* seq by A1, Th19
.= (- h) /* seq by CFUNCT_1:40 ; :: thesis: verum