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

now :: thesis: for n being Element of NAT holds (- (Re seq)) . n = (Re (- seq)) . n

let n be Element of NAT ; :: thesis: (- (Re seq)) . n = (Re (- seq)) . n
thus (- (Re seq)) . n = - ((Re seq) . n) by SEQ_1:10
.= - (Re (seq . n)) by Def5
.= Re (- (seq . n)) by COMPLEX1:17
.= Re ((- seq) . n) by VALUED_1:8
.= (Re (- seq)) . n by Def5 ; :: thesis: verum

end;

hence - (Re seq) = Re (- seq) ; :: thesis: - (Im seq) = Im (- seq)

now :: thesis: for n being Element of NAT holds (- (Im seq)) . n = (Im (- seq)) . n

let n be Element of NAT ; :: thesis: (- (Im seq)) . n = (Im (- seq)) . n
thus (- (Im seq)) . n = - ((Im seq) . n) by SEQ_1:10
.= - (Im (seq . n)) by Def6
.= Im (- (seq . n)) by COMPLEX1:17
.= Im ((- seq) . n) by VALUED_1:8
.= (Im (- seq)) . n by Def6 ; :: thesis: verum

end;

hence - (Im seq) = Im (- seq) ; :: thesis: verum