let x, y, w, z, a, b, c, d be set ; :: thesis: ( 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 x,y,w,z are_mutually_different ; :: thesis: ( (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 A1: ( x <> w & x <> z & y <> w & y <> z & w <> y & z <> y & x <> y & w <> z ) by ZFMISC_1:def 6;
set f = x,y --> a,b;
set g = w,z --> c,d;
A2: ( (x,y --> a,b) . x = a & (x,y --> a,b) . y = b & (w,z --> c,d) . w = c & (w,z --> c,d) . z = d ) by A1, FUNCT_4:66;
A3: ( dom (x,y --> a,b) = {x,y} & dom (w,z --> c,d) = {w,z} ) by FUNCT_4:65;
then A4: not x in dom (w,z --> c,d) by A1, TARSKI:def 2;
A5: not y in dom (w,z --> c,d) by A1, A3, TARSKI:def 2;
A6: w in dom (w,z --> c,d) by A3, TARSKI:def 2;
z in dom (w,z --> c,d) by A3, 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 A2, A4, A5, A6, FUNCT_4:12, FUNCT_4:14; :: thesis: verum