let x be set ; :: thesis: for n, m being Nat st n |-> x = m |-> x holds
n = m
let n, m be Nat; :: thesis: ( n |-> x = m |-> x implies n = m )
len (n |-> x) = n by FINSEQ_1:def 18;
hence ( n |-> x = m |-> x implies n = m ) by FINSEQ_1:def 18; :: thesis: verum