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