let seq be Complex_Sequence; :: thesis: seq = (seq *') *'
for x being set st x in NAT holds
seq . x = ((seq *') *') . x

proof

let x be set ; :: thesis: ( x in NAT implies seq . x = ((seq *') *') . x )
assume x in NAT ; :: thesis: seq . x = ((seq *') *') . x
then reconsider x = x as Element of NAT ;
((seq *') *') . x = ((seq *') . x) *' by COMSEQ_2:def 2
.= ((seq . x) *') *' by COMSEQ_2:def 2
.= (Re ((seq . x) *')) - ((Im ((seq . x) *')) * <i>) by COMPLEX1:def 11
.= (Re ((seq . x) *')) + ((- (Im ((seq . x) *'))) * <i>)
.= (Re (seq . x)) + ((- (Im ((seq . x) *'))) * <i>) by COMPLEX1:27
.= (Re (seq . x)) + ((- (- (Im (seq . x)))) * <i>) by COMPLEX1:27
.= (Re (seq . x)) + ((Im (seq . x)) * <i>) ;
hence seq . x = ((seq *') *') . x by COMPLEX1:13; :: thesis: verum

end;

hence seq = (seq *') *' by FUNCT_2:12; :: thesis: verum