let a, b, c, x, y, z, w, d be object ; :: thesis: ((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; :: thesis: verum