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 Def5
.= (Re (seq1 . n)) + (Re (seq2 . n)) by Def5
.= Re ((seq1 . n) + (seq2 . n)) by COMPLEX1:8
.= Re ((seq1 + seq2) . n) by VALUED_1:1
.= (Re (seq1 + seq2)) . n by Def5 ; :: 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 Def6
.= (Im (seq1 . n)) + (Im (seq2 . n)) by Def6
.= Im ((seq1 . n) + (seq2 . n)) by COMPLEX1:8
.= Im ((seq1 + seq2) . n) by VALUED_1:1
.= (Im (seq1 + seq2)) . n by Def6 ; :: thesis: verum

end;

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