let a, b, c, d be object ; :: 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 that
A1: dom h = {a,b} and
A2: h . a = c and
A3: h . b = d ; :: thesis: h = (a,b) --> (c,d)
set f = {a} --> c;
set g = {b} --> d;
A4: b in {b} by TARSKI:def 1;
A5: a in {a} by TARSKI:def 1;
A6: now :: thesis: for x being object st x in (dom ({a} --> c)) \/ (dom ({b} --> d)) holds
( ( x in dom ({b} --> d) implies h . x = ({b} --> d) . x ) & ( not x in dom ({b} --> d) implies h . x = ({a} --> c) . x ) )
let x be object ; :: 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 A7: 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 A3, A4, FUNCOP_1:7; :: thesis: verum
end;
assume not x in dom ({b} --> d) ; :: thesis: h . x = ({a} --> c) . x
then x in dom ({a} --> c) by A7, XBOOLE_0:def 3;
then x = a by TARSKI:def 1;
hence h . x = ({a} --> c) . x by A2, A5, FUNCOP_1:7; :: thesis: verum
end;
dom h = (dom ({a} --> c)) \/ (dom ({b} --> d)) by A1, ENUMSET1:1;
hence h = (a,b) --> (c,d) by A6, Def1; :: thesis: verum