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