let n, i be Element of NAT ; :: thesis: ( dom (n proj i) = n -tuples_on NAT & ( 1 <= i & i <= n implies rng (n proj i) = NAT ) )
thus A1: dom (n proj i) = product (n |-> NAT) by CARD_3:def 16
.= n -tuples_on NAT by FINSEQ_3:131 ; :: thesis: ( 1 <= i & i <= n implies rng (n proj i) = NAT )
assume that
A2: 1 <= i and
A3: i <= n ; :: thesis: rng (n proj i) = NAT

now

let x be set ; :: thesis: ( ( x in rng (n proj i) implies x in NAT ) & ( x in NAT implies x in rng (n proj i) ) )

hereby :: thesis: ( x in NAT implies x in rng (n proj i) )

assume x in rng (n proj i) ; :: thesis: x in NAT
then consider d being set such that
d in dom (n proj i) and
A5: x = (n proj i) . d by FUNCT_1:def 3;
thus x in NAT by A5; :: thesis: verum

end;

assume x in NAT ; :: thesis: x in rng (n proj i)
then reconsider x9 = x as Element of NAT ;
reconsider d = n |-> x9 as FinSequence of NAT by FINSEQ_2:63;
i in Seg n by A2, A3, FINSEQ_1:1;
then A6: d . i = x9 by FUNCOP_1:7;
A7: d is Element of n -tuples_on NAT by FINSEQ_2:112;
then (n proj i) . d = d . i by A1, CARD_3:def 16;
hence x in rng (n proj i) by A1, A7, A6, FUNCT_1:def 3; :: thesis: verum

end;

hence rng (n proj i) = NAT by TARSKI:1; :: thesis: verum