let i, n 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 :: thesis: for x being object holds
( ( x in rng (n proj i) implies x in NAT ) & ( x in NAT implies x in rng (n proj i) ) )
let x be object ; :: thesis: ( ( x in rng (n proj i) implies x in NAT ) & ( x in NAT implies x in rng (n proj i) ) )
thus ( x in rng (n proj i) implies x in NAT ) by ORDINAL1:def 12; :: thesis: ( x in NAT implies x in rng (n proj i) )
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 ;
i in Seg n by A2, A3, FINSEQ_1:1;
then A4: d . i = x9 by FUNCOP_1:7;
(n proj i) . d = d . i by A1, CARD_3:def 16;
hence x in rng (n proj i) by A1, A4, FUNCT_1:def 3; :: thesis: verum
end;
hence rng (n proj i) = NAT by TARSKI:2; :: thesis: verum