A1: ( dom (pr1 f) = dom f & dom f = Seg (len f) ) by FINSEQ_1:def 3, MCART_1:def 12;
then reconsider p = pr1 f as FinSequence by FINSEQ_1:def 2;
rng p c= X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in X )
assume x in rng p ; :: thesis: x in X
then consider i being set such that
A2: ( i in dom p & x = p . i ) by FUNCT_1:def 5;
( f . i in [:X,Y:] & x = (f . i) `1 ) by A1, A2, Th2, MCART_1:def 12;
hence x in X by MCART_1:10; :: thesis: verum

end;

hence pr1 f is FinSequence of X by FINSEQ_1:def 4; :: thesis: verum