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 A1: ( rng nt = rng nt1 & nt is without_repeated_line ) ; :: thesis: nt1 is without_repeated_line
( len nt = n & len nt1 = n ) by FINSEQ_2:109;
hence nt1 is without_repeated_line by A1, FINSEQ_4:76; :: thesis: verum