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:66;
A9:
(x,y --> a,b) . y = b
by FUNCT_4:66;
A10:
(w,z --> c,d) . w = c
by A7, FUNCT_4:66;
A11:
(w,z --> c,d) . z = d
by FUNCT_4:66;
A12:
dom (w,z --> c,d) = {w,z}
by FUNCT_4:65;
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:12, FUNCT_4:14; verum