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 A1: ( a <> b & c <> d & dom h = {a,b,c,d} & h . a = e & h . b = i & h . c = j & 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;
A2: ( dom (a,b --> e,i) = {a,b} & dom (c,d --> j,k) = {c,d} ) by FUNCT_4:65;
then A3: dom h = (dom (a,b --> e,i)) \/ (dom (c,d --> j,k)) by A1, 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 A4: 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 A5: x in dom (c,d --> j,k) ; :: thesis: h . x = (c,d --> j,k) . x

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

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

hence h . x = (c,d --> j,k) . x by A1, 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 A1, 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 A6: x in dom (a,b --> e,i) by A4, XBOOLE_0:def 3;

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

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

hence h . x = (a,b --> e,i) . x by A1, 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 A1, FUNCT_4:66; :: thesis: verum

end;

end;

end;

end;

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