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