let a, b, c, d be set ; :: thesis: for g being Function st dom g = {a,b} & g . a = c & g . b = d holds
g = a,b --> c,d
let h be Function; :: thesis: ( dom h = {a,b} & h . a = c & h . b = d implies h = a,b --> c,d )
assume A1: ( dom h = {a,b} & h . a = c & h . b = d ) ; :: thesis: h = a,b --> c,d
set f = {a} --> c;
set g = {b} --> d;
A2: ( a in {a} & b in {b} ) by TARSKI:def 1;
( dom ({a} --> c) = {a} & dom ({b} --> d) = {b} ) by FUNCOP_1:19;
then A4: dom h = (dom ({a} --> c)) \/ (dom ({b} --> d)) by A1, ENUMSET1:41;

now

let x be set ; :: thesis: ( x in (dom ({a} --> c)) \/ (dom ({b} --> d)) implies ( ( x in dom ({b} --> d) implies h . x = ({b} --> d) . x ) & ( not x in dom ({b} --> d) implies h . x = ({a} --> c) . x ) ) )
assume A5: x in (dom ({a} --> c)) \/ (dom ({b} --> d)) ; :: thesis: ( ( x in dom ({b} --> d) implies h . x = ({b} --> d) . x ) & ( not x in dom ({b} --> d) implies h . x = ({a} --> c) . x ) )
thus ( x in dom ({b} --> d) implies h . x = ({b} --> d) . x ) :: thesis: ( not x in dom ({b} --> d) implies h . x = ({a} --> c) . x )

proof

assume x in dom ({b} --> d) ; :: thesis: h . x = ({b} --> d) . x
then x = b by TARSKI:def 1;
hence h . x = ({b} --> d) . x by A1, A2, FUNCOP_1:13; :: thesis: verum

end;

assume not x in dom ({b} --> d) ; :: thesis: h . x = ({a} --> c) . x
then x in dom ({a} --> c) by A5, XBOOLE_0:def 3;
then x = a by TARSKI:def 1;
hence h . x = ({a} --> c) . x by A1, A2, FUNCOP_1:13; :: thesis: verum

end;

hence h = a,b --> c,d by A4, Def1; :: thesis: verum