let x be FinSequence of COMPLEX ; :: thesis: ( len (Re x) = len x & len (Im x) = len x )

A1: len x = len (x *') by Def1;

A2: len (Im x) = len (x - (x *')) by Th3

.= len x by A1, Th7 ;

len (Re x) = len (x + (x *')) by Th3

.= len x by A1, Th6 ;

hence ( len (Re x) = len x & len (Im x) = len x ) by A2; :: thesis: verum

A1: len x = len (x *') by Def1;

A2: len (Im x) = len (x - (x *')) by Th3

.= len x by A1, Th7 ;

len (Re x) = len (x + (x *')) by Th3

.= len x by A1, Th6 ;

hence ( len (Re x) = len x & len (Im x) = len x ) by A2; :: thesis: verum