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: (Re (seq (#) (seq *' ))) . n = Re ((seq (#) (seq *' )) . n) by COMSEQ_3:def 3
.= 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:126 ;
( 0 <= (Re z1) ^2 & 0 <= (Im z1) ^2 ) by XREAL_1:65;
then (Re (seq (#) (seq *' ))) . n >= 0 + 0 by A1, XREAL_1:9;
hence (Re (seq (#) (seq *' ))) . n >= 0 ; :: thesis: (Im (seq (#) (seq *' ))) . n = 0
(Im (seq (#) (seq *' ))) . n = Im ((seq (#) (seq *' )) . n) by COMSEQ_3:def 4
.= 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:126; :: thesis: verum