set f = z *' ;
A1: dom (z *') = dom z by COMSEQ_2:def 1;
ex n being Nat st dom z = Seg n by FINSEQ_1:def 2;
then A2: z *' is FinSequence by A1, FINSEQ_1:def 2;
rng (z *') c= COMPLEX
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (z *') or y in COMPLEX )
thus ( not y in rng (z *') or y in COMPLEX ) by XCMPLX_0:def 2; :: thesis: verum
end;
hence z *' is FinSequence of COMPLEX by A2, FINSEQ_1:def 4; :: thesis: verum