let a, b, c, d, e, i, j, k be object ; :: thesis: for g being Function st 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: ( 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: dom h = {a,b,c,d} and
A2: h . a = e and
A3: h . b = i and
A4: h . c = j and
A5: 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);
A6: dom ((a,b) --> (e,i)) = {a,b} by Th62;
A7: dom ((c,d) --> (j,k)) = {c,d} by Th62;
then A8: dom h = (dom ((a,b) --> (e,i))) \/ (dom ((c,d) --> (j,k))) by A1, A6, ENUMSET1:5;

now :: thesis: for x being object st x in (dom ((a,b) --> (e,i))) \/ (dom ((c,d) --> (j,k))) holds
( ( 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 ) )

let x be object ; :: 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 A9: 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 A10: x in dom ((c,d) --> (j,k)) ; :: thesis: h . x = ((c,d) --> (j,k)) . x

per cases ( ( x = c & c <> d ) or x = d ) by A7, A10, TARSKI:def 2;

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

hence h . x = ((c,d) --> (j,k)) . x by A4, Th63; :: thesis: verum

end;

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

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

per cases ( ( x = a & a <> b ) or x = b ) by A6, A11, TARSKI:def 2;

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

hence h . x = ((a,b) --> (e,i)) . x by A2, Th63; :: thesis: verum

end;

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

hence h . x = ((a,b) --> (e,i)) . x by A3, Th63; :: thesis: verum

end;

end;

end;

end;

hence h = (a,b,c,d) --> (e,i,j,k) by A8, Def1; :: thesis: verum