let a, b, c, x, y, z, w, d be object ; ( w <> z implies ((x,y,w,z) --> (a,b,c,d)) . w = c )
assume A1:
w <> z
; ((x,y,w,z) --> (a,b,c,d)) . w = c
A2:
w <> z
by A1;
set f = (x,y) --> (a,b);
set g = (w,z) --> (c,d);
A3:
((w,z) --> (c,d)) . w = c
by A2, Th63;
A4:
dom ((w,z) --> (c,d)) = {w,z}
by Th62;
A5:
w in dom ((w,z) --> (c,d))
by A4, TARSKI:def 2;
thus
((x,y,w,z) --> (a,b,c,d)) . w = c
by A3, A5, Th13; verum