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