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