let x, y, w, z, a, b, c, d be set ; ( x,y,w,z are_mutually_different implies ( ((x,y,w,z) --> (a,b,c,d)) . x = a & ((x,y,w,z) --> (a,b,c,d)) . y = b & ((x,y,w,z) --> (a,b,c,d)) . w = c & ((x,y,w,z) --> (a,b,c,d)) . z = d ) )
assume A1:
x,y,w,z are_mutually_different
; ( ((x,y,w,z) --> (a,b,c,d)) . x = a & ((x,y,w,z) --> (a,b,c,d)) . y = b & ((x,y,w,z) --> (a,b,c,d)) . w = c & ((x,y,w,z) --> (a,b,c,d)) . z = d )
then A2:
x <> w
by ZFMISC_1:def 6;
A3:
x <> z
by A1, ZFMISC_1:def 6;
A4:
y <> w
by A1, ZFMISC_1:def 6;
A5:
y <> z
by A1, ZFMISC_1:def 6;
A6:
x <> y
by A1, ZFMISC_1:def 6;
A7:
w <> z
by A1, ZFMISC_1:def 6;
set f = (x,y) --> (a,b);
set g = (w,z) --> (c,d);
A8:
((x,y) --> (a,b)) . x = a
by A6, FUNCT_4:63;
A9:
((x,y) --> (a,b)) . y = b
by FUNCT_4:63;
A10:
((w,z) --> (c,d)) . w = c
by A7, FUNCT_4:63;
A11:
((w,z) --> (c,d)) . z = d
by FUNCT_4:63;
A12:
dom ((w,z) --> (c,d)) = {w,z}
by FUNCT_4:62;
then A13:
not x in dom ((w,z) --> (c,d))
by A2, A3, TARSKI:def 2;
A14:
not y in dom ((w,z) --> (c,d))
by A4, A5, A12, TARSKI:def 2;
A15:
w in dom ((w,z) --> (c,d))
by A12, TARSKI:def 2;
z in dom ((w,z) --> (c,d))
by A12, TARSKI:def 2;
hence
( ((x,y,w,z) --> (a,b,c,d)) . x = a & ((x,y,w,z) --> (a,b,c,d)) . y = b & ((x,y,w,z) --> (a,b,c,d)) . w = c & ((x,y,w,z) --> (a,b,c,d)) . z = d )
by A8, A9, A10, A11, A13, A14, A15, FUNCT_4:11, FUNCT_4:13; verum