consider u, w being object such that
A1:
u in f
and
A2:
w in f
and
A3:
u <> w
by ZFMISC_1:def 10;
consider u1, u2 being object such that
A4:
u = [u1,u2]
by A1, RELAT_1:def 1;
consider w1, w2 being object such that
A5:
w = [w1,w2]
by A2, RELAT_1:def 1;
take
u1
; ZFMISC_1:def 10 ex b1 being object st
( u1 in dom f & b1 in dom f & not u1 = b1 )
take
w1
; ( u1 in dom f & w1 in dom f & not u1 = w1 )
thus
( u1 in dom f & w1 in dom f )
by A4, A5, A1, A2, XTUPLE_0:def 12; not u1 = w1
thus
u1 <> w1
by A1, A2, A3, A4, A5, Def1; verum