let seq be Complex_Sequence; :: thesis: for n being Nat holds
( (Re (seq (#) (seq *'))) . n >= 0 & (Im (seq (#) (seq *'))) . n = 0 )
let n be Nat; :: thesis: ( (Re (seq (#) (seq *'))) . n >= 0 & (Im (seq (#) (seq *'))) . n = 0 )
A1: n in NAT by ORDINAL1:def 12;
then reconsider nn = n as Element of NAT ;
reconsider z1 = seq . nn as Element of COMPLEX ;
A2: ( 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, A1
.= ((Re z1) ^2) + ((Im z1) ^2) by COMPLEX1:40 ;
then (Re (seq (#) (seq *'))) . n >= 0 + 0 by A2;
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, A1 ;
hence (Im (seq (#) (seq *'))) . n = 0 by COMPLEX1:40; :: thesis: verum