A5: dom (pr2 f) = dom f by MCART_1:def 13;
dom f = Seg (len f) by FINSEQ_1:def 3;
then reconsider p = pr2 f as FinSequence by A5, FINSEQ_1:def 2;
rng p c= Y

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in Y )
assume x in rng p ; :: thesis: x in Y
then consider i being object such that
A6: i in dom p and
A7: x = p . i by FUNCT_1:def 3;
A8: f . i in [:X,Y:] by A5, A6, Th2;
x = (f . i) `2 by A5, A6, A7, MCART_1:def 13;
hence x in Y by A8, MCART_1:10; :: thesis: verum

end;

hence pr2 f is FinSequence of Y by FINSEQ_1:def 4; :: thesis: verum