let a, b, c, d, e, i, j, k be object ; 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; ( 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
; 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 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 ;
( 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)))
;
( ( 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 )
( not x in dom ((c,d) --> (j,k)) implies h . x = ((a,b) --> (e,i)) . x )thus
( not
x in dom ((c,d) --> (j,k)) implies
h . x = ((a,b) --> (e,i)) . x )
verum end;
hence
h = (a,b,c,d) --> (e,i,j,k)
by A8, Def1; verum