A1: len z = len (z *') by Def1;
A2: len ((- ((1 / 2) * <i>)) * (z - (z *'))) = len (z - (z *')) by Th3
.= len z by A1, Th7 ;
rng ((- ((1 / 2) * <i>)) * (z - (z *'))) c= REAL

proof

let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in rng ((- ((1 / 2) * <i>)) * (z - (z *'))) or w in REAL )
assume w in rng ((- ((1 / 2) * <i>)) * (z - (z *'))) ; :: thesis: w in REAL
then consider x being object such that
A3: x in dom ((- ((1 / 2) * <i>)) * (z - (z *'))) and
A4: w = ((- ((1 / 2) * <i>)) * (z - (z *'))) . x by FUNCT_1:def 3;
reconsider i = x as Element of NAT by A3;
x in Seg (len ((- ((1 / 2) * <i>)) * (z - (z *')))) by A3, FINSEQ_1:def 3;
then A5: ( 1 <= i & i <= len z ) by A2, FINSEQ_1:1;
((- ((1 / 2) * <i>)) * (z - (z *'))) . i = (- ((1 / 2) * <i>)) * ((z - (z *')) . i) by Th12
.= (- ((1 / 2) * <i>)) * ((z . i) - ((z *') . i)) by A1, Th21
.= (- ((1 / 2) * <i>)) * ((z . i) - ((z . i) *')) by A5, Def1
.= (- ((1 / 2) * <i>)) * ((2 * (Im (z . i))) * <i>) by Th23 ;
hence w in REAL by A4; :: thesis: verum

end;

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