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

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

let n be Element of NAT ; :: thesis: (Re (seq1 (#) seq2)) . n = (((Re seq1) (#) (Re seq2)) - ((Im seq1) (#) (Im seq2))) . n
thus (Re (seq1 (#) seq2)) . n = Re ((seq1 (#) seq2) . n) by Def5
.= Re ((seq1 . n) * (seq2 . n)) by VALUED_1:5
.= Re ((((Re (seq1 . n)) * (Re (seq2 . n))) - ((Im (seq1 . n)) * (Im (seq2 . n)))) + ((((Re (seq1 . n)) * (Im (seq2 . n))) + ((Re (seq2 . n)) * (Im (seq1 . n)))) * <i>)) by COMPLEX1:82
.= ((Re (seq1 . n)) * (Re (seq2 . n))) - ((Im (seq1 . n)) * (Im (seq2 . n))) by COMPLEX1:12
.= (((Re seq1) . n) * (Re (seq2 . n))) - ((Im (seq1 . n)) * (Im (seq2 . n))) by Def5
.= (((Re seq1) . n) * ((Re seq2) . n)) - ((Im (seq1 . n)) * (Im (seq2 . n))) by Def5
.= (((Re seq1) . n) * ((Re seq2) . n)) - ((Im (seq1 . n)) * ((Im seq2) . n)) by Def6
.= (((Re seq1) . n) * ((Re seq2) . n)) - (((Im seq1) . n) * ((Im seq2) . n)) by Def6
.= (((Re seq1) (#) (Re seq2)) . n) - (((Im seq1) . n) * ((Im seq2) . n)) by SEQ_1:8
.= (((Re seq1) (#) (Re seq2)) . n) - (((Im seq1) (#) (Im seq2)) . n) by SEQ_1:8
.= (((Re seq1) (#) (Re seq2)) . n) + (- (((Im seq1) (#) (Im seq2)) . n))
.= (((Re seq1) (#) (Re seq2)) . n) + ((- ((Im seq1) (#) (Im seq2))) . n) by SEQ_1:10
.= (((Re seq1) (#) (Re seq2)) - ((Im seq1) (#) (Im seq2))) . n by SEQ_1:7 ; :: thesis: verum

end;

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

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

let n be Element of NAT ; :: thesis: (Im (seq1 (#) seq2)) . n = (((Re seq1) (#) (Im seq2)) + ((Im seq1) (#) (Re seq2))) . n
thus (Im (seq1 (#) seq2)) . n = Im ((seq1 (#) seq2) . n) by Def6
.= Im ((seq1 . n) * (seq2 . n)) by VALUED_1:5
.= Im ((((Re (seq1 . n)) * (Re (seq2 . n))) - ((Im (seq1 . n)) * (Im (seq2 . n)))) + ((((Re (seq1 . n)) * (Im (seq2 . n))) + ((Re (seq2 . n)) * (Im (seq1 . n)))) * <i>)) by COMPLEX1:82
.= ((Re (seq1 . n)) * (Im (seq2 . n))) + ((Re (seq2 . n)) * (Im (seq1 . n))) by COMPLEX1:12
.= ((Re (seq1 . n)) * (Im (seq2 . n))) + ((Im (seq1 . n)) * ((Re seq2) . n)) by Def5
.= (((Re seq1) . n) * (Im (seq2 . n))) + ((Im (seq1 . n)) * ((Re seq2) . n)) by Def5
.= (((Re seq1) . n) * ((Im seq2) . n)) + ((Im (seq1 . n)) * ((Re seq2) . n)) by Def6
.= (((Re seq1) . n) * ((Im seq2) . n)) + (((Im seq1) . n) * ((Re seq2) . n)) by Def6
.= (((Re seq1) (#) (Im seq2)) . n) + (((Im seq1) . n) * ((Re seq2) . n)) by SEQ_1:8
.= (((Re seq1) (#) (Im seq2)) . n) + (((Im seq1) (#) (Re seq2)) . n) by SEQ_1:8
.= (((Re seq1) (#) (Im seq2)) + ((Im seq1) (#) (Re seq2))) . n by SEQ_1:7 ; :: thesis: verum

end;

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