let seq be Complex_Sequence; :: thesis: for n being Element of NAT holds
( (Re (seq (#) (seq *'))) . n >= 0 & (Im (seq (#) (seq *'))) . n = 0 )
let n be Element of NAT ; :: thesis: ( (Re (seq (#) (seq *'))) . n >= 0 & (Im (seq (#) (seq *'))) . n = 0 )
reconsider z1 = seq . n as Element of COMPLEX ;
A1: ( 0 <= (Re z1) ^2 & 0 <= (Im z1) ^2 ) by XREAL_1:63;
(Re (seq (#) (seq *'))) . n = Re ((seq (#) (seq *')) . n) by COMSEQ_3:def 5
.= Re ((seq . n) * ((seq *') . n)) by VALUED_1:5
.= Re ((seq . n) * ((seq . n) *')) by COMSEQ_2:def 2
.= ((Re z1) ^2) + ((Im z1) ^2) by COMPLEX1:40 ;
then (Re (seq (#) (seq *'))) . n >= 0 + 0 by A1, XREAL_1:7;
hence (Re (seq (#) (seq *'))) . n >= 0 ; :: thesis: (Im (seq (#) (seq *'))) . n = 0
(Im (seq (#) (seq *'))) . n = Im ((seq (#) (seq *')) . n) by COMSEQ_3:def 6
.= Im ((seq . n) * ((seq *') . n)) by VALUED_1:5
.= Im ((seq . n) * ((seq . n) *')) by COMSEQ_2:def 2 ;
hence (Im (seq (#) (seq *'))) . n = 0 by COMPLEX1:40; :: thesis: verum