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