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