let seq be Complex_Sequence; :: thesis: ( - (Re seq) = Re (- seq) & - (Im seq) = Im (- seq) )

now

let n be Element of NAT ; :: thesis: (- (Re seq)) . n = (Re (- seq)) . n
thus (- (Re seq)) . n = - ((Re seq) . n) by SEQ_1:14
.= - (Re (seq . n)) by Def3
.= Re (- (seq . n)) by COMPLEX1:34
.= Re ((- seq) . n) by VALUED_1:8
.= (Re (- seq)) . n by Def3 ; :: thesis: verum

end;

hence - (Re seq) = Re (- seq) by FUNCT_2:113; :: thesis: - (Im seq) = Im (- seq)

now

let n be Element of NAT ; :: thesis: (- (Im seq)) . n = (Im (- seq)) . n
thus (- (Im seq)) . n = - ((Im seq) . n) by SEQ_1:14
.= - (Im (seq . n)) by Def4
.= Im (- (seq . n)) by COMPLEX1:34
.= Im ((- seq) . n) by VALUED_1:8
.= (Im (- seq)) . n by Def4 ; :: thesis: verum

end;

hence - (Im seq) = Im (- seq) by FUNCT_2:113; :: thesis: verum