let n be Nat; :: thesis: for nt, nt1 being Element of n -tuples_on NAT st rng nt = rng nt1 & nt is one-to-one holds
nt1 is one-to-one
let nt, nt1 be Element of n -tuples_on NAT; :: thesis: ( rng nt = rng nt1 & nt is one-to-one implies nt1 is one-to-one )
assume that
A1: rng nt = rng nt1 and
A2: nt is one-to-one ; :: thesis: nt1 is one-to-one
A3: len nt1 = n by CARD_1:def 7;
len nt = n by CARD_1:def 7;
hence nt1 is one-to-one by A1, A2, A3, FINSEQ_4:61; :: thesis: verum