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 set ; :: 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 set such that
A3: x in dom ((- ((1 / 2) * <i> )) * (z - (z *' ))) and
A4: w = ((- ((1 / 2) * <i> )) * (z - (z *' ))) . x by FUNCT_1:def 5;
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:3;
((- ((1 / 2) * <i> )) * (z - (z *' ))) . i = (- ((1 / 2) * <i> )) * ((z - (z *' )) . i) by Th16
.= (- ((1 / 2) * <i> )) * ((z . i) - ((z *' ) . i)) by A1, Th25
.= (- ((1 / 2) * <i> )) * ((z . i) - ((z . i) *' )) by A5, Def1
.= (- ((1 / 2) * <i> )) * ((2 * (Im (z . i))) * <i> ) by Th27 ;
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