A1: len z = len (z *' ) by Def1;
A2: len ((1 / 2) * (z + (z *' ))) = len (z + (z *' )) by Th3
.= len z by A1, Th6 ;
rng ((1 / 2) * (z + (z *' ))) c= REAL

proof

let w be set ; :: according to TARSKI:def 3 :: thesis: ( not w in rng ((1 / 2) * (z + (z *' ))) or w in REAL )
assume w in rng ((1 / 2) * (z + (z *' ))) ; :: thesis: w in REAL
then consider x being set such that
A3: ( x in dom ((1 / 2) * (z + (z *' ))) & w = ((1 / 2) * (z + (z *' ))) . x ) by FUNCT_1:def 5;
A4: x in Seg (len ((1 / 2) * (z + (z *' )))) by A3, FINSEQ_1:def 3;
reconsider i = x as Element of NAT by A3;
A5: ( 1 <= i & i <= len z ) by A2, A4, FINSEQ_1:3;
((1 / 2) * (z + (z *' ))) . i = (1 / 2) * ((z + (z *' )) . i) by Th16
.= (1 / 2) * ((z . i) + ((z *' ) . i)) by A1, Th26
.= (1 / 2) * ((z . i) + ((z . i) *' )) by A5, Def1
.= (1 / 2) * (2 * (Re (z . i))) by Th24 ;
hence w in REAL by A3; :: thesis: verum

end;

hence (1 / 2) * (z + (z *' )) is FinSequence of REAL by FINSEQ_1:def 4; :: thesis: verum