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

proof

let x be set ; :: 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 set such that
A4: ( i in dom p & x = p . i ) by FUNCT_1:def 5;
( f . i in [:X,Y:] & x = (f . i) `2 ) by A3, A4, Th2, MCART_1:def 13;
hence x in Y by MCART_1:10; :: thesis: verum

end;

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