A1: len z = len (z *') by Def1;
A2: len ((- ((1 / 2) * <i>)) * (z - (z *'))) = len (z - (z *')) by Th3
.= len z by ;
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:
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 ;
then A5: ( 1 <= i & i <= len z ) by ;
((- ((1 / 2) * <i>)) * (z - (z *'))) . i = (- ((1 / 2) * <i>)) * ((z - (z *')) . i) by Th12
.= (- ((1 / 2) * <i>)) * ((z . i) - ((z *') . i)) by
.= (- ((1 / 2) * <i>)) * ((z . i) - ((z . i) *')) by
.= (- ((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