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 15
.= (Re ((seq . x) *' )) + ((- (Im ((seq . x) *' ))) * <i> )
.= (Re (seq . x)) + ((- (Im ((seq . x) *' ))) * <i> ) by COMPLEX1:112
.= (Re (seq . x)) + ((- (- (Im (seq . x)))) * <i> ) by COMPLEX1:112
.= (Re (seq . x)) + ((Im (seq . x)) * <i> ) ;
hence seq . x = ((seq *' ) *' ) . x by COMPLEX1:29; :: thesis: verum

end;

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