A1: dom (pr1 f) = dom f by MCART_1:def 12;
dom f = Seg (len f) by FINSEQ_1:def 3;
then reconsider p = pr1 f as FinSequence by A1, FINSEQ_1:def 2;
rng p c= X
proof
let x be object ; :: 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 object such that
A2: i in dom p and
A3: x = p . i by FUNCT_1:def 3;
A4: f . i in [:X,Y:] by A1, A2, Th2;
x = (f . i) `1 by A1, A2, A3, MCART_1:def 12;
hence x in X by A4, MCART_1:10; :: thesis: verum
end;
hence pr1 f is FinSequence of X by FINSEQ_1:def 4; :: thesis: verum