let X be non empty set ; :: thesis: for n1, n2 being Nat st X --> n1 = X --> n2 holds
n1 = n2
let n1, n2 be Nat; :: thesis: ( X --> n1 = X --> n2 implies n1 = n2 )
assume A1: X --> n1 = X --> n2 ; :: thesis: n1 = n2
{n1} = rng (X --> n1) by FUNCOP_1:8
.= rng (X --> n2) by A1
.= {n2} by FUNCOP_1:8 ;
hence n1 = n2 by ZFMISC_1:3; :: thesis: verum