let seq1, seq2 be Complex_Sequence; :: thesis: ( (Re seq1) - (Re seq2) = Re (seq1 - seq2) & (Im seq1) - (Im seq2) = Im (seq1 - seq2) )

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

let n be Element of NAT ; :: thesis: ((Re seq1) - (Re seq2)) . n = (Re (seq1 - seq2)) . n
thus ((Re seq1) - (Re seq2)) . n = ((Re seq1) . n) + ((- (Re seq2)) . n) by SEQ_1:7
.= ((Re seq1) . n) + ((Re (- seq2)) . n) by Th16
.= ((Re seq1) + (Re (- seq2))) . n by SEQ_1:7
.= (Re (seq1 - seq2)) . n by Th15 ; :: thesis: verum

end;

hence (Re seq1) - (Re seq2) = Re (seq1 - seq2) ; :: thesis: (Im seq1) - (Im seq2) = Im (seq1 - seq2)

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

let n be Element of NAT ; :: thesis: ((Im seq1) - (Im seq2)) . n = (Im (seq1 - seq2)) . n
thus ((Im seq1) - (Im seq2)) . n = ((Im seq1) . n) + ((- (Im seq2)) . n) by SEQ_1:7
.= ((Im seq1) . n) + ((Im (- seq2)) . n) by Th16
.= ((Im seq1) + (Im (- seq2))) . n by SEQ_1:7
.= (Im (seq1 - seq2)) . n by Th15 ; :: thesis: verum

end;

hence (Im seq1) - (Im seq2) = Im (seq1 - seq2) ; :: thesis: verum