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