let a, b, c, d, e, i, j, k be set ; :: thesis: for g being Function st a <> b & c <> d & dom g = {a,b,c,d} & g . a = e & g . b = i & g . c = j & g . d = k holds
g = (a,b,c,d) --> (e,i,j,k)
let h be Function; :: thesis: ( a <> b & c <> d & dom h = {a,b,c,d} & h . a = e & h . b = i & h . c = j & h . d = k implies h = (a,b,c,d) --> (e,i,j,k) )
assume that
A1: a <> b and
A2: c <> d and
A3: dom h = {a,b,c,d} and
A4: h . a = e and
A5: h . b = i and
A6: h . c = j and
A7: h . d = k ; :: thesis: h = (a,b,c,d) --> (e,i,j,k)
set f = (a,b) --> (e,i);
set g = (c,d) --> (j,k);
A8: dom ((a,b) --> (e,i)) = {a,b} by FUNCT_4:65;
A9: dom ((c,d) --> (j,k)) = {c,d} by FUNCT_4:65;
then A10: dom h = (dom ((a,b) --> (e,i))) \/ (dom ((c,d) --> (j,k))) by A3, A8, ENUMSET1:45;

now

let x be set ; :: thesis: ( x in (dom ((a,b) --> (e,i))) \/ (dom ((c,d) --> (j,k))) implies ( ( x in dom ((c,d) --> (j,k)) implies h . x = ((c,d) --> (j,k)) . x ) & ( not x in dom ((c,d) --> (j,k)) implies h . x = ((a,b) --> (e,i)) . x ) ) )
assume A11: x in (dom ((a,b) --> (e,i))) \/ (dom ((c,d) --> (j,k))) ; :: thesis: ( ( x in dom ((c,d) --> (j,k)) implies h . x = ((c,d) --> (j,k)) . x ) & ( not x in dom ((c,d) --> (j,k)) implies h . x = ((a,b) --> (e,i)) . x ) )
thus ( x in dom ((c,d) --> (j,k)) implies h . x = ((c,d) --> (j,k)) . x ) :: thesis: ( not x in dom ((c,d) --> (j,k)) implies h . x = ((a,b) --> (e,i)) . x )

proof

assume A12: x in dom ((c,d) --> (j,k)) ; :: thesis: h . x = ((c,d) --> (j,k)) . x

per cases ( x = c or x = d ) by A9, A12, TARSKI:def 2;

suppose x = c ; :: thesis: h . x = ((c,d) --> (j,k)) . x

hence h . x = ((c,d) --> (j,k)) . x by A2, A6, FUNCT_4:66; :: thesis: verum

end;

suppose x = d ; :: thesis: h . x = ((c,d) --> (j,k)) . x

hence h . x = ((c,d) --> (j,k)) . x by A7, FUNCT_4:66; :: thesis: verum

end;

end;

end;

thus ( not x in dom ((c,d) --> (j,k)) implies h . x = ((a,b) --> (e,i)) . x ) :: thesis: verum

proof

assume not x in dom ((c,d) --> (j,k)) ; :: thesis: h . x = ((a,b) --> (e,i)) . x
then A13: x in dom ((a,b) --> (e,i)) by A11, XBOOLE_0:def 3;

per cases ( x = a or x = b ) by A8, A13, TARSKI:def 2;

suppose x = a ; :: thesis: h . x = ((a,b) --> (e,i)) . x

hence h . x = ((a,b) --> (e,i)) . x by A1, A4, FUNCT_4:66; :: thesis: verum

end;

suppose x = b ; :: thesis: h . x = ((a,b) --> (e,i)) . x

hence h . x = ((a,b) --> (e,i)) . x by A5, FUNCT_4:66; :: thesis: verum

end;

end;

end;

end;

hence h = (a,b,c,d) --> (e,i,j,k) by A10, FUNCT_4:def 1; :: thesis: verum