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 *'))) and
A4: w = ((1 / 2) * (z + (z *'))) . x by FUNCT_1:def 3;
reconsider i = x as Element of NAT by A3;
x in Seg (len ((1 / 2) * (z + (z *')))) by A3, FINSEQ_1:def 3;
then A5: ( 1 <= i & i <= len z ) by A2, FINSEQ_1:1;
((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 A4; :: thesis: verum

end;

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