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