:: FUNCT_4 semantic presentation

begin

                             Lm1:  for x, x9, y, y9, x1, x19, y1, y19 being set st [[x,x9],[y,y9]] = [[x1,x19],[y1,y19]] holds
( x = x1 & y = y1 & x9 = x19 & y9 = y19 )
proof
let x, x9, y, y9, x1, x19, y1, y19 be set ; ::_thesis: ( [[x,x9],[y,y9]] = [[x1,x19],[y1,y19]] implies ( x = x1 & y = y1 & x9 = x19 & y9 = y19 ) )
assume  [[x,x9],[y,y9]] = [[x1,x19],[y1,y19]] ; ::_thesis: ( x = x1 & y = y1 & x9 = x19 & y9 = y19 )
then  ( [x,x9] = [x1,x19] & [y,y9] = [y1,y19] ) by XTUPLE_0:1;
hence  ( x = x1 & y = y1 & x9 = x19 & y9 = y19 ) by XTUPLE_0:1; ::_thesis: verum
end;

theorem Th1: :: FUNCT_4:1
for Z being set st ( for z being set st z in Z holds
ex x, y being set st z = [x,y] ) holds
ex X, Y being set st Z c= [:X,Y:]
proof
let Z be set ; ::_thesis: ( ( for z being set st z in Z holds
ex x, y being set st z = [x,y] ) implies ex X, Y being set st Z c= [:X,Y:] )
assume A1: for z being set st z in Z holds
ex x, y being set st z = [x,y] ; ::_thesis: ex X, Y being set st Z c= [:X,Y:]
defpred S1[ set ] means  ex y being set st [$1,y] in Z;
consider X being set  such that
A2: for x being set holds
( x in X iff ( x in union (union Z) & S1[x] ) ) from XBOOLE_0:sch_1();
defpred S2[ set ] means  ex x being set st [x,$1] in Z;
consider Y being set  such that
A3: for y being set holds
( y in Y iff ( y in union (union Z) & S2[y] ) ) from XBOOLE_0:sch_1();
take  X ; ::_thesis: ex Y being set st Z c= [:X,Y:]
take  Y ; ::_thesis: Z c= [:X,Y:]
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Z or z in [:X,Y:] )
assume A4: z in Z ; ::_thesis: z in [:X,Y:]
then consider x, y being set  such that
A5: z = [x,y] by A1;
 x in union (union Z) by A4, A5, ZFMISC_1:134;
then A6: x in X by A2, A4, A5;
 y in union (union Z) by A4, A5, ZFMISC_1:134;
then  y in Y by A3, A4, A5;
hence  z in [:X,Y:] by A5, A6, ZFMISC_1:87; ::_thesis: verum
end;

theorem :: FUNCT_4:2
for g, f being Function holds g * f = (g | (rng f)) * f
proof
let g, f be Function; ::_thesis: g * f = (g | (rng f)) * f
 for x being set holds
( x in dom (g * f) iff x in dom ((g | (rng f)) * f) )
proof
let x be set ; ::_thesis: ( x in dom (g * f) iff x in dom ((g | (rng f)) * f) )
A1: dom (g | (rng f)) = (dom g) /\ (rng f) by RELAT_1:61;
thus  ( x in dom (g * f) implies x in dom ((g | (rng f)) * f) ) ::_thesis: ( x in dom ((g | (rng f)) * f) implies x in dom (g * f) )
proof
assume A2: x in dom (g * f) ; ::_thesis: x in dom ((g | (rng f)) * f)
then A3: x in dom f by FUNCT_1:11;
 x in dom f by A2, FUNCT_1:11;
then A4: f . x in rng f by FUNCT_1:def_3;
 f . x in dom g by A2, FUNCT_1:11;
then  f . x in dom (g | (rng f)) by A1, A4, XBOOLE_0:def_4;
hence  x in dom ((g | (rng f)) * f) by A3, FUNCT_1:11; ::_thesis: verum
end;
assume A5: x in dom ((g | (rng f)) * f) ; ::_thesis: x in dom (g * f)
then  f . x in dom (g | (rng f)) by FUNCT_1:11;
then A6: f . x in dom g by A1, XBOOLE_0:def_4;
 x in dom f by A5, FUNCT_1:11;
hence  x in dom (g * f) by A6, FUNCT_1:11; ::_thesis: verum
end;
then A7: dom (g * f) = dom ((g | (rng f)) * f) by TARSKI:1;
 for x being set st x in dom (g * f) holds
(g * f) . x = ((g | (rng f)) * f) . x
proof
let x be set ; ::_thesis: ( x in dom (g * f) implies (g * f) . x = ((g | (rng f)) * f) . x )
assume A8: x in dom (g * f) ; ::_thesis: (g * f) . x = ((g | (rng f)) * f) . x
then A9: x in dom f by FUNCT_1:11;
then A10: f . x in rng f by FUNCT_1:def_3;
thus (g * f) . x = g . (f . x) by A8, FUNCT_1:12
.= (g | (rng f)) . (f . x) by A10, FUNCT_1:49
.= ((g | (rng f)) * f) . x by A9, FUNCT_1:13 ; ::_thesis: verum
end;
hence  g * f = (g | (rng f)) * f by A7, FUNCT_1:2; ::_thesis: verum
end;

theorem :: FUNCT_4:3
for X, Y being set holds
( id X c= id Y iff X c= Y )
proof
let X, Y be set ; ::_thesis: ( id X c= id Y iff X c= Y )
thus  ( id X c= id Y implies X c= Y ) ::_thesis: ( X c= Y implies id X c= id Y )
proof
assume A1: id X c= id Y ; ::_thesis: X c= Y
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Y )
assume  x in X ; ::_thesis: x in Y
then  [x,x] in id X by RELAT_1:def_10;
hence  x in Y by A1, RELAT_1:def_10; ::_thesis: verum
end;
assume A2: X c= Y ; ::_thesis: id X c= id Y
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in id X or z in id Y )
assume A3: z in id X ; ::_thesis: z in id Y
then consider x, x9 being set  such that
A4: x in X and
 x9 in X and
A5: z = [x,x9] by ZFMISC_1:84;
 x = x9 by A3, A5, RELAT_1:def_10;
hence  z in id Y by A2, A4, A5, RELAT_1:def_10; ::_thesis: verum
end;

theorem :: FUNCT_4:4
for X, Y, a being set st X c= Y holds
X --> a c= Y --> a
proof
let X, Y, a be set ; ::_thesis: ( X c= Y implies X --> a c= Y --> a )
A1: dom (X --> a) = X by FUNCOP_1:13;
assume A2: X c= Y ; ::_thesis: X --> a c= Y --> a
A3: now__::_thesis:_for_x_being_set_st_x_in_dom_(X_-->_a)_holds_
(X_-->_a)_._x_=_(Y_-->_a)_._x
let x be set ; ::_thesis: ( x in dom (X --> a) implies (X --> a) . x = (Y --> a) . x )
assume A4: x in dom (X --> a) ; ::_thesis: (X --> a) . x = (Y --> a) . x
then  (X --> a) . x = a by FUNCOP_1:7;
hence  (X --> a) . x = (Y --> a) . x by A2, A1, A4, FUNCOP_1:7; ::_thesis: verum
end;
 dom (Y --> a) = Y by FUNCOP_1:13;
hence  X --> a c= Y --> a by A2, A1, A3, GRFUNC_1:2; ::_thesis: verum
end;

theorem Th5: :: FUNCT_4:5
for X, a, Y, b being set st X --> a c= Y --> b holds
X c= Y
proof
let X, a, Y, b be set ; ::_thesis: ( X --> a c= Y --> b implies X c= Y )
assume  X --> a c= Y --> b ; ::_thesis: X c= Y
then A1: dom (X --> a) c= dom (Y --> b) by RELAT_1:11;
 dom (X --> a) = X by FUNCOP_1:13;
hence  X c= Y by A1, FUNCOP_1:13; ::_thesis: verum
end;

theorem :: FUNCT_4:6
for X, a, Y, b being set st X <> {} & X --> a c= Y --> b holds
a = b
proof
let X, a, Y, b be set ; ::_thesis: ( X <> {} & X --> a c= Y --> b implies a = b )
assume A1: X <> {} ; ::_thesis: ( not X --> a c= Y --> b or a = b )
set x = the Element of X;
assume A2: X --> a c= Y --> b ; ::_thesis: a = b
then  X c= Y by Th5;
then  the Element of X in Y by A1, TARSKI:def_3;
then A3: (Y --> b) . the Element of X = b by FUNCOP_1:7;
 ( dom (X --> a) = X & (X --> a) . the Element of X = a ) by A1, FUNCOP_1:7, FUNCOP_1:13;
hence  a = b by A1, A2, A3, GRFUNC_1:2; ::_thesis: verum
end;

theorem :: FUNCT_4:7
for x being set
for f being Function st x in dom f holds
x .--> (f . x) c= f
proof
let x be set ; ::_thesis: for f being Function st x in dom f holds
x .--> (f . x) c= f
let f be Function; ::_thesis: ( x in dom f implies x .--> (f . x) c= f )
A1: now__::_thesis:_for_y_being_set_st_y_in_dom_(x_.-->_(f_._x))_holds_
(x_.-->_(f_._x))_._y_=_f_._y
let y be set ; ::_thesis: ( y in dom (x .--> (f . x)) implies (x .--> (f . x)) . y = f . y )
assume  y in dom (x .--> (f . x)) ; ::_thesis: (x .--> (f . x)) . y = f . y
then  x = y by FUNCOP_1:75;
hence  (x .--> (f . x)) . y = f . y by FUNCOP_1:72; ::_thesis: verum
end;
assume A2: x in dom f ; ::_thesis: x .--> (f . x) c= f
 dom (x .--> (f . x)) c= dom f
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in dom (x .--> (f . x)) or y in dom f )
thus  ( not y in dom (x .--> (f . x)) or y in dom f ) by A2, FUNCOP_1:75; ::_thesis: verum
end;
hence  x .--> (f . x) c= f by A1, GRFUNC_1:2; ::_thesis: verum
end;

theorem :: FUNCT_4:8
for Y, X being set
for f being Function holds (Y |` f) | X c= f
proof
let Y, X be set ; ::_thesis: for f being Function holds (Y |` f) | X c= f
let f be Function; ::_thesis: (Y |` f) | X c= f
 ( (Y |` f) | X c= Y |` f & Y |` f c= f ) by RELAT_1:59, RELAT_1:86;
hence  (Y |` f) | X c= f by XBOOLE_1:1; ::_thesis: verum
end;

theorem :: FUNCT_4:9
for Y, X being set
for f, g being Function st f c= g holds
(Y |` f) | X c= (Y |` g) | X
proof
let Y, X be set ; ::_thesis: for f, g being Function st f c= g holds
(Y |` f) | X c= (Y |` g) | X
let f, g be Function; ::_thesis: ( f c= g implies (Y |` f) | X c= (Y |` g) | X )
assume  f c= g ; ::_thesis: (Y |` f) | X c= (Y |` g) | X
then  Y |` f c= Y |` g by RELAT_1:101;
hence  (Y |` f) | X c= (Y |` g) | X by RELAT_1:76; ::_thesis: verum
end;

definition
let f, g be Function;
funcf +* g ->  Function means :Def1: :: FUNCT_4:def 1
( dom it = (dom f) \/ (dom g) & ( for x being set st x in (dom f) \/ (dom g) holds
( ( x in dom g implies it . x = g . x ) & ( not x in dom g implies it . x = f . x ) ) ) );
existence
 ex b1 being Function st
( dom b1 = (dom f) \/ (dom g) & ( for x being set st x in (dom f) \/ (dom g) holds
( ( x in dom g implies b1 . x = g . x ) & ( not x in dom g implies b1 . x = f . x ) ) ) )
proof
deffunc H1( set ) ->  set = f . $1;
deffunc H2( set ) ->  set = g . $1;
defpred S1[ set ] means $1 in dom g;
thus  ex F being Function st
( dom F = (dom f) \/ (dom g) & ( for x being set st x in (dom f) \/ (dom g) holds
( ( S1[x] implies F . x = H2(x) ) & ( not S1[x] implies F . x = H1(x) ) ) ) ) from PARTFUN1:sch_1(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function st dom b1 = (dom f) \/ (dom g) & ( for x being set st x in (dom f) \/ (dom g) holds
( ( x in dom g implies b1 . x = g . x ) & ( not x in dom g implies b1 . x = f . x ) ) ) & dom b2 = (dom f) \/ (dom g) & ( for x being set st x in (dom f) \/ (dom g) holds
( ( x in dom g implies b2 . x = g . x ) & ( not x in dom g implies b2 . x = f . x ) ) ) holds
b1 = b2
proof
let h1, h2 be Function; ::_thesis: ( dom h1 = (dom f) \/ (dom g) & ( for x being set st x in (dom f) \/ (dom g) holds
( ( x in dom g implies h1 . x = g . x ) & ( not x in dom g implies h1 . x = f . x ) ) ) & dom h2 = (dom f) \/ (dom g) & ( for x being set st x in (dom f) \/ (dom g) holds
( ( x in dom g implies h2 . x = g . x ) & ( not x in dom g implies h2 . x = f . x ) ) ) implies h1 = h2 )
assume that
A1: dom h1 = (dom f) \/ (dom g) and
A2: for x being set st x in (dom f) \/ (dom g) holds
( ( x in dom g implies h1 . x = g . x ) & ( not x in dom g implies h1 . x = f . x ) ) and
A3: dom h2 = (dom f) \/ (dom g) and
A4: for x being set st x in (dom f) \/ (dom g) holds
( ( x in dom g implies h2 . x = g . x ) & ( not x in dom g implies h2 . x = f . x ) ) ; ::_thesis: h1 = h2
 for x being set st x in (dom f) \/ (dom g) holds
h1 . x = h2 . x
proof
let x be set ; ::_thesis: ( x in (dom f) \/ (dom g) implies h1 . x = h2 . x )
assume A5: x in (dom f) \/ (dom g) ; ::_thesis: h1 . x = h2 . x
then A6: ( not x in dom g implies ( h1 . x = f . x & h2 . x = f . x ) ) by A2, A4;
 ( x in dom g implies ( h1 . x = g . x & h2 . x = g . x ) ) by A2, A4, A5;
hence  h1 . x = h2 . x by A6; ::_thesis: verum
end;
hence  h1 = h2 by A1, A3, FUNCT_1:2; ::_thesis: verum
end;
idempotence
 for f being Function holds
( dom f = (dom f) \/ (dom f) & ( for x being set st x in (dom f) \/ (dom f) holds
( ( x in dom f implies f . x = f . x ) & ( not x in dom f implies f . x = f . x ) ) ) ) ;
end;

:: deftheorem Def1 defines +* FUNCT_4:def_1_:_
 for f, g, b3 being Function holds
( b3 = f +* g iff ( dom b3 = (dom f) \/ (dom g) & ( for x being set st x in (dom f) \/ (dom g) holds
( ( x in dom g implies b3 . x = g . x ) & ( not x in dom g implies b3 . x = f . x ) ) ) ) );

theorem Th10: :: FUNCT_4:10
for f, g being Function holds
( dom f c= dom (f +* g) & dom g c= dom (f +* g) )
proof
let f, g be Function; ::_thesis: ( dom f c= dom (f +* g) & dom g c= dom (f +* g) )
 dom (f +* g) = (dom f) \/ (dom g) by Def1;
hence  ( dom f c= dom (f +* g) & dom g c= dom (f +* g) ) by XBOOLE_1:7; ::_thesis: verum
end;

theorem Th11: :: FUNCT_4:11
for x being set
for g, f being Function st not x in dom g holds
(f +* g) . x = f . x
proof
let x be set ; ::_thesis: for g, f being Function st not x in dom g holds
(f +* g) . x = f . x
let g, f be Function; ::_thesis: ( not x in dom g implies (f +* g) . x = f . x )
assume A1: not x in dom g ; ::_thesis: (f +* g) . x = f . x
percases ( x in dom f or not x in dom f ) ;
suppose x in dom f ; ::_thesis: (f +* g) . x = f . x
then  x in (dom f) \/ (dom g) by XBOOLE_0:def_3;
hence  (f +* g) . x = f . x by A1, Def1; ::_thesis: verum
end;
supposeA2: not x in dom f ; ::_thesis: (f +* g) . x = f . x
then  not x in (dom f) \/ (dom g) by A1, XBOOLE_0:def_3;
then  not x in dom (f +* g) by Def1;
hence (f +* g) . x = {} by FUNCT_1:def_2
.= f . x by A2, FUNCT_1:def_2 ;
::_thesis: verum
end;
end;
end;

theorem Th12: :: FUNCT_4:12
for x being set
for f, g being Function holds
( x in dom (f +* g) iff ( x in dom f or x in dom g ) )
proof
let x be set ; ::_thesis: for f, g being Function holds
( x in dom (f +* g) iff ( x in dom f or x in dom g ) )
let f, g be Function; ::_thesis: ( x in dom (f +* g) iff ( x in dom f or x in dom g ) )
 ( x in dom (f +* g) iff x in (dom f) \/ (dom g) ) by Def1;
hence  ( x in dom (f +* g) iff ( x in dom f or x in dom g ) ) by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem Th13: :: FUNCT_4:13
for x being set
for g, f being Function st x in dom g holds
(f +* g) . x = g . x
proof
let x be set ; ::_thesis: for g, f being Function st x in dom g holds
(f +* g) . x = g . x
let g, f be Function; ::_thesis: ( x in dom g implies (f +* g) . x = g . x )
 ( x in dom g implies x in (dom f) \/ (dom g) ) by XBOOLE_0:def_3;
hence  ( x in dom g implies (f +* g) . x = g . x ) by Def1; ::_thesis: verum
end;

theorem Th14: :: FUNCT_4:14
for f, g, h being Function holds (f +* g) +* h = f +* (g +* h)
proof
let f, g, h be Function; ::_thesis: (f +* g) +* h = f +* (g +* h)
A1: now__::_thesis:_for_x_being_set_st_x_in_(dom_f)_\/_(dom_(g_+*_h))_holds_
(_(_x_in_dom_(g_+*_h)_implies_((f_+*_g)_+*_h)_._x_=_(g_+*_h)_._x_)_&_(_not_x_in_dom_(g_+*_h)_implies_((f_+*_g)_+*_h)_._x_=_f_._x_)_)
let x be set ; ::_thesis: ( x in (dom f) \/ (dom (g +* h)) implies ( ( x in dom (g +* h) implies ((f +* g) +* h) . x = (g +* h) . x ) & ( not x in dom (g +* h) implies ((f +* g) +* h) . x = f . x ) ) )
assume  x in (dom f) \/ (dom (g +* h)) ; ::_thesis: ( ( x in dom (g +* h) implies ((f +* g) +* h) . x = (g +* h) . x ) & ( not x in dom (g +* h) implies ((f +* g) +* h) . x = f . x ) )
hereby  ::_thesis: ( not x in dom (g +* h) implies ((f +* g) +* h) . x = f . x )
assume A2: x in dom (g +* h) ; ::_thesis: ((f +* g) +* h) . x = (g +* h) . x
percases ( ( x in dom g & not x in dom h ) or x in dom h ) by A2, Th12;
supposeA3: ( x in dom g & not x in dom h ) ; ::_thesis: ((f +* g) +* h) . x = (g +* h) . x
hence ((f +* g) +* h) . x = (f +* g) . x by Th11
.= g . x by A3, Th13
.= (g +* h) . x by A3, Th11 ;
::_thesis: verum
end;
supposeA4: x in dom h ; ::_thesis: ((f +* g) +* h) . x = (g +* h) . x
hence ((f +* g) +* h) . x = h . x by Th13
.= (g +* h) . x by A4, Th13 ;
::_thesis: verum
end;
end;
end;
assume A5: not x in dom (g +* h) ; ::_thesis: ((f +* g) +* h) . x = f . x
then A6: not x in dom g by Th12;
 not x in dom h by A5, Th12;
hence ((f +* g) +* h) . x = (f +* g) . x by Th11
.= f . x by A6, Th11 ;
::_thesis: verum
end;
dom ((f +* g) +* h) = (dom (f +* g)) \/ (dom h) by Def1
.= ((dom f) \/ (dom g)) \/ (dom h) by Def1
.= (dom f) \/ ((dom g) \/ (dom h)) by XBOOLE_1:4
.= (dom f) \/ (dom (g +* h)) by Def1 ;
hence  (f +* g) +* h = f +* (g +* h) by A1, Def1; ::_thesis: verum
end;

theorem Th15: :: FUNCT_4:15
for x being set
for f, g being Function st f tolerates g & x in dom f holds
(f +* g) . x = f . x
proof
let x be set ; ::_thesis: for f, g being Function st f tolerates g & x in dom f holds
(f +* g) . x = f . x
let f, g be Function; ::_thesis: ( f tolerates g & x in dom f implies (f +* g) . x = f . x )
assume that
A1: f tolerates g and
A2: x in dom f ; ::_thesis: (f +* g) . x = f . x
now__::_thesis:_(f_+*_g)_._x_=_f_._x
percases ( x in dom g or not x in dom g ) ;
suppose x in dom g ; ::_thesis: (f +* g) . x = f . x
then  ( x in (dom f) /\ (dom g) & (f +* g) . x = g . x ) by A2, Th13, XBOOLE_0:def_4;
hence  (f +* g) . x = f . x by A1, PARTFUN1:def_4; ::_thesis: verum
end;
suppose not x in dom g ; ::_thesis: (f +* g) . x = f . x
hence  (f +* g) . x = f . x by Th11; ::_thesis: verum
end;
end;
end;
hence  (f +* g) . x = f . x ; ::_thesis: verum
end;

theorem :: FUNCT_4:16
for x being set
for f, g being Function st dom f misses dom g & x in dom f holds
(f +* g) . x = f . x
proof
let x be set ; ::_thesis: for f, g being Function st dom f misses dom g & x in dom f holds
(f +* g) . x = f . x
let f, g be Function; ::_thesis: ( dom f misses dom g & x in dom f implies (f +* g) . x = f . x )
assume  ( (dom f) /\ (dom g) = {} & x in dom f ) ; :: according to XBOOLE_0:def_7 ::_thesis: (f +* g) . x = f . x
then  not x in dom g by XBOOLE_0:def_4;
hence  (f +* g) . x = f . x by Th11; ::_thesis: verum
end;

theorem Th17: :: FUNCT_4:17
for f, g being Function holds rng (f +* g) c= (rng f) \/ (rng g)
proof
let f, g be Function; ::_thesis: rng (f +* g) c= (rng f) \/ (rng g)
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (f +* g) or y in (rng f) \/ (rng g) )
assume  y in rng (f +* g) ; ::_thesis: y in (rng f) \/ (rng g)
then consider x being set  such that
A1: x in dom (f +* g) and
A2: y = (f +* g) . x by FUNCT_1:def_3;
 ( ( x in dom f & not x in dom g ) or x in dom g ) by A1, Th12;
then  ( ( x in dom f & (f +* g) . x = f . x ) or ( x in dom g & (f +* g) . x = g . x ) ) by Th11, Th13;
then  ( y in rng f or y in rng g ) by A2, FUNCT_1:def_3;
hence  y in (rng f) \/ (rng g) by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem :: FUNCT_4:18
for g, f being Function holds rng g c= rng (f +* g)
proof
let g, f be Function; ::_thesis: rng g c= rng (f +* g)
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in rng (f +* g) )
assume  y in rng g ; ::_thesis: y in rng (f +* g)
then consider x being set  such that
A1: ( x in dom g & y = g . x ) by FUNCT_1:def_3;
 ( x in dom (f +* g) & (f +* g) . x = y ) by A1, Th12, Th13;
hence  y in rng (f +* g) by FUNCT_1:def_3; ::_thesis: verum
end;

theorem Th19: :: FUNCT_4:19
for f, g being Function st dom f c= dom g holds
f +* g = g
proof
let f, g be Function; ::_thesis: ( dom f c= dom g implies f +* g = g )
assume  dom f c= dom g ; ::_thesis: f +* g = g
then  (dom f) \/ (dom g) = dom g by XBOOLE_1:12;
then  ( dom (f +* g) = dom g & ( for x being set st x in dom g holds
(f +* g) . x = g . x ) ) by Def1;
hence  f +* g = g by FUNCT_1:2; ::_thesis: verum
end;

registration
let f be Function;
let g be empty Function;
reduceg +* f to f;
reducibility
 g +* f = f
proof
 dom g c= dom f by XBOOLE_1:2;
hence  g +* f = f by Th19; ::_thesis: verum
end;
reducef +* g to f;
reducibility
 f +* g = f
proof
A1: for x being set st x in dom f holds
(f +* g) . x = f . x
proof
let x be set ; ::_thesis: ( x in dom f implies (f +* g) . x = f . x )
assume  x in dom f ; ::_thesis: (f +* g) . x = f . x
then  x in (dom f) \ (dom g) ;
hence  (f +* g) . x = f . x by Th11; ::_thesis: verum
end;
 (dom f) \/ (dom g) = dom f ;
then  dom (f +* g) = dom f by Def1;
hence  f +* g = f by A1, FUNCT_1:2; ::_thesis: verum
end;
end;

theorem Th20: :: FUNCT_4:20
for f being Function holds {} +* f = f ;

theorem Th21: :: FUNCT_4:21
for f being Function holds f +* {} = f ;

theorem :: FUNCT_4:22
for X, Y being set holds (id X) +* (id Y) = id (X \/ Y)
proof
let X, Y be set ; ::_thesis: (id X) +* (id Y) = id (X \/ Y)
A1: for x being set st x in dom (id (X \/ Y)) holds
((id X) +* (id Y)) . x = (id (X \/ Y)) . x
proof
let x be set ; ::_thesis: ( x in dom (id (X \/ Y)) implies ((id X) +* (id Y)) . x = (id (X \/ Y)) . x )
assume A2: x in dom (id (X \/ Y)) ; ::_thesis: ((id X) +* (id Y)) . x = (id (X \/ Y)) . x
now__::_thesis:_((id_X)_+*_(id_Y))_._x_=_(id_(X_\/_Y))_._x
percases ( x in Y or not x in Y ) ;
supposeA3: x in Y ; ::_thesis: ((id X) +* (id Y)) . x = (id (X \/ Y)) . x
 dom (id Y) = Y ;
hence ((id X) +* (id Y)) . x = (id Y) . x by A3, Th13
.= x by A3, FUNCT_1:18
.= (id (X \/ Y)) . x by A2, FUNCT_1:18 ;
::_thesis: verum
end;
supposeA4: not x in Y ; ::_thesis: ((id X) +* (id Y)) . x = (id (X \/ Y)) . x
then A5: x in X by A2, XBOOLE_0:def_3;
 not x in dom (id Y) by A4;
hence ((id X) +* (id Y)) . x = (id X) . x by Th11
.= x by A5, FUNCT_1:18
.= (id (X \/ Y)) . x by A2, FUNCT_1:18 ;
::_thesis: verum
end;
end;
end;
hence  ((id X) +* (id Y)) . x = (id (X \/ Y)) . x ; ::_thesis: verum
end;
dom ((id X) +* (id Y)) = (dom (id X)) \/ (dom (id Y)) by Def1
.= X \/ (dom (id Y))
.= X \/ Y
.= dom (id (X \/ Y)) ;
hence  (id X) +* (id Y) = id (X \/ Y) by A1, FUNCT_1:2; ::_thesis: verum
end;

theorem :: FUNCT_4:23
for f, g being Function holds (f +* g) | (dom g) = g
proof
let f, g be Function; ::_thesis: (f +* g) | (dom g) = g
 (dom f) \/ (dom g) = dom (f +* g) by Def1;
then A1: dom ((f +* g) | (dom g)) = dom g by RELAT_1:62, XBOOLE_1:7;
 for x being set st x in dom g holds
((f +* g) | (dom g)) . x = g . x
proof
let x be set ; ::_thesis: ( x in dom g implies ((f +* g) | (dom g)) . x = g . x )
 ( x in dom g implies (f +* g) . x = g . x ) by Th13;
hence  ( x in dom g implies ((f +* g) | (dom g)) . x = g . x ) by A1, FUNCT_1:47; ::_thesis: verum
end;
hence  (f +* g) | (dom g) = g by A1, FUNCT_1:2; ::_thesis: verum
end;

theorem Th24: :: FUNCT_4:24
for f, g being Function holds (f +* g) | ((dom f) \ (dom g)) c= f
proof
let f, g be Function; ::_thesis: (f +* g) | ((dom f) \ (dom g)) c= f
A1: for x being set st x in dom ((f +* g) | ((dom f) \ (dom g))) holds
((f +* g) | ((dom f) \ (dom g))) . x = f . x
proof
let x be set ; ::_thesis: ( x in dom ((f +* g) | ((dom f) \ (dom g))) implies ((f +* g) | ((dom f) \ (dom g))) . x = f . x )
assume A2: x in dom ((f +* g) | ((dom f) \ (dom g))) ; ::_thesis: ((f +* g) | ((dom f) \ (dom g))) . x = f . x
 dom ((f +* g) | ((dom f) \ (dom g))) c= (dom f) \ (dom g) by RELAT_1:58;
then  not x in dom g by A2, XBOOLE_0:def_5;
then  (f +* g) . x = f . x by Th11;
hence  ((f +* g) | ((dom f) \ (dom g))) . x = f . x by A2, FUNCT_1:47; ::_thesis: verum
end;
 dom ((f +* g) | ((dom f) \ (dom g))) c= (dom f) \ (dom g) by RELAT_1:58;
then  dom ((f +* g) | ((dom f) \ (dom g))) c= dom f by XBOOLE_1:1;
hence  (f +* g) | ((dom f) \ (dom g)) c= f by A1, GRFUNC_1:2; ::_thesis: verum
end;

theorem Th25: :: FUNCT_4:25
for g, f being Function holds g c= f +* g
proof
let g, f be Function; ::_thesis: g c= f +* g
 dom (f +* g) = (dom f) \/ (dom g) by Def1;
then A1: dom g c= dom (f +* g) by XBOOLE_1:7;
 for x being set st x in dom g holds
(f +* g) . x = g . x by Th13;
hence  g c= f +* g by A1, GRFUNC_1:2; ::_thesis: verum
end;

theorem :: FUNCT_4:26
for f, g, h being Function st f tolerates g +* h holds
f | ((dom f) \ (dom h)) tolerates g
proof
let f, g, h be Function; ::_thesis: ( f tolerates g +* h implies f | ((dom f) \ (dom h)) tolerates g )
assume A1: f tolerates g +* h ; ::_thesis: f | ((dom f) \ (dom h)) tolerates g
let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not x in (dom (f | ((dom f) \ (dom h)))) /\ (dom g) or (f | ((dom f) \ (dom h))) . x = g . x )
assume A2: x in (dom (f | ((dom f) \ (dom h)))) /\ (dom g) ; ::_thesis: (f | ((dom f) \ (dom h))) . x = g . x
then A3: x in dom (f | ((dom f) \ (dom h))) by XBOOLE_0:def_4;
 x in dom g by A2, XBOOLE_0:def_4;
then A4: x in dom (g +* h) by Th12;
A5: dom (f | ((dom f) \ (dom h))) c= (dom f) \ (dom h) by RELAT_1:58;
then  x in dom f by A3, XBOOLE_0:def_5;
then A6: x in (dom f) /\ (dom (g +* h)) by A4, XBOOLE_0:def_4;
 not x in dom h by A3, A5, XBOOLE_0:def_5;
then  (g +* h) . x = g . x by Th11;
then  f . x = g . x by A1, A6, PARTFUN1:def_4;
hence  (f | ((dom f) \ (dom h))) . x = g . x by A3, A5, FUNCT_1:49; ::_thesis: verum
end;

theorem Th27: :: FUNCT_4:27
for f, g, h being Function st f tolerates g +* h holds
f tolerates h
proof
let f, g, h be Function; ::_thesis: ( f tolerates g +* h implies f tolerates h )
assume A1: f tolerates g +* h ; ::_thesis: f tolerates h
let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not x in (dom f) /\ (dom h) or f . x = h . x )
assume A2: x in (dom f) /\ (dom h) ; ::_thesis: f . x = h . x
then A3: x in dom f by XBOOLE_0:def_4;
A4: x in dom h by A2, XBOOLE_0:def_4;
then  x in dom (g +* h) by Th12;
then A5: x in (dom f) /\ (dom (g +* h)) by A3, XBOOLE_0:def_4;
 (g +* h) . x = h . x by A4, Th13;
hence  f . x = h . x by A1, A5, PARTFUN1:def_4; ::_thesis: verum
end;

theorem Th28: :: FUNCT_4:28
for f, g being Function holds
( f tolerates g iff f c= f +* g )
proof
let f, g be Function; ::_thesis: ( f tolerates g iff f c= f +* g )
thus  ( f tolerates g implies f c= f +* g ) ::_thesis: ( f c= f +* g implies f tolerates g )
proof
 (dom f) \/ (dom g) = dom (f +* g) by Def1;
then A1: dom f c= dom (f +* g) by XBOOLE_1:7;
assume  f tolerates g ; ::_thesis: f c= f +* g
then  for x being set st x in dom f holds
(f +* g) . x = f . x by Th15;
hence  f c= f +* g by A1, GRFUNC_1:2; ::_thesis: verum
end;
thus  ( f c= f +* g implies f tolerates g ) by Th27, PARTFUN1:54; ::_thesis: verum
end;

theorem Th29: :: FUNCT_4:29
for f, g being Function holds f +* g c= f \/ g
proof
let f, g be Function; ::_thesis: f +* g c= f \/ g
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in f +* g or p in f \/ g )
assume A1: p in f +* g ; ::_thesis: p in f \/ g
then consider x, y being set  such that
A2: p = [x,y] by RELAT_1:def_1;
 x in dom (f +* g) by A1, A2, FUNCT_1:1;
then  ( ( x in dom f & not x in dom g ) or x in dom g ) by Th12;
then A3: ( ( x in dom f & (f +* g) . x = f . x ) or ( x in dom g & (f +* g) . x = g . x ) ) by Th11, Th13;
 y = (f +* g) . x by A1, A2, FUNCT_1:1;
then  ( p in f or p in g ) by A2, A3, FUNCT_1:1;
hence  p in f \/ g by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem Th30: :: FUNCT_4:30
for f, g being Function holds
( f tolerates g iff f \/ g = f +* g )
proof
let f, g be Function; ::_thesis: ( f tolerates g iff f \/ g = f +* g )
thus  ( f tolerates g implies f \/ g = f +* g ) ::_thesis: ( f \/ g = f +* g implies f tolerates g )
proof
assume  f tolerates g ; ::_thesis: f \/ g = f +* g
then A1: f c= f +* g by Th28;
A2: f +* g c= f \/ g by Th29;
 g c= f +* g by Th25;
then  f \/ g c= f +* g by A1, XBOOLE_1:8;
hence  f \/ g = f +* g by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
thus  ( f \/ g = f +* g implies f tolerates g ) by PARTFUN1:51; ::_thesis: verum
end;

theorem Th31: :: FUNCT_4:31
for f, g being Function st dom f misses dom g holds
f \/ g = f +* g
proof
let f, g be Function; ::_thesis: ( dom f misses dom g implies f \/ g = f +* g )
assume  dom f misses dom g ; ::_thesis: f \/ g = f +* g
then  f tolerates g by PARTFUN1:56;
hence  f \/ g = f +* g by Th30; ::_thesis: verum
end;

theorem Th32: :: FUNCT_4:32
for f, g being Function st dom f misses dom g holds
f c= f +* g
proof
let f, g be Function; ::_thesis: ( dom f misses dom g implies f c= f +* g )
assume  dom f misses dom g ; ::_thesis: f c= f +* g
then  f \/ g = f +* g by Th31;
hence  f c= f +* g by XBOOLE_1:7; ::_thesis: verum
end;

theorem :: FUNCT_4:33
for f, g being Function st dom f misses dom g holds
(f +* g) | (dom f) = f
proof
let f, g be Function; ::_thesis: ( dom f misses dom g implies (f +* g) | (dom f) = f )
assume  dom f misses dom g ; ::_thesis: (f +* g) | (dom f) = f
then A1: (dom f) \ (dom g) = dom f by XBOOLE_1:83;
dom ((f +* g) | (dom f)) = (dom (f +* g)) /\ (dom f) by RELAT_1:61
.= ((dom f) \/ (dom g)) /\ (dom f) by Def1
.= dom f by XBOOLE_1:21 ;
hence  (f +* g) | (dom f) = f by A1, Th24, GRFUNC_1:3; ::_thesis: verum
end;

theorem Th34: :: FUNCT_4:34
for f, g being Function holds
( f tolerates g iff f +* g = g +* f )
proof
let f, g be Function; ::_thesis: ( f tolerates g iff f +* g = g +* f )
thus  ( f tolerates g implies f +* g = g +* f ) ::_thesis: ( f +* g = g +* f implies f tolerates g )
proof
assume A1: f tolerates g ; ::_thesis: f +* g = g +* f
A2: for x being set st x in dom (f +* g) holds
(f +* g) . x = (g +* f) . x
proof
let x be set ; ::_thesis: ( x in dom (f +* g) implies (f +* g) . x = (g +* f) . x )
assume A3: x in dom (f +* g) ; ::_thesis: (f +* g) . x = (g +* f) . x
now__::_thesis:_(f_+*_g)_._x_=_(g_+*_f)_._x
A4: dom (f +* g) = (dom f) \/ (dom g) by Def1;
percases ( ( x in dom f & x in dom g ) or ( x in dom f & not x in dom g ) or ( not x in dom f & x in dom g ) ) by A3, A4, XBOOLE_0:def_3;
supposeA5: ( x in dom f & x in dom g ) ; ::_thesis: (f +* g) . x = (g +* f) . x
then A6: (g +* f) . x = f . x by Th13;
 ( x in (dom f) /\ (dom g) & (f +* g) . x = g . x ) by A5, Th13, XBOOLE_0:def_4;
hence  (f +* g) . x = (g +* f) . x by A1, A6, PARTFUN1:def_4; ::_thesis: verum
end;
supposeA7: ( x in dom f & not x in dom g ) ; ::_thesis: (f +* g) . x = (g +* f) . x
then  (f +* g) . x = f . x by Th11;
hence  (f +* g) . x = (g +* f) . x by A7, Th13; ::_thesis: verum
end;
supposeA8: ( not x in dom f & x in dom g ) ; ::_thesis: (f +* g) . x = (g +* f) . x
then  (f +* g) . x = g . x by Th13;
hence  (f +* g) . x = (g +* f) . x by A8, Th11; ::_thesis: verum
end;
end;
end;
hence  (f +* g) . x = (g +* f) . x ; ::_thesis: verum
end;
dom (f +* g) = (dom g) \/ (dom f) by Def1
.= dom (g +* f) by Def1 ;
hence  f +* g = g +* f by A2, FUNCT_1:2; ::_thesis: verum
end;
assume A9: f +* g = g +* f ; ::_thesis: f tolerates g
let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not x in (dom f) /\ (dom g) or f . x = g . x )
assume A10: x in (dom f) /\ (dom g) ; ::_thesis: f . x = g . x
then  x in dom g by XBOOLE_0:def_4;
then A11: (f +* g) . x = g . x by Th13;
 x in dom f by A10, XBOOLE_0:def_4;
hence  f . x = g . x by A9, A11, Th13; ::_thesis: verum
end;

theorem Th35: :: FUNCT_4:35
for f, g being Function st dom f misses dom g holds
f +* g = g +* f
proof
let f, g be Function; ::_thesis: ( dom f misses dom g implies f +* g = g +* f )
assume  dom f misses dom g ; ::_thesis: f +* g = g +* f
then  f tolerates g by PARTFUN1:56;
hence  f +* g = g +* f by Th34; ::_thesis: verum
end;

theorem :: FUNCT_4:36
for X, Y being set
for f, g being PartFunc of X,Y st g is total holds
f +* g = g
proof
let X, Y be set ; ::_thesis: for f, g being PartFunc of X,Y st g is total holds
f +* g = g
let f, g be PartFunc of X,Y; ::_thesis: ( g is total implies f +* g = g )
assume  dom g = X ; :: according to PARTFUN1:def_2 ::_thesis: f +* g = g
then  dom f c= dom g ;
hence  f +* g = g by Th19; ::_thesis: verum
end;

theorem Th37: :: FUNCT_4:37
for X, Y being set
for f, g being Function of X,Y st ( Y = {} implies X = {} ) holds
f +* g = g
proof
let X, Y be set ; ::_thesis: for f, g being Function of X,Y st ( Y = {} implies X = {} ) holds
f +* g = g
let f, g be Function of X,Y; ::_thesis: ( ( Y = {} implies X = {} ) implies f +* g = g )
assume  ( Y = {} implies X = {} ) ; ::_thesis: f +* g = g
then  ( dom f = X & dom g = X ) by FUNCT_2:def_1;
hence  f +* g = g by Th19; ::_thesis: verum
end;

theorem :: FUNCT_4:38
for X being set
for f, g being Function of X,X holds f +* g = g by Th37;

theorem :: FUNCT_4:39
for X being set
for D being non empty set
for f, g being Function of X,D holds f +* g = g by Th37;

theorem :: FUNCT_4:40
for X, Y being set
for f, g being PartFunc of X,Y holds f +* g is PartFunc of X,Y
proof
let X, Y be set ; ::_thesis: for f, g being PartFunc of X,Y holds f +* g is PartFunc of X,Y
let f, g be PartFunc of X,Y; ::_thesis: f +* g is PartFunc of X,Y
 rng (f +* g) c= (rng f) \/ (rng g) by Th17;
then A1: rng (f +* g) c= Y by XBOOLE_1:1;
 dom (f +* g) = (dom f) \/ (dom g) by Def1;
hence  f +* g is PartFunc of X,Y by A1, RELSET_1:4; ::_thesis: verum
end;

definition
let f be Function;
func ~ f ->  Function means :Def2: :: FUNCT_4:def 2
( ( for x being set holds
( x in dom it iff ex y, z being set st
( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being set st [y,z] in dom f holds
it . (z,y) = f . (y,z) ) );
existence
 ex b1 being Function st
( ( for x being set holds
( x in dom b1 iff ex y, z being set st
( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being set st [y,z] in dom f holds
b1 . (z,y) = f . (y,z) ) )
proof
defpred S1[ set , set ] means  ex y, z being set st
( $1 = [z,y] & $2 = f . [y,z] );
defpred S2[ set ] means  ex y being set st [$1,y] in dom f;
consider D1 being set  such that
A1: for x being set holds
( x in D1 iff ( x in union (union (dom f)) & S2[x] ) ) from XBOOLE_0:sch_1();
defpred S3[ set ] means  ex y being set st [y,$1] in dom f;
consider D2 being set  such that
A2: for y being set holds
( y in D2 iff ( y in union (union (dom f)) & S3[y] ) ) from XBOOLE_0:sch_1();
defpred S4[ set ] means  ex y, z being set st
( $1 = [z,y] & [y,z] in dom f );
consider D being set  such that
A3: for x being set holds
( x in D iff ( x in [:D2,D1:] & S4[x] ) ) from XBOOLE_0:sch_1();
A4: for x, y1, y2 being set st x in D & S1[x,y1] & S1[x,y2] holds
y1 = y2
proof
let x, y1, y2 be set ; ::_thesis: ( x in D & S1[x,y1] & S1[x,y2] implies y1 = y2 )
assume  x in D ; ::_thesis: ( not S1[x,y1] or not S1[x,y2] or y1 = y2 )
given y, z being set  such that A5: x = [z,y] and
A6: y1 = f . [y,z] ; ::_thesis: ( not S1[x,y2] or y1 = y2 )
given y9, z9 being set  such that A7: x = [z9,y9] and
A8: y2 = f . [y9,z9] ; ::_thesis: y1 = y2
 z = z9 by A5, A7, XTUPLE_0:1;
hence  y1 = y2 by A5, A6, A7, A8, XTUPLE_0:1; ::_thesis: verum
end;
A9: for x being set st x in D holds
ex y1 being set st S1[x,y1]
proof
let x be set ; ::_thesis: ( x in D implies ex y1 being set st S1[x,y1] )
assume  x in D ; ::_thesis: ex y1 being set st S1[x,y1]
then consider y, z being set  such that
A10: x = [z,y] and
 [y,z] in dom f by A3;
take  f . [y,z] ; ::_thesis: S1[x,f . [y,z]]
thus  S1[x,f . [y,z]] by A10; ::_thesis: verum
end;
consider h being Function such that
A11: dom h = D and
A12: for x being set st x in D holds
S1[x,h . x] from FUNCT_1:sch_2(A4, A9);
take  h ; ::_thesis: ( ( for x being set holds
( x in dom h iff ex y, z being set st
( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being set st [y,z] in dom f holds
h . (z,y) = f . (y,z) ) )
thus A13: for x being set holds
( x in dom h iff ex y, z being set st
( x = [z,y] & [y,z] in dom f ) ) ::_thesis: for y, z being set st [y,z] in dom f holds
h . (z,y) = f . (y,z)
proof
let x be set ; ::_thesis: ( x in dom h iff ex y, z being set st
( x = [z,y] & [y,z] in dom f ) )
thus  ( x in dom h implies ex y, z being set st
( x = [z,y] & [y,z] in dom f ) ) by A3, A11; ::_thesis: ( ex y, z being set st
( x = [z,y] & [y,z] in dom f ) implies x in dom h )
given y, z being set  such that A14: x = [z,y] and
A15: [y,z] in dom f ; ::_thesis: x in dom h
 y in union (union (dom f)) by A15, ZFMISC_1:134;
then A16: y in D1 by A1, A15;
 z in union (union (dom f)) by A15, ZFMISC_1:134;
then  z in D2 by A2, A15;
then  [z,y] in [:D2,D1:] by A16, ZFMISC_1:87;
hence  x in dom h by A3, A11, A14, A15; ::_thesis: verum
end;
let y, z be set ; ::_thesis: ( [y,z] in dom f implies h . (z,y) = f . (y,z) )
assume  [y,z] in dom f ; ::_thesis: h . (z,y) = f . (y,z)
then  [z,y] in D by A11, A13;
then consider y9, z9 being set  such that
A17: [z,y] = [z9,y9] and
A18: h . (z,y) = f . [y9,z9] by A12;
 z = z9 by A17, XTUPLE_0:1;
hence  h . (z,y) = f . (y,z) by A17, A18, XTUPLE_0:1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function st ( for x being set holds
( x in dom b1 iff ex y, z being set st
( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being set st [y,z] in dom f holds
b1 . (z,y) = f . (y,z) ) & ( for x being set holds
( x in dom b2 iff ex y, z being set st
( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being set st [y,z] in dom f holds
b2 . (z,y) = f . (y,z) ) holds
b1 = b2
proof
let h1, h2 be Function; ::_thesis: ( ( for x being set holds
( x in dom h1 iff ex y, z being set st
( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being set st [y,z] in dom f holds
h1 . (z,y) = f . (y,z) ) & ( for x being set holds
( x in dom h2 iff ex y, z being set st
( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being set st [y,z] in dom f holds
h2 . (z,y) = f . (y,z) ) implies h1 = h2 )
assume that
A19: for x being set holds
( x in dom h1 iff ex y, z being set st
( x = [z,y] & [y,z] in dom f ) ) and
A20: for y, z being set st [y,z] in dom f holds
h1 . (z,y) = f . (y,z) and
A21: for x being set holds
( x in dom h2 iff ex y, z being set st
( x = [z,y] & [y,z] in dom f ) ) and
A22: for y, z being set st [y,z] in dom f holds
h2 . (z,y) = f . (y,z) ; ::_thesis: h1 = h2
A23: for x being set st x in dom h1 holds
h1 . x = h2 . x
proof
let x be set ; ::_thesis: ( x in dom h1 implies h1 . x = h2 . x )
assume  x in dom h1 ; ::_thesis: h1 . x = h2 . x
then consider x1, x2 being set  such that
A24: x = [x2,x1] and
A25: [x1,x2] in dom f by A19;
h1 . (x2,x1) = f . (x1,x2) by A20, A25
.= h2 . (x2,x1) by A22, A25 ;
hence  h1 . x = h2 . x by A24; ::_thesis: verum
end;
 for x being set holds
( x in dom h1 iff x in dom h2 )
proof
let x be set ; ::_thesis: ( x in dom h1 iff x in dom h2 )
 ( x in dom h1 iff ex y, z being set st
( x = [z,y] & [y,z] in dom f ) ) by A19;
hence  ( x in dom h1 iff x in dom h2 ) by A21; ::_thesis: verum
end;
then  dom h1 = dom h2 by TARSKI:1;
hence  h1 = h2 by A23, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines ~ FUNCT_4:def_2_:_
 for f, b2 being Function holds
( b2 = ~ f iff ( ( for x being set holds
( x in dom b2 iff ex y, z being set st
( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being set st [y,z] in dom f holds
b2 . (z,y) = f . (y,z) ) ) );

theorem Th41: :: FUNCT_4:41
for f being Function holds rng (~ f) c= rng f
proof
let f be Function; ::_thesis: rng (~ f) c= rng f
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (~ f) or y in rng f )
assume  y in rng (~ f) ; ::_thesis: y in rng f
then consider x being set  such that
A1: x in dom (~ f) and
A2: y = (~ f) . x by FUNCT_1:def_3;
consider x1, x2 being set  such that
A3: x = [x2,x1] and
A4: [x1,x2] in dom f by A1, Def2;
y = (~ f) . (x2,x1) by A2, A3
.= f . (x1,x2) by A4, Def2 ;
hence  y in rng f by A4, FUNCT_1:def_3; ::_thesis: verum
end;

theorem Th42: :: FUNCT_4:42
for x, y being set
for f being Function holds
( [x,y] in dom f iff [y,x] in dom (~ f) )
proof
let x, y be set ; ::_thesis: for f being Function holds
( [x,y] in dom f iff [y,x] in dom (~ f) )
let f be Function; ::_thesis: ( [x,y] in dom f iff [y,x] in dom (~ f) )
thus  ( [x,y] in dom f implies [y,x] in dom (~ f) ) by Def2; ::_thesis: ( [y,x] in dom (~ f) implies [x,y] in dom f )
assume  [y,x] in dom (~ f) ; ::_thesis: [x,y] in dom f
then consider x1, y1 being set  such that
A1: [y,x] = [y1,x1] and
A2: [x1,y1] in dom f by Def2;
 x1 = x by A1, XTUPLE_0:1;
hence  [x,y] in dom f by A1, A2, XTUPLE_0:1; ::_thesis: verum
end;

theorem :: FUNCT_4:43
for y, x being set
for f being Function st [y,x] in dom (~ f) holds
(~ f) . (y,x) = f . (x,y)
proof
let y, x be set ; ::_thesis: for f being Function st [y,x] in dom (~ f) holds
(~ f) . (y,x) = f . (x,y)
let f be Function; ::_thesis: ( [y,x] in dom (~ f) implies (~ f) . (y,x) = f . (x,y) )
assume  [y,x] in dom (~ f) ; ::_thesis: (~ f) . (y,x) = f . (x,y)
then  [x,y] in dom f by Th42;
hence  (~ f) . (y,x) = f . (x,y) by Def2; ::_thesis: verum
end;

theorem :: FUNCT_4:44
for f being Function ex X, Y being set st dom (~ f) c= [:X,Y:]
proof
let f be Function; ::_thesis: ex X, Y being set st dom (~ f) c= [:X,Y:]
now__::_thesis:_for_z_being_set_st_z_in_dom_(~_f)_holds_
ex_x,_y_being_set_st_z_=_[x,y]
let z be set ; ::_thesis: ( z in dom (~ f) implies ex x, y being set st z = [x,y] )
assume  z in dom (~ f) ; ::_thesis: ex x, y being set st z = [x,y]
then  ex x, y being set st
( z = [y,x] & [x,y] in dom f ) by Def2;
hence  ex x, y being set st z = [x,y] ; ::_thesis: verum
end;
hence  ex X, Y being set st dom (~ f) c= [:X,Y:] by Th1; ::_thesis: verum
end;

theorem Th45: :: FUNCT_4:45
for X, Y being set
for f being Function st dom f c= [:X,Y:] holds
dom (~ f) c= [:Y,X:]
proof
let X, Y be set ; ::_thesis: for f being Function st dom f c= [:X,Y:] holds
dom (~ f) c= [:Y,X:]
let f be Function; ::_thesis: ( dom f c= [:X,Y:] implies dom (~ f) c= [:Y,X:] )
assume A1: dom f c= [:X,Y:] ; ::_thesis: dom (~ f) c= [:Y,X:]
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in dom (~ f) or z in [:Y,X:] )
assume  z in dom (~ f) ; ::_thesis: z in [:Y,X:]
then  ex x, y being set st
( z = [y,x] & [x,y] in dom f ) by Def2;
hence  z in [:Y,X:] by A1, ZFMISC_1:88; ::_thesis: verum
end;

theorem Th46: :: FUNCT_4:46
for X, Y being set
for f being Function st dom f = [:X,Y:] holds
dom (~ f) = [:Y,X:]
proof
let X, Y be set ; ::_thesis: for f being Function st dom f = [:X,Y:] holds
dom (~ f) = [:Y,X:]
let f be Function; ::_thesis: ( dom f = [:X,Y:] implies dom (~ f) = [:Y,X:] )
assume A1: dom f = [:X,Y:] ; ::_thesis: dom (~ f) = [:Y,X:]
hence  dom (~ f) c= [:Y,X:] by Th45; :: according to XBOOLE_0:def_10 ::_thesis: [:Y,X:] c= dom (~ f)
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in [:Y,X:] or z in dom (~ f) )
assume  z in [:Y,X:] ; ::_thesis: z in dom (~ f)
then consider y, x being set  such that
A2: ( y in Y & x in X ) and
A3: z = [y,x] by ZFMISC_1:def_2;
 [x,y] in dom f by A1, A2, ZFMISC_1:def_2;
hence  z in dom (~ f) by A3, Def2; ::_thesis: verum
end;

theorem Th47: :: FUNCT_4:47
for X, Y being set
for f being Function st dom f c= [:X,Y:] holds
rng (~ f) = rng f
proof
let X, Y be set ; ::_thesis: for f being Function st dom f c= [:X,Y:] holds
rng (~ f) = rng f
let f be Function; ::_thesis: ( dom f c= [:X,Y:] implies rng (~ f) = rng f )
assume A1: dom f c= [:X,Y:] ; ::_thesis: rng (~ f) = rng f
thus  rng (~ f) c= rng f by Th41; :: according to XBOOLE_0:def_10 ::_thesis: rng f c= rng (~ f)
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in rng (~ f) )
assume  y in rng f ; ::_thesis: y in rng (~ f)
then consider x being set  such that
A2: x in dom f and
A3: y = f . x by FUNCT_1:def_3;
consider x1, y1 being set  such that
 x1 in X and
 y1 in Y and
A4: x = [x1,y1] by A1, A2, ZFMISC_1:84;
A5: [y1,x1] in dom (~ f) by A2, A4, Th42;
y = f . (x1,y1) by A3, A4
.= (~ f) . (y1,x1) by A2, A4, Def2 ;
hence  y in rng (~ f) by A5, FUNCT_1:def_3; ::_thesis: verum
end;

theorem :: FUNCT_4:48
for X, Y, Z being set
for f being PartFunc of [:X,Y:],Z holds ~ f is PartFunc of [:Y,X:],Z
proof
let X, Y, Z be set ; ::_thesis: for f being PartFunc of [:X,Y:],Z holds ~ f is PartFunc of [:Y,X:],Z
let f be PartFunc of [:X,Y:],Z; ::_thesis: ~ f is PartFunc of [:Y,X:],Z
A1: dom f c= [:X,Y:] ;
then A2: dom (~ f) c= [:Y,X:] by Th45;
 rng f c= Z ;
then  rng (~ f) c= Z by A1, Th47;
hence  ~ f is PartFunc of [:Y,X:],Z by A2, RELSET_1:4; ::_thesis: verum
end;

theorem Th49: :: FUNCT_4:49
for X, Y, Z being set
for f being Function of [:X,Y:],Z st Z <> {} holds
~ f is Function of [:Y,X:],Z
proof
let X, Y, Z be set ; ::_thesis: for f being Function of [:X,Y:],Z st Z <> {} holds
~ f is Function of [:Y,X:],Z
let f be Function of [:X,Y:],Z; ::_thesis: ( Z <> {} implies ~ f is Function of [:Y,X:],Z )
assume A1: Z <> {} ; ::_thesis: ~ f is Function of [:Y,X:],Z
then A2: dom f = [:X,Y:] by FUNCT_2:def_1;
then A3: [:Y,X:] = dom (~ f) by Th46;
 rng f c= Z ;
then  rng (~ f) c= Z by A2, Th47;
then reconsider R = ~ f as Relation of [:Y,X:],Z by A3, RELSET_1:4;
 R is quasi_total
proof
percases ( Z <> {} or Z = {} ) ;
:: according to FUNCT_2:def_1
case Z <> {} ; ::_thesis: [:Y,X:] = dom R
 dom f = [:X,Y:] by A1, FUNCT_2:def_1;
hence  [:Y,X:] = dom R by Th46; ::_thesis: verum
end;
case Z = {} ; ::_thesis: R = {}
hence  R = {} ; ::_thesis: verum
end;
end;
end;
hence  ~ f is Function of [:Y,X:],Z ; ::_thesis: verum
end;

theorem :: FUNCT_4:50
for X, Y being set
for D being non empty set
for f being Function of [:X,Y:],D holds ~ f is Function of [:Y,X:],D by Th49;

theorem Th51: :: FUNCT_4:51
for f being Function holds ~ (~ f) c= f
proof
let f be Function; ::_thesis: ~ (~ f) c= f
A1: now__::_thesis:_for_x_being_set_st_x_in_dom_(~_(~_f))_holds_
ex_y2,_z2_being_set_st_
(_x_=_[z2,y2]_&_[y2,z2]_in_dom_(~_f)_&_[z2,y2]_in_dom_f_)
let x be set ; ::_thesis: ( x in dom (~ (~ f)) implies ex y2, z2 being set st
( x = [z2,y2] & [y2,z2] in dom (~ f) & [z2,y2] in dom f ) )
assume  x in dom (~ (~ f)) ; ::_thesis: ex y2, z2 being set st
( x = [z2,y2] & [y2,z2] in dom (~ f) & [z2,y2] in dom f )
then consider y2, z2 being set  such that
A2: ( x = [z2,y2] & [y2,z2] in dom (~ f) ) by Def2;
take y2 = y2; ::_thesis: ex z2 being set st
( x = [z2,y2] & [y2,z2] in dom (~ f) & [z2,y2] in dom f )
take z2 = z2; ::_thesis: ( x = [z2,y2] & [y2,z2] in dom (~ f) & [z2,y2] in dom f )
thus  ( x = [z2,y2] & [y2,z2] in dom (~ f) & [z2,y2] in dom f ) by A2, Th42; ::_thesis: verum
end;
A3: for x being set st x in dom (~ (~ f)) holds
(~ (~ f)) . x = f . x
proof
let x be set ; ::_thesis: ( x in dom (~ (~ f)) implies (~ (~ f)) . x = f . x )
assume  x in dom (~ (~ f)) ; ::_thesis: (~ (~ f)) . x = f . x
then consider y2, z2 being set  such that
A4: x = [z2,y2] and
A5: [y2,z2] in dom (~ f) and
A6: [z2,y2] in dom f by A1;
(~ (~ f)) . (z2,y2) = (~ f) . (y2,z2) by A5, Def2
.= f . (z2,y2) by A6, Def2 ;
hence  (~ (~ f)) . x = f . x by A4; ::_thesis: verum
end;
 dom (~ (~ f)) c= dom f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (~ (~ f)) or x in dom f )
assume  x in dom (~ (~ f)) ; ::_thesis: x in dom f
then  ex y2, z2 being set st
( x = [z2,y2] & [y2,z2] in dom (~ f) & [z2,y2] in dom f ) by A1;
hence  x in dom f ; ::_thesis: verum
end;
hence  ~ (~ f) c= f by A3, GRFUNC_1:2; ::_thesis: verum
end;

theorem Th52: :: FUNCT_4:52
for X, Y being set
for f being Function st dom f c= [:X,Y:] holds
~ (~ f) = f
proof
let X, Y be set ; ::_thesis: for f being Function st dom f c= [:X,Y:] holds
~ (~ f) = f
let f be Function; ::_thesis: ( dom f c= [:X,Y:] implies ~ (~ f) = f )
assume A1: dom f c= [:X,Y:] ; ::_thesis: ~ (~ f) = f
A2: ~ (~ f) c= f by Th51;
 dom (~ (~ f)) = dom f
proof
thus  dom (~ (~ f)) c= dom f by A2, RELAT_1:11; :: according to XBOOLE_0:def_10 ::_thesis: dom f c= dom (~ (~ f))
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in dom f or z in dom (~ (~ f)) )
assume A3: z in dom f ; ::_thesis: z in dom (~ (~ f))
then consider x, y being set  such that
 x in X and
 y in Y and
A4: z = [x,y] by A1, ZFMISC_1:84;
 [y,x] in dom (~ f) by A3, A4, Th42;
hence  z in dom (~ (~ f)) by A4, Th42; ::_thesis: verum
end;
hence  ~ (~ f) = f by Th51, GRFUNC_1:3; ::_thesis: verum
end;

theorem :: FUNCT_4:53
for X, Y, Z being set
for f being PartFunc of [:X,Y:],Z holds ~ (~ f) = f
proof
let X, Y, Z be set ; ::_thesis: for f being PartFunc of [:X,Y:],Z holds ~ (~ f) = f
let f be PartFunc of [:X,Y:],Z; ::_thesis: ~ (~ f) = f
 dom f c= [:X,Y:] ;
hence  ~ (~ f) = f by Th52; ::_thesis: verum
end;

definition
let f, g be Function;
func|:f,g:| ->  Function means :Def3: :: FUNCT_4:def 3
( ( for z being set holds
( z in dom it iff ex x, y, x9, y9 being set st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being set st [x,y] in dom f & [x9,y9] in dom g holds
it . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ) );
existence
 ex b1 being Function st
( ( for z being set holds
( z in dom b1 iff ex x, y, x9, y9 being set st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being set st [x,y] in dom f & [x9,y9] in dom g holds
b1 . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ) )
proof
defpred S1[ set , set ] means  ex x, y, x9, y9 being set st
( $1 = [[x,x9],[y,y9]] & $2 = [(f . [x,y]),(g . [x9,y9])] );
defpred S2[ set ] means  ex y being set st [$1,y] in dom f;
consider D1 being set  such that
A1: for x being set holds
( x in D1 iff ( x in union (union (dom f)) & S2[x] ) ) from XBOOLE_0:sch_1();
defpred S3[ set ] means  ex x being set st [x,$1] in dom f;
consider D2 being set  such that
A2: for y being set holds
( y in D2 iff ( y in union (union (dom f)) & S3[y] ) ) from XBOOLE_0:sch_1();
defpred S4[ set ] means  ex y being set st [$1,y] in dom g;
consider D19 being set  such that
A3: for x being set holds
( x in D19 iff ( x in union (union (dom g)) & S4[x] ) ) from XBOOLE_0:sch_1();
defpred S5[ set ] means  ex x being set st [x,$1] in dom g;
consider D29 being set  such that
A4: for y being set holds
( y in D29 iff ( y in union (union (dom g)) & S5[y] ) ) from XBOOLE_0:sch_1();
defpred S6[ set ] means  ex x, y, x9, y9 being set st
( $1 = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g );
consider D being set  such that
A5: for z being set holds
( z in D iff ( z in [:[:D1,D19:],[:D2,D29:]:] & S6[z] ) ) from XBOOLE_0:sch_1();
A6: for z, z1, z2 being set st z in D & S1[z,z1] & S1[z,z2] holds
z1 = z2
proof
let z, z1, z2 be set ; ::_thesis: ( z in D & S1[z,z1] & S1[z,z2] implies z1 = z2 )
assume  z in D ; ::_thesis: ( not S1[z,z1] or not S1[z,z2] or z1 = z2 )
given x, y, x9, y9 being set  such that A7: z = [[x,x9],[y,y9]] and
A8: z1 = [(f . [x,y]),(g . [x9,y9])] ; ::_thesis: ( not S1[z,z2] or z1 = z2 )
given x1, y1, x19, y19 being set  such that A9: z = [[x1,x19],[y1,y19]] and
A10: z2 = [(f . [x1,y1]),(g . [x19,y19])] ; ::_thesis: z1 = z2
A11: x9 = x19 by A7, A9, Lm1;
 ( x = x1 & y = y1 ) by A7, A9, Lm1;
hence  z1 = z2 by A7, A8, A9, A10, A11, Lm1; ::_thesis: verum
end;
A12: for z being set st z in D holds
ex z1 being set st S1[z,z1]
proof
let z be set ; ::_thesis: ( z in D implies ex z1 being set st S1[z,z1] )
assume  z in D ; ::_thesis: ex z1 being set st S1[z,z1]
then consider x, y, x9, y9 being set  such that
A13: z = [[x,x9],[y,y9]] and
 [x,y] in dom f and
 [x9,y9] in dom g by A5;
take  [(f . [x,y]),(g . [x9,y9])] ; ::_thesis: S1[z,[(f . [x,y]),(g . [x9,y9])]]
thus  S1[z,[(f . [x,y]),(g . [x9,y9])]] by A13; ::_thesis: verum
end;
consider h being Function such that
A14: dom h = D and
A15: for z being set st z in D holds
S1[z,h . z] from FUNCT_1:sch_2(A6, A12);
take  h ; ::_thesis: ( ( for z being set holds
( z in dom h iff ex x, y, x9, y9 being set st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being set st [x,y] in dom f & [x9,y9] in dom g holds
h . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ) )
thus A16: for z being set holds
( z in dom h iff ex x, y, x9, y9 being set st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ::_thesis: for x, y, x9, y9 being set st [x,y] in dom f & [x9,y9] in dom g holds
h . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))]
proof
let z be set ; ::_thesis: ( z in dom h iff ex x, y, x9, y9 being set st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) )
thus  ( z in dom h implies ex x, y, x9, y9 being set st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) by A5, A14; ::_thesis: ( ex x, y, x9, y9 being set st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) implies z in dom h )
given x, y, x9, y9 being set  such that A17: z = [[x,x9],[y,y9]] and
A18: [x,y] in dom f and
A19: [x9,y9] in dom g ; ::_thesis: z in dom h
 y9 in union (union (dom g)) by A19, ZFMISC_1:134;
then A20: y9 in D29 by A4, A19;
 y in union (union (dom f)) by A18, ZFMISC_1:134;
then  y in D2 by A2, A18;
then A21: [y,y9] in [:D2,D29:] by A20, ZFMISC_1:87;
 x9 in union (union (dom g)) by A19, ZFMISC_1:134;
then A22: x9 in D19 by A3, A19;
 x in union (union (dom f)) by A18, ZFMISC_1:134;
then  x in D1 by A1, A18;
then  [x,x9] in [:D1,D19:] by A22, ZFMISC_1:87;
then  z in [:[:D1,D19:],[:D2,D29:]:] by A17, A21, ZFMISC_1:87;
hence  z in dom h by A5, A14, A17, A18, A19; ::_thesis: verum
end;
let x, y, x9, y9 be set ; ::_thesis: ( [x,y] in dom f & [x9,y9] in dom g implies h . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] )
assume  ( [x,y] in dom f & [x9,y9] in dom g ) ; ::_thesis: h . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))]
then  [[x,x9],[y,y9]] in D by A14, A16;
then consider x1, y1, x19, y19 being set  such that
A23: [[x,x9],[y,y9]] = [[x1,x19],[y1,y19]] and
A24: h . [[x,x9],[y,y9]] = [(f . [x1,y1]),(g . [x19,y19])] by A15;
A25: x9 = x19 by A23, Lm1;
 ( x = x1 & y = y1 ) by A23, Lm1;
hence  h . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] by A23, A24, A25, Lm1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function st ( for z being set holds
( z in dom b1 iff ex x, y, x9, y9 being set st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being set st [x,y] in dom f & [x9,y9] in dom g holds
b1 . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ) & ( for z being set holds
( z in dom b2 iff ex x, y, x9, y9 being set st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being set st [x,y] in dom f & [x9,y9] in dom g holds
b2 . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ) holds
b1 = b2
proof
let h1, h2 be Function; ::_thesis: ( ( for z being set holds
( z in dom h1 iff ex x, y, x9, y9 being set st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being set st [x,y] in dom f & [x9,y9] in dom g holds
h1 . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ) & ( for z being set holds
( z in dom h2 iff ex x, y, x9, y9 being set st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being set st [x,y] in dom f & [x9,y9] in dom g holds
h2 . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ) implies h1 = h2 )
assume that
A26: for z being set holds
( z in dom h1 iff ex x, y, x9, y9 being set st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) and
A27: for x, y, x9, y9 being set st [x,y] in dom f & [x9,y9] in dom g holds
h1 . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] and
A28: for z being set holds
( z in dom h2 iff ex x, y, x9, y9 being set st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) and
A29: for x, y, x9, y9 being set st [x,y] in dom f & [x9,y9] in dom g holds
h2 . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ; ::_thesis: h1 = h2
A30: for z being set st z in dom h1 holds
h1 . z = h2 . z
proof
let z be set ; ::_thesis: ( z in dom h1 implies h1 . z = h2 . z )
assume  z in dom h1 ; ::_thesis: h1 . z = h2 . z
then consider x, y, x9, y9 being set  such that
A31: z = [[x,x9],[y,y9]] and
A32: ( [x,y] in dom f & [x9,y9] in dom g ) by A26;
h1 . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] by A27, A32
.= h2 . ([x,x9],[y,y9]) by A29, A32 ;
hence  h1 . z = h2 . z by A31; ::_thesis: verum
end;
 for z being set holds
( z in dom h1 iff z in dom h2 )
proof
let z be set ; ::_thesis: ( z in dom h1 iff z in dom h2 )
 ( z in dom h1 iff ex x, y, x9, y9 being set st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) by A26;
hence  ( z in dom h1 iff z in dom h2 ) by A28; ::_thesis: verum
end;
then  dom h1 = dom h2 by TARSKI:1;
hence  h1 = h2 by A30, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines |: FUNCT_4:def_3_:_
 for f, g, b3 being Function holds
( b3 = |:f,g:| iff ( ( for z being set holds
( z in dom b3 iff ex x, y, x9, y9 being set st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being set st [x,y] in dom f & [x9,y9] in dom g holds
b3 . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ) ) );

theorem Th54: :: FUNCT_4:54
for x, x9, y, y9 being set
for f, g being Function holds
( [[x,x9],[y,y9]] in dom |:f,g:| iff ( [x,y] in dom f & [x9,y9] in dom g ) )
proof
let x, x9, y, y9 be set ; ::_thesis: for f, g being Function holds
( [[x,x9],[y,y9]] in dom |:f,g:| iff ( [x,y] in dom f & [x9,y9] in dom g ) )
let f, g be Function; ::_thesis: ( [[x,x9],[y,y9]] in dom |:f,g:| iff ( [x,y] in dom f & [x9,y9] in dom g ) )
thus  ( [[x,x9],[y,y9]] in dom |:f,g:| implies ( [x,y] in dom f & [x9,y9] in dom g ) ) ::_thesis: ( [x,y] in dom f & [x9,y9] in dom g implies [[x,x9],[y,y9]] in dom |:f,g:| )
proof
assume  [[x,x9],[y,y9]] in dom |:f,g:| ; ::_thesis: ( [x,y] in dom f & [x9,y9] in dom g )
then consider x1, y1, x19, y19 being set  such that
A1: [[x,x9],[y,y9]] = [[x1,x19],[y1,y19]] and
A2: ( [x1,y1] in dom f & [x19,y19] in dom g ) by Def3;
 ( x = x1 & x9 = x19 ) by A1, Lm1;
hence  ( [x,y] in dom f & [x9,y9] in dom g ) by A1, A2, Lm1; ::_thesis: verum
end;
thus  ( [x,y] in dom f & [x9,y9] in dom g implies [[x,x9],[y,y9]] in dom |:f,g:| ) by Def3; ::_thesis: verum
end;

theorem :: FUNCT_4:55
for x, x9, y, y9 being set
for f, g being Function st [[x,x9],[y,y9]] in dom |:f,g:| holds
|:f,g:| . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))]
proof
let x, x9, y, y9 be set ; ::_thesis: for f, g being Function st [[x,x9],[y,y9]] in dom |:f,g:| holds
|:f,g:| . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))]
let f, g be Function; ::_thesis: ( [[x,x9],[y,y9]] in dom |:f,g:| implies |:f,g:| . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] )
assume  [[x,x9],[y,y9]] in dom |:f,g:| ; ::_thesis: |:f,g:| . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))]
then  ( [x,y] in dom f & [x9,y9] in dom g ) by Th54;
hence  |:f,g:| . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] by Def3; ::_thesis: verum
end;

theorem Th56: :: FUNCT_4:56
for f, g being Function holds rng |:f,g:| c= [:(rng f),(rng g):]
proof
let f, g be Function; ::_thesis: rng |:f,g:| c= [:(rng f),(rng g):]
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng |:f,g:| or z in [:(rng f),(rng g):] )
assume  z in rng |:f,g:| ; ::_thesis: z in [:(rng f),(rng g):]
then consider p being set  such that
A1: p in dom |:f,g:| and
A2: z = |:f,g:| . p by FUNCT_1:def_3;
consider x, y, x9, y9 being set  such that
A3: p = [[x,x9],[y,y9]] and
A4: ( [x,y] in dom f & [x9,y9] in dom g ) by A1, Def3;
A5: ( f . [x,y] in rng f & g . [x9,y9] in rng g ) by A4, FUNCT_1:def_3;
z = |:f,g:| . ([x,x9],[y,y9]) by A2, A3
.= [(f . (x,y)),(g . (x9,y9))] by A4, Def3 ;
hence  z in [:(rng f),(rng g):] by A5, ZFMISC_1:87; ::_thesis: verum
end;

theorem Th57: :: FUNCT_4:57
for X, Y, X9, Y9 being set
for f, g being Function st dom f c= [:X,Y:] & dom g c= [:X9,Y9:] holds
dom |:f,g:| c= [:[:X,X9:],[:Y,Y9:]:]
proof
let X, Y, X9, Y9 be set ; ::_thesis: for f, g being Function st dom f c= [:X,Y:] & dom g c= [:X9,Y9:] holds
dom |:f,g:| c= [:[:X,X9:],[:Y,Y9:]:]
let f, g be Function; ::_thesis: ( dom f c= [:X,Y:] & dom g c= [:X9,Y9:] implies dom |:f,g:| c= [:[:X,X9:],[:Y,Y9:]:] )
assume A1: ( dom f c= [:X,Y:] & dom g c= [:X9,Y9:] ) ; ::_thesis: dom |:f,g:| c= [:[:X,X9:],[:Y,Y9:]:]
let xy be set ; :: according to TARSKI:def_3 ::_thesis: ( not xy in dom |:f,g:| or xy in [:[:X,X9:],[:Y,Y9:]:] )
assume  xy in dom |:f,g:| ; ::_thesis: xy in [:[:X,X9:],[:Y,Y9:]:]
then consider x, y, x9, y9 being set  such that
A2: xy = [[x,x9],[y,y9]] and
A3: ( [x,y] in dom f & [x9,y9] in dom g ) by Def3;
 ( y in Y & y9 in Y9 ) by A1, A3, ZFMISC_1:87;
then A4: [y,y9] in [:Y,Y9:] by ZFMISC_1:87;
 ( x in X & x9 in X9 ) by A1, A3, ZFMISC_1:87;
then  [x,x9] in [:X,X9:] by ZFMISC_1:87;
hence  xy in [:[:X,X9:],[:Y,Y9:]:] by A2, A4, ZFMISC_1:87; ::_thesis: verum
end;

theorem Th58: :: FUNCT_4:58
for X, Y, X9, Y9 being set
for f, g being Function st dom f = [:X,Y:] & dom g = [:X9,Y9:] holds
dom |:f,g:| = [:[:X,X9:],[:Y,Y9:]:]
proof
let X, Y, X9, Y9 be set ; ::_thesis: for f, g being Function st dom f = [:X,Y:] & dom g = [:X9,Y9:] holds
dom |:f,g:| = [:[:X,X9:],[:Y,Y9:]:]
let f, g be Function; ::_thesis: ( dom f = [:X,Y:] & dom g = [:X9,Y9:] implies dom |:f,g:| = [:[:X,X9:],[:Y,Y9:]:] )
assume A1: ( dom f = [:X,Y:] & dom g = [:X9,Y9:] ) ; ::_thesis: dom |:f,g:| = [:[:X,X9:],[:Y,Y9:]:]
hence  dom |:f,g:| c= [:[:X,X9:],[:Y,Y9:]:] by Th57; :: according to XBOOLE_0:def_10 ::_thesis: [:[:X,X9:],[:Y,Y9:]:] c= dom |:f,g:|
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in [:[:X,X9:],[:Y,Y9:]:] or z in dom |:f,g:| )
assume  z in [:[:X,X9:],[:Y,Y9:]:] ; ::_thesis: z in dom |:f,g:|
then consider xx, yy being set  such that
A2: xx in [:X,X9:] and
A3: yy in [:Y,Y9:] and
A4: z = [xx,yy] by ZFMISC_1:def_2;
consider y, y9 being set  such that
A5: ( y in Y & y9 in Y9 ) and
A6: yy = [y,y9] by A3, ZFMISC_1:def_2;
consider x, x9 being set  such that
A7: ( x in X & x9 in X9 ) and
A8: xx = [x,x9] by A2, ZFMISC_1:def_2;
 ( [x,y] in dom f & [x9,y9] in dom g ) by A1, A7, A5, ZFMISC_1:87;
hence  z in dom |:f,g:| by A4, A8, A6, Def3; ::_thesis: verum
end;

theorem :: FUNCT_4:59
for X, Y, Z, X9, Y9, Z9 being set
for f being PartFunc of [:X,Y:],Z
for g being PartFunc of [:X9,Y9:],Z9 holds |:f,g:| is PartFunc of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:]
proof
let X, Y, Z, X9, Y9, Z9 be set ; ::_thesis: for f being PartFunc of [:X,Y:],Z
for g being PartFunc of [:X9,Y9:],Z9 holds |:f,g:| is PartFunc of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:]
let f be PartFunc of [:X,Y:],Z; ::_thesis: for g being PartFunc of [:X9,Y9:],Z9 holds |:f,g:| is PartFunc of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:]
let g be PartFunc of [:X9,Y9:],Z9; ::_thesis: |:f,g:| is PartFunc of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:]
 ( rng |:f,g:| c= [:(rng f),(rng g):] & [:(rng f),(rng g):] c= [:Z,Z9:] ) by Th56, ZFMISC_1:96;
then A1: rng |:f,g:| c= [:Z,Z9:] by XBOOLE_1:1;
 ( dom f c= [:X,Y:] & dom g c= [:X9,Y9:] ) ;
then  dom |:f,g:| c= [:[:X,X9:],[:Y,Y9:]:] by Th57;
hence  |:f,g:| is PartFunc of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:] by A1, RELSET_1:4; ::_thesis: verum
end;

theorem Th60: :: FUNCT_4:60
for X, Y, Z, X9, Y9, Z9 being set
for f being Function of [:X,Y:],Z
for g being Function of [:X9,Y9:],Z9 st Z <> {} & Z9 <> {} holds
|:f,g:| is Function of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:]
proof
let X, Y, Z, X9, Y9, Z9 be set ; ::_thesis: for f being Function of [:X,Y:],Z
for g being Function of [:X9,Y9:],Z9 st Z <> {} & Z9 <> {} holds
|:f,g:| is Function of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:]
let f be Function of [:X,Y:],Z; ::_thesis: for g being Function of [:X9,Y9:],Z9 st Z <> {} & Z9 <> {} holds
|:f,g:| is Function of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:]
let g be Function of [:X9,Y9:],Z9; ::_thesis: ( Z <> {} & Z9 <> {} implies |:f,g:| is Function of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:] )
 ( rng |:f,g:| c= [:(rng f),(rng g):] & [:(rng f),(rng g):] c= [:Z,Z9:] ) by Th56, ZFMISC_1:96;
then A1: rng |:f,g:| c= [:Z,Z9:] by XBOOLE_1:1;
assume A2: ( Z <> {} & Z9 <> {} ) ; ::_thesis: |:f,g:| is Function of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:]
then  ( dom f = [:X,Y:] & dom g = [:X9,Y9:] ) by FUNCT_2:def_1;
then  [:[:X,X9:],[:Y,Y9:]:] = dom |:f,g:| by Th58;
then reconsider R = |:f,g:| as Relation of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:] by A1, RELSET_1:4;
 R is quasi_total
proof
percases ( [:Z,Z9:] <> {} or [:Z,Z9:] = {} ) ;
:: according to FUNCT_2:def_1
case [:Z,Z9:] <> {} ; ::_thesis: [:[:X,X9:],[:Y,Y9:]:] = dom R
 ( dom f = [:X,Y:] & dom g = [:X9,Y9:] ) by A2, FUNCT_2:def_1;
hence  [:[:X,X9:],[:Y,Y9:]:] = dom R by Th58; ::_thesis: verum
end;
case [:Z,Z9:] = {} ; ::_thesis: R = {}
hence  R = {} ; ::_thesis: verum
end;
end;
end;
hence  |:f,g:| is Function of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:] ; ::_thesis: verum
end;

theorem :: FUNCT_4:61
for X, Y, X9, Y9 being set
for D, D9 being non empty set
for f being Function of [:X,Y:],D
for g being Function of [:X9,Y9:],D9 holds |:f,g:| is Function of [:[:X,X9:],[:Y,Y9:]:],[:D,D9:] by Th60;

definition
let x, y, a, b be set ;
func(x,y) --> (a,b) ->  set  equals :: FUNCT_4:def 4
(x .--> a) +* (y .--> b);
correctness
coherence
(x .--> a) +* (y .--> b) is set ;
;
end;

:: deftheorem  defines --> FUNCT_4:def_4_:_
 for x, y, a, b being set holds (x,y) --> (a,b) = (x .--> a) +* (y .--> b);

registration
let x, y, a, b be set ;
cluster(x,y) --> (a,b) ->  Relation-like Function-like ;
coherence
 ( (x,y) --> (a,b) is Function-like & (x,y) --> (a,b) is Relation-like ) ;
end;

theorem Th62: :: FUNCT_4:62
for x1, x2, y1, y2 being set holds
( dom ((x1,x2) --> (y1,y2)) = {x1,x2} & rng ((x1,x2) --> (y1,y2)) c= {y1,y2} )
proof
let x1, x2, y1, y2 be set ; ::_thesis: ( dom ((x1,x2) --> (y1,y2)) = {x1,x2} & rng ((x1,x2) --> (y1,y2)) c= {y1,y2} )
set f = {x1} --> y1;
set g = {x2} --> y2;
set h = (x1,x2) --> (y1,y2);
 (rng ({x1} --> y1)) \/ (rng ({x2} --> y2)) c= {y1} \/ {y2} by XBOOLE_1:13;
then A1: (rng ({x1} --> y1)) \/ (rng ({x2} --> y2)) c= {y1,y2} by ENUMSET1:1;
 ( dom ({x1} --> y1) = {x1} & dom ({x2} --> y2) = {x2} ) by FUNCOP_1:13;
then  (dom ({x1} --> y1)) \/ (dom ({x2} --> y2)) = {x1,x2} by ENUMSET1:1;
hence  dom ((x1,x2) --> (y1,y2)) = {x1,x2} by Def1; ::_thesis: rng ((x1,x2) --> (y1,y2)) c= {y1,y2}
 rng ((x1,x2) --> (y1,y2)) c= (rng ({x1} --> y1)) \/ (rng ({x2} --> y2)) by Th17;
hence  rng ((x1,x2) --> (y1,y2)) c= {y1,y2} by A1, XBOOLE_1:1; ::_thesis: verum
end;

theorem Th63: :: FUNCT_4:63
for x1, x2, y1, y2 being set holds
( ( x1 <> x2 implies ((x1,x2) --> (y1,y2)) . x1 = y1 ) & ((x1,x2) --> (y1,y2)) . x2 = y2 )
proof
let x1, x2, y1, y2 be set ; ::_thesis: ( ( x1 <> x2 implies ((x1,x2) --> (y1,y2)) . x1 = y1 ) & ((x1,x2) --> (y1,y2)) . x2 = y2 )
set f = {x1} --> y1;
set g = {x2} --> y2;
set h = (x1,x2) --> (y1,y2);
A1: x2 in {x2} by TARSKI:def_1;
A2: x1 in {x1} by TARSKI:def_1;
hereby  ::_thesis: ((x1,x2) --> (y1,y2)) . x2 = y2
assume  x1 <> x2 ; ::_thesis: ((x1,x2) --> (y1,y2)) . x1 = y1
then  not x1 in dom ({x2} --> y2) by TARSKI:def_1;
then  ((x1,x2) --> (y1,y2)) . x1 = ({x1} --> y1) . x1 by Th11;
hence  ((x1,x2) --> (y1,y2)) . x1 = y1 by A2, FUNCOP_1:7; ::_thesis: verum
end;
 {x2} = dom ({x2} --> y2) by FUNCOP_1:13;
then  ((x1,x2) --> (y1,y2)) . x2 = ({x2} --> y2) . x2 by A1, Th13;
hence  ((x1,x2) --> (y1,y2)) . x2 = y2 by A1, FUNCOP_1:7; ::_thesis: verum
end;

theorem :: FUNCT_4:64
for x1, x2, y1, y2 being set st x1 <> x2 holds
rng ((x1,x2) --> (y1,y2)) = {y1,y2}
proof
let x1, x2, y1, y2 be set ; ::_thesis: ( x1 <> x2 implies rng ((x1,x2) --> (y1,y2)) = {y1,y2} )
set h = (x1,x2) --> (y1,y2);
assume A1: x1 <> x2 ; ::_thesis: rng ((x1,x2) --> (y1,y2)) = {y1,y2}
thus  rng ((x1,x2) --> (y1,y2)) c= {y1,y2} by Th62; :: according to XBOOLE_0:def_10 ::_thesis: {y1,y2} c= rng ((x1,x2) --> (y1,y2))
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {y1,y2} or y in rng ((x1,x2) --> (y1,y2)) )
assume  y in {y1,y2} ; ::_thesis: y in rng ((x1,x2) --> (y1,y2))
then  ( y = y1 or y = y2 ) by TARSKI:def_2;
then A2: ( ((x1,x2) --> (y1,y2)) . x1 = y or ((x1,x2) --> (y1,y2)) . x2 = y ) by A1, Th63;
 dom ((x1,x2) --> (y1,y2)) = {x1,x2} by Th62;
then  ( x1 in dom ((x1,x2) --> (y1,y2)) & x2 in dom ((x1,x2) --> (y1,y2)) ) by TARSKI:def_2;
hence  y in rng ((x1,x2) --> (y1,y2)) by A2, FUNCT_1:def_3; ::_thesis: verum
end;

theorem :: FUNCT_4:65
for x1, x2, y being set holds (x1,x2) --> (y,y) = {x1,x2} --> y
proof
let x1, x2, y be set ; ::_thesis: (x1,x2) --> (y,y) = {x1,x2} --> y
set F = (x1,x2) --> (y,y);
set f = {x1} --> y;
set g = {x2} --> y;
set F9 = {x1,x2} --> y;
now__::_thesis:_(_dom_((x1,x2)_-->_(y,y))_=_{x1,x2}_&_dom_({x1,x2}_-->_y)_=_{x1,x2}_&_(_for_x_being_set_st_x_in_{x1,x2}_holds_
((x1,x2)_-->_(y,y))_._x_=_({x1,x2}_-->_y)_._x_)_)
thus A1: ( dom ((x1,x2) --> (y,y)) = {x1,x2} & dom ({x1,x2} --> y) = {x1,x2} ) by Th62, FUNCOP_1:13; ::_thesis: for x being set st x in {x1,x2} holds
((x1,x2) --> (y,y)) . x = ({x1,x2} --> y) . x
let x be set ; ::_thesis: ( x in {x1,x2} implies ((x1,x2) --> (y,y)) . x = ({x1,x2} --> y) . x )
assume A2: x in {x1,x2} ; ::_thesis: ((x1,x2) --> (y,y)) . x = ({x1,x2} --> y) . x
now__::_thesis:_(_((x1,x2)_-->_(y,y))_._x_=_y_&_({x1,x2}_-->_y)_._x_=_y_)
percases ( ( x in dom ({x1} --> y) & not x in dom ({x2} --> y) ) or x in dom ({x2} --> y) ) by A1, A2, Th12;
supposeA3: ( x in dom ({x1} --> y) & not x in dom ({x2} --> y) ) ; ::_thesis: ( ((x1,x2) --> (y,y)) . x = y & ({x1,x2} --> y) . x = y )
then  ((x1,x2) --> (y,y)) . x = ({x1} --> y) . x by Th11;
hence  ( ((x1,x2) --> (y,y)) . x = y & ({x1,x2} --> y) . x = y ) by A2, A3, FUNCOP_1:7; ::_thesis: verum
end;
supposeA4: x in dom ({x2} --> y) ; ::_thesis: ( ((x1,x2) --> (y,y)) . x = y & ({x1,x2} --> y) . x = y )
then  ((x1,x2) --> (y,y)) . x = ({x2} --> y) . x by Th13;
hence  ( ((x1,x2) --> (y,y)) . x = y & ({x1,x2} --> y) . x = y ) by A2, A4, FUNCOP_1:7; ::_thesis: verum
end;
end;
end;
hence  ((x1,x2) --> (y,y)) . x = ({x1,x2} --> y) . x ; ::_thesis: verum
end;
hence  (x1,x2) --> (y,y) = {x1,x2} --> y by FUNCT_1:2; ::_thesis: verum
end;

definition
let A be non empty set ;
let x1, x2 be set ;
let y1, y2 be Element of A;
:: original: -->
redefine func(x1,x2) --> (y1,y2) ->  Function of {x1,x2},A;
coherence
 (x1,x2) --> (y1,y2) is Function of {x1,x2},A
proof
set f = {x1} --> y1;
set g = {x2} --> y2;
set h = (x1,x2) --> (y1,y2);
 rng ((x1,x2) --> (y1,y2)) c= (rng ({x1} --> y1)) \/ (rng ({x2} --> y2)) by Th17;
then A1: rng ((x1,x2) --> (y1,y2)) c= A by XBOOLE_1:1;
 dom ((x1,x2) --> (y1,y2)) = {x1,x2} by Th62;
hence  (x1,x2) --> (y1,y2) is Function of {x1,x2},A by A1, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
end;

theorem :: FUNCT_4:66
for a, b, c, d being set
for g being Function st dom g = {a,b} & g . a = c & g . b = d holds
g = (a,b) --> (c,d)
proof
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 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_set_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 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 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 ({a} --> c) = {a} & dom ({b} --> d) = {b} ) by FUNCOP_1:13;
then  dom h = (dom ({a} --> c)) \/ (dom ({b} --> d)) by A1, ENUMSET1:1;
hence  h = (a,b) --> (c,d) by A6, Def1; ::_thesis: verum
end;

theorem Th67: :: FUNCT_4:67
for a, b, c, d being set st a <> c holds
(a,c) --> (b,d) = {[a,b],[c,d]}
proof
let a, b, c, d be set ; ::_thesis: ( a <> c implies (a,c) --> (b,d) = {[a,b],[c,d]} )
assume A1: a <> c ; ::_thesis: (a,c) --> (b,d) = {[a,b],[c,d]}
set f = {a} --> b;
set g = {c} --> d;
A2: ( dom ({a} --> b) = {a} & dom ({c} --> d) = {c} ) by FUNCOP_1:13;
 ( {a} --> b = {[a,b]} & {c} --> d = {[c,d]} ) by ZFMISC_1:29;
hence (a,c) --> (b,d) = {[a,b]} \/ {[c,d]} by A1, A2, Th31, ZFMISC_1:11
.= {[a,b],[c,d]} by ENUMSET1:1 ;
::_thesis: verum
end;

theorem :: FUNCT_4:68
for a, b, x, y, x9, y9 being set st a <> b & (a,b) --> (x,y) = (a,b) --> (x9,y9) holds
( x = x9 & y = y9 )
proof
let a, b, x, y, x9, y9 be set ; ::_thesis: ( a <> b & (a,b) --> (x,y) = (a,b) --> (x9,y9) implies ( x = x9 & y = y9 ) )
assume that
A1: a <> b and
A2: (a,b) --> (x,y) = (a,b) --> (x9,y9) ; ::_thesis: ( x = x9 & y = y9 )
thus x = ((a,b) --> (x,y)) . a by A1, Th63
.= x9 by A1, A2, Th63 ; ::_thesis: y = y9
thus y = ((a,b) --> (x,y)) . b by Th63
.= y9 by A2, Th63 ; ::_thesis: verum
end;

begin

theorem :: FUNCT_4:69
for f1, f2, g1, g2 being Function st rng g1 c= dom f1 & rng g2 c= dom f2 & f1 tolerates f2 holds
(f1 +* f2) * (g1 +* g2) = (f1 * g1) +* (f2 * g2)
proof
let f1, f2, g1, g2 be Function; ::_thesis: ( rng g1 c= dom f1 & rng g2 c= dom f2 & f1 tolerates f2 implies (f1 +* f2) * (g1 +* g2) = (f1 * g1) +* (f2 * g2) )
assume that
A1: ( rng g1 c= dom f1 & rng g2 c= dom f2 ) and
A2: f1 tolerates f2 ; ::_thesis: (f1 +* f2) * (g1 +* g2) = (f1 * g1) +* (f2 * g2)
A3: ( rng (g1 +* g2) c= (rng g1) \/ (rng g2) & dom (f1 +* f2) = (dom f1) \/ (dom f2) ) by Def1, Th17;
 (rng g1) \/ (rng g2) c= (dom f1) \/ (dom f2) by A1, XBOOLE_1:13;
then A4: dom ((f1 +* f2) * (g1 +* g2)) = dom (g1 +* g2) by A3, RELAT_1:27, XBOOLE_1:1
.= (dom g1) \/ (dom g2) by Def1 ;
A5: ( dom (f1 * g1) = dom g1 & dom (f2 * g2) = dom g2 ) by A1, RELAT_1:27;
A6: now__::_thesis:_for_x_being_set_st_x_in_(dom_g1)_\/_(dom_g2)_holds_
((f1_+*_f2)_*_(g1_+*_g2))_._x_=_((f1_*_g1)_+*_(f2_*_g2))_._x
let x be set ; ::_thesis: ( x in (dom g1) \/ (dom g2) implies ((f1 +* f2) * (g1 +* g2)) . x = ((f1 * g1) +* (f2 * g2)) . x )
A7: ( not x in dom g2 or x in dom g2 ) ;
assume A8: x in (dom g1) \/ (dom g2) ; ::_thesis: ((f1 +* f2) * (g1 +* g2)) . x = ((f1 * g1) +* (f2 * g2)) . x
then A9: ((f1 +* f2) * (g1 +* g2)) . x = (f1 +* f2) . ((g1 +* g2) . x) by A4, FUNCT_1:12;
 ( x in dom g1 or x in dom g2 ) by A8, XBOOLE_0:def_3;
then  ( ( (g1 +* g2) . x = g1 . x & ((f1 * g1) +* (f2 * g2)) . x = (f1 * g1) . x & (f1 * g1) . x = f1 . (g1 . x) & g1 . x in rng g1 & ( g1 . x in rng g1 implies g1 . x in dom f1 ) ) or ( (g1 +* g2) . x = g2 . x & ((f1 * g1) +* (f2 * g2)) . x = (f2 * g2) . x & (f2 * g2) . x = f2 . (g2 . x) & g2 . x in rng g2 & ( g2 . x in rng g2 implies g2 . x in dom f2 ) ) ) by A1, A5, A8, A7, Def1, FUNCT_1:12, FUNCT_1:def_3;
hence  ((f1 +* f2) * (g1 +* g2)) . x = ((f1 * g1) +* (f2 * g2)) . x by A2, A9, Th13, Th15; ::_thesis: verum
end;
 dom ((f1 * g1) +* (f2 * g2)) = (dom g1) \/ (dom g2) by A5, Def1;
hence  (f1 +* f2) * (g1 +* g2) = (f1 * g1) +* (f2 * g2) by A4, A6, FUNCT_1:2; ::_thesis: verum
end;


theorem Th70: :: FUNCT_4:70
for f being Function
for A, B being set st dom f c= A \/ B holds
(f | A) +* (f | B) = f
proof
let f be Function; ::_thesis: for A, B being set st dom f c= A \/ B holds
(f | A) +* (f | B) = f
let A, B be set ; ::_thesis: ( dom f c= A \/ B implies (f | A) +* (f | B) = f )
A1: ( dom (f | A) = (dom f) /\ A & dom (f | B) = (dom f) /\ B ) by RELAT_1:61;
A2: for x being set st x in (dom (f | A)) \/ (dom (f | B)) holds
( ( x in dom (f | B) implies f . x = (f | B) . x ) & ( not x in dom (f | B) implies f . x = (f | A) . x ) )
proof
let x be set ; ::_thesis: ( x in (dom (f | A)) \/ (dom (f | B)) implies ( ( x in dom (f | B) implies f . x = (f | B) . x ) & ( not x in dom (f | B) implies f . x = (f | A) . x ) ) )
assume A3: x in (dom (f | A)) \/ (dom (f | B)) ; ::_thesis: ( ( x in dom (f | B) implies f . x = (f | B) . x ) & ( not x in dom (f | B) implies f . x = (f | A) . x ) )
thus  ( x in dom (f | B) implies f . x = (f | B) . x ) by FUNCT_1:47; ::_thesis: ( not x in dom (f | B) implies f . x = (f | A) . x )
assume  not x in dom (f | B) ; ::_thesis: f . x = (f | A) . x
then  x in dom (f | A) by A3, XBOOLE_0:def_3;
hence  f . x = (f | A) . x by FUNCT_1:47; ::_thesis: verum
end;
assume  dom f c= A \/ B ; ::_thesis: (f | A) +* (f | B) = f
then  dom f = (dom f) /\ (A \/ B) by XBOOLE_1:28
.= (dom (f | A)) \/ (dom (f | B)) by A1, XBOOLE_1:23 ;
hence  (f | A) +* (f | B) = f by A2, Def1; ::_thesis: verum
end;

theorem Th71: :: FUNCT_4:71
for p, q being Function
for A being set holds (p +* q) | A = (p | A) +* (q | A)
proof
let p, q be Function; ::_thesis: for A being set holds (p +* q) | A = (p | A) +* (q | A)
let A be set ; ::_thesis: (p +* q) | A = (p | A) +* (q | A)
A1: dom ((p +* q) | A) = (dom (p +* q)) /\ A by RELAT_1:61
.= ((dom p) \/ (dom q)) /\ A by Def1
.= ((dom p) /\ A) \/ ((dom q) /\ A) by XBOOLE_1:23
.= (dom (p | A)) \/ ((dom q) /\ A) by RELAT_1:61
.= (dom (p | A)) \/ (dom (q | A)) by RELAT_1:61 ;
 for x being set st x in (dom (p | A)) \/ (dom (q | A)) holds
( ( x in dom (q | A) implies ((p +* q) | A) . x = (q | A) . x ) & ( not x in dom (q | A) implies ((p +* q) | A) . x = (p | A) . x ) )
proof
let x be set ; ::_thesis: ( x in (dom (p | A)) \/ (dom (q | A)) implies ( ( x in dom (q | A) implies ((p +* q) | A) . x = (q | A) . x ) & ( not x in dom (q | A) implies ((p +* q) | A) . x = (p | A) . x ) ) )
assume A2: x in (dom (p | A)) \/ (dom (q | A)) ; ::_thesis: ( ( x in dom (q | A) implies ((p +* q) | A) . x = (q | A) . x ) & ( not x in dom (q | A) implies ((p +* q) | A) . x = (p | A) . x ) )
then  ( x in dom (p | A) or x in dom (q | A) ) by XBOOLE_0:def_3;
then  ( x in (dom p) /\ A or x in (dom q) /\ A ) by RELAT_1:61;
then A3: x in A by XBOOLE_0:def_4;
hereby  ::_thesis: ( not x in dom (q | A) implies ((p +* q) | A) . x = (p | A) . x )
assume A4: x in dom (q | A) ; ::_thesis: ((p +* q) | A) . x = (q | A) . x
then  x in (dom q) /\ A by RELAT_1:61;
then A5: x in dom q by XBOOLE_0:def_4;
thus ((p +* q) | A) . x = (p +* q) . x by A1, A2, FUNCT_1:47
.= q . x by A5, Th13
.= (q | A) . x by A4, FUNCT_1:47 ; ::_thesis: verum
end;
assume A6: not x in dom (q | A) ; ::_thesis: ((p +* q) | A) . x = (p | A) . x
then  not x in (dom q) /\ A by RELAT_1:61;
then A7: not x in dom q by A3, XBOOLE_0:def_4;
A8: x in dom (p | A) by A2, A6, XBOOLE_0:def_3;
then  x in (dom p) /\ A by RELAT_1:61;
then  x in dom p by XBOOLE_0:def_4;
then  x in dom (p +* q) by Th12;
then  x in (dom (p +* q)) /\ A by A3, XBOOLE_0:def_4;
then  x in dom ((p +* q) | A) by RELAT_1:61;
hence ((p +* q) | A) . x = (p +* q) . x by FUNCT_1:47
.= p . x by A7, Th11
.= (p | A) . x by A8, FUNCT_1:47 ;
::_thesis: verum
end;
hence  (p +* q) | A = (p | A) +* (q | A) by A1, Def1; ::_thesis: verum
end;

theorem Th72: :: FUNCT_4:72
for f, g being Function
for A being set st A misses dom g holds
(f +* g) | A = f | A
proof
let f, g be Function; ::_thesis: for A being set st A misses dom g holds
(f +* g) | A = f | A
let A be set ; ::_thesis: ( A misses dom g implies (f +* g) | A = f | A )
assume  A misses dom g ; ::_thesis: (f +* g) | A = f | A
then  (dom g) /\ A = {} by XBOOLE_0:def_7;
then  dom (g | A) = {} by RELAT_1:61;
then  g | A = {} ;
hence (f +* g) | A = (f | A) +* {} by Th71
.= f | A ;
::_thesis: verum
end;

theorem :: FUNCT_4:73
for f, g being Function
for A being set st dom f misses A holds
(f +* g) | A = g | A
proof
let f, g be Function; ::_thesis: for A being set st dom f misses A holds
(f +* g) | A = g | A
let A be set ; ::_thesis: ( dom f misses A implies (f +* g) | A = g | A )
assume  dom f misses A ; ::_thesis: (f +* g) | A = g | A
then  (dom f) /\ A = {} by XBOOLE_0:def_7;
then  dom (f | A) = {} by RELAT_1:61;
then  f | A = {} ;
hence (f +* g) | A = {} +* (g | A) by Th71
.= g | A ;
::_thesis: verum
end;

theorem :: FUNCT_4:74
for f, g, h being Function st dom g = dom h holds
(f +* g) +* h = f +* h
proof
let f, g, h be Function; ::_thesis: ( dom g = dom h implies (f +* g) +* h = f +* h )
assume A1: dom g = dom h ; ::_thesis: (f +* g) +* h = f +* h
thus (f +* g) +* h = f +* (g +* h) by Th14
.= f +* h by A1, Th19 ; ::_thesis: verum
end;

Lm2:  for f, g being Function st f c= g holds
g +* f = g
proof
let f, g be Function; ::_thesis: ( f c= g implies g +* f = g )
assume A1: f c= g ; ::_thesis: g +* f = g
then  f tolerates g by PARTFUN1:54;
hence g +* f = f \/ g by Th30
.= g by A1, XBOOLE_1:12 ;
::_thesis: verum
end;

theorem :: FUNCT_4:75
for f being Function
for A being set holds f +* (f | A) = f by Lm2, RELAT_1:59;

theorem :: FUNCT_4:76
for f, g being Function
for B, C being set st dom f c= B & dom g c= C & B misses C holds
( (f +* g) | B = f & (f +* g) | C = g )
proof
let f, g be Function; ::_thesis: for B, C being set st dom f c= B & dom g c= C & B misses C holds
( (f +* g) | B = f & (f +* g) | C = g )
let B, C be set ; ::_thesis: ( dom f c= B & dom g c= C & B misses C implies ( (f +* g) | B = f & (f +* g) | C = g ) )
assume that
A1: dom f c= B and
A2: dom g c= C and
A3: B misses C ; ::_thesis: ( (f +* g) | B = f & (f +* g) | C = g )
 dom f misses C by A1, A3, XBOOLE_1:63;
then  (dom f) /\ C = {} by XBOOLE_0:def_7;
then  dom (f | C) = {} by RELAT_1:61;
then A4: f | C = {} ;
 dom g misses B by A2, A3, XBOOLE_1:63;
then  (dom g) /\ B = {} by XBOOLE_0:def_7;
then  dom (g | B) = {} by RELAT_1:61;
then A5: g | B = {} ;
thus (f +* g) | B = (f | B) +* (g | B) by Th71
.= f | B by A5, Th21
.= f by A1, RELAT_1:68 ; ::_thesis: (f +* g) | C = g
thus (f +* g) | C = (f | C) +* (g | C) by Th71
.= g | C by A4, Th20
.= g by A2, RELAT_1:68 ; ::_thesis: verum
end;

theorem :: FUNCT_4:77
for p, q being Function
for A being set st dom p c= A & dom q misses A holds
(p +* q) | A = p
proof
let p, q be Function; ::_thesis: for A being set st dom p c= A & dom q misses A holds
(p +* q) | A = p
let A be set ; ::_thesis: ( dom p c= A & dom q misses A implies (p +* q) | A = p )
assume that
A1: dom p c= A and
A2: dom q misses A ; ::_thesis: (p +* q) | A = p
thus (p +* q) | A = p | A by A2, Th72
.= p by A1, RELAT_1:68 ; ::_thesis: verum
end;

theorem :: FUNCT_4:78
for f being Function
for A, B being set holds f | (A \/ B) = (f | A) +* (f | B)
proof
let f be Function; ::_thesis: for A, B being set holds f | (A \/ B) = (f | A) +* (f | B)
let A, B be set ; ::_thesis: f | (A \/ B) = (f | A) +* (f | B)
A1: (f | (A \/ B)) | B = f | ((A \/ B) /\ B) by RELAT_1:71
.= f | B by XBOOLE_1:21 ;
A2: dom (f | (A \/ B)) c= A \/ B by RELAT_1:58;
(f | (A \/ B)) | A = f | ((A \/ B) /\ A) by RELAT_1:71
.= f | A by XBOOLE_1:21 ;
hence  f | (A \/ B) = (f | A) +* (f | B) by A1, A2, Th70; ::_thesis: verum
end;


theorem :: FUNCT_4:79
for i, j, k being set holds (i,j) :-> k = [i,j] .--> k ;

theorem :: FUNCT_4:80
for i, j, k being set holds ((i,j) :-> k) . (i,j) = k by FUNCOP_1:71;

theorem :: FUNCT_4:81
for a, b, c being set holds (a,a) --> (b,c) = a .--> c
proof
let a, b, c be set ; ::_thesis: (a,a) --> (b,c) = a .--> c
dom (a .--> c) = {a} by FUNCOP_1:13
.= dom ({a} --> b) by FUNCOP_1:13 ;
hence  (a,a) --> (b,c) = a .--> c by Th19; ::_thesis: verum
end;

theorem :: FUNCT_4:82
for x, y being set holds x .--> y = {[x,y]} by ZFMISC_1:29;

theorem :: FUNCT_4:83
for f being Function
for a, b, c being set st a <> c holds
(f +* (a .--> b)) . c = f . c
proof
let f be Function; ::_thesis: for a, b, c being set st a <> c holds
(f +* (a .--> b)) . c = f . c
let a, b, c be set ; ::_thesis: ( a <> c implies (f +* (a .--> b)) . c = f . c )
assume A1: a <> c ; ::_thesis: (f +* (a .--> b)) . c = f . c
set g = a .--> b;
 not c in dom (a .--> b) by A1, TARSKI:def_1;
hence  (f +* (a .--> b)) . c = f . c by Th11; ::_thesis: verum
end;

theorem :: FUNCT_4:84
for f being Function
for a, b, c, d being set st a <> b holds
( (f +* ((a,b) --> (c,d))) . a = c & (f +* ((a,b) --> (c,d))) . b = d )
proof
let f be Function; ::_thesis: for a, b, c, d being set st a <> b holds
( (f +* ((a,b) --> (c,d))) . a = c & (f +* ((a,b) --> (c,d))) . b = d )
let a, b, c, d be set ; ::_thesis: ( a <> b implies ( (f +* ((a,b) --> (c,d))) . a = c & (f +* ((a,b) --> (c,d))) . b = d ) )
assume A1: a <> b ; ::_thesis: ( (f +* ((a,b) --> (c,d))) . a = c & (f +* ((a,b) --> (c,d))) . b = d )
set g = (a,b) --> (c,d);
A2: dom ((a,b) --> (c,d)) = {a,b} by Th62;
then  a in dom ((a,b) --> (c,d)) by TARSKI:def_2;
hence (f +* ((a,b) --> (c,d))) . a = ((a,b) --> (c,d)) . a by Th13
.= c by A1, Th63 ;
::_thesis: (f +* ((a,b) --> (c,d))) . b = d
 b in dom ((a,b) --> (c,d)) by A2, TARSKI:def_2;
hence (f +* ((a,b) --> (c,d))) . b = ((a,b) --> (c,d)) . b by Th13
.= d by Th63 ;
::_thesis: verum
end;

theorem Th85: :: FUNCT_4:85
for a, b being set
for f being Function st a in dom f & f . a = b holds
a .--> b c= f
proof
let a, b be set ; ::_thesis: for f being Function st a in dom f & f . a = b holds
a .--> b c= f
let f be Function; ::_thesis: ( a in dom f & f . a = b implies a .--> b c= f )
assume  ( a in dom f & f . a = b ) ; ::_thesis: a .--> b c= f
then  [a,b] in f by FUNCT_1:1;
then  {[a,b]} c= f by ZFMISC_1:31;
hence  a .--> b c= f by ZFMISC_1:29; ::_thesis: verum
end;

theorem :: FUNCT_4:86
for a, b, c, d being set
for f being Function st a in dom f & c in dom f & f . a = b & f . c = d holds
(a,c) --> (b,d) c= f
proof
let a, b, c, d be set ; ::_thesis: for f being Function st a in dom f & c in dom f & f . a = b & f . c = d holds
(a,c) --> (b,d) c= f
let f be Function; ::_thesis: ( a in dom f & c in dom f & f . a = b & f . c = d implies (a,c) --> (b,d) c= f )
assume that
A1: a in dom f and
A2: c in dom f and
A3: ( f . a = b & f . c = d ) ; ::_thesis: (a,c) --> (b,d) c= f
percases ( a <> c or a = c ) ;
supposeA4: a <> c ; ::_thesis: (a,c) --> (b,d) c= f
 ( [a,b] in f & [c,d] in f ) by A1, A2, A3, FUNCT_1:1;
then  {[a,b],[c,d]} c= f by ZFMISC_1:32;
hence  (a,c) --> (b,d) c= f by A4, Th67; ::_thesis: verum
end;
suppose a = c ; ::_thesis: (a,c) --> (b,d) c= f
hence  (a,c) --> (b,d) c= f by A1, A3, Th85; ::_thesis: verum
end;
end;
end;

theorem Th87: :: FUNCT_4:87
for f, g, h being Function st f c= h & g c= h holds
f +* g c= h
proof
let f, g, h be Function; ::_thesis: ( f c= h & g c= h implies f +* g c= h )
assume  ( f c= h & g c= h ) ; ::_thesis: f +* g c= h
then A1: f \/ g c= h by XBOOLE_1:8;
 f +* g c= f \/ g by Th29;
hence  f +* g c= h by A1, XBOOLE_1:1; ::_thesis: verum
end;

theorem :: FUNCT_4:88
for f, g being Function
for A being set st A /\ (dom f) c= A /\ (dom g) holds
(f +* (g | A)) | A = g | A
proof
let f, g be Function; ::_thesis: for A being set st A /\ (dom f) c= A /\ (dom g) holds
(f +* (g | A)) | A = g | A
let A be set ; ::_thesis: ( A /\ (dom f) c= A /\ (dom g) implies (f +* (g | A)) | A = g | A )
assume A1: A /\ (dom f) c= A /\ (dom g) ; ::_thesis: (f +* (g | A)) | A = g | A
A2: ( dom (f | A) = A /\ (dom f) & dom (g | A) = A /\ (dom g) ) by RELAT_1:61;
thus (f +* (g | A)) | A = (f | A) +* ((g | A) | A) by Th71
.= (f | A) +* (g | A)
.= g | A by A1, A2, Th19 ; ::_thesis: verum
end;

theorem :: FUNCT_4:89
for f being Function
for a, b, n, m being set holds ((f +* (a .--> b)) +* (m .--> n)) . m = n
proof
let f be Function; ::_thesis: for a, b, n, m being set holds ((f +* (a .--> b)) +* (m .--> n)) . m = n
let a, b, n, m be set ; ::_thesis: ((f +* (a .--> b)) +* (m .--> n)) . m = n
set mn = m .--> n;
 dom (m .--> n) = {m} by FUNCOP_1:13;
then  m in dom (m .--> n) by TARSKI:def_1;
hence ((f +* (a .--> b)) +* (m .--> n)) . m = (m .--> n) . m by Th13
.= n by FUNCOP_1:72 ;
::_thesis: verum
end;

theorem :: FUNCT_4:90
for f being Function
for n, m being set holds ((f +* (n .--> m)) +* (m .--> n)) . n = m
proof
let f be Function; ::_thesis: for n, m being set holds ((f +* (n .--> m)) +* (m .--> n)) . n = m
let n, m be set ; ::_thesis: ((f +* (n .--> m)) +* (m .--> n)) . n = m
set mn = m .--> n;
set nm = n .--> m;
 dom (m .--> n) = {m} by FUNCOP_1:13;
then A1: m in dom (m .--> n) by TARSKI:def_1;
percases ( n = m or n <> m ) ;
supposeA2: n = m ; ::_thesis: ((f +* (n .--> m)) +* (m .--> n)) . n = m
hence ((f +* (n .--> m)) +* (m .--> n)) . n = (m .--> n) . m by A1, Th13
.= m by A2, FUNCOP_1:72 ;
::_thesis: verum
end;
supposeA3: n <> m ; ::_thesis: ((f +* (n .--> m)) +* (m .--> n)) . n = m
 dom (n .--> m) = {n} by FUNCOP_1:13;
then A4: n in dom (n .--> m) by TARSKI:def_1;
 not n in dom (m .--> n) by A3, TARSKI:def_1;
hence ((f +* (n .--> m)) +* (m .--> n)) . n = (f +* (n .--> m)) . n by Th11
.= (n .--> m) . n by A4, Th13
.= m by FUNCOP_1:72 ;
::_thesis: verum
end;
end;
end;

theorem :: FUNCT_4:91
for f being Function
for a, b, n, m, x being set st x <> m & x <> a holds
((f +* (a .--> b)) +* (m .--> n)) . x = f . x
proof
let f be Function; ::_thesis: for a, b, n, m, x being set st x <> m & x <> a holds
((f +* (a .--> b)) +* (m .--> n)) . x = f . x
let a, b, n, m, x be set ; ::_thesis: ( x <> m & x <> a implies ((f +* (a .--> b)) +* (m .--> n)) . x = f . x )
assume that
A1: x <> m and
A2: x <> a ; ::_thesis: ((f +* (a .--> b)) +* (m .--> n)) . x = f . x
set mn = m .--> n;
set nm = a .--> b;
A3: not x in dom (a .--> b) by A2, TARSKI:def_1;
 not x in dom (m .--> n) by A1, TARSKI:def_1;
hence ((f +* (a .--> b)) +* (m .--> n)) . x = (f +* (a .--> b)) . x by Th11
.= f . x by A3, Th11 ;
::_thesis: verum
end;

theorem :: FUNCT_4:92
for f, g being Function st f is one-to-one & g is one-to-one & rng f misses rng g holds
f +* g is one-to-one
proof
let f, g be Function; ::_thesis: ( f is one-to-one & g is one-to-one & rng f misses rng g implies f +* g is one-to-one )
assume that
A1: f is one-to-one and
A2: g is one-to-one and
A3: rng f misses rng g ; ::_thesis: f +* g is one-to-one
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom (f +* g) or not x2 in dom (f +* g) or not (f +* g) . x1 = (f +* g) . x2 or x1 = x2 )
set fg = f +* g;
assume that
A4: x1 in dom (f +* g) and
A5: x2 in dom (f +* g) and
A6: (f +* g) . x1 = (f +* g) . x2 ; ::_thesis: x1 = x2
A7: ( x1 in dom f or x1 in dom g ) by A4, Th12;
A8: ( x2 in dom f or x2 in dom g ) by A5, Th12;
percases ( ( x1 in dom g & x2 in dom g ) or ( x1 in dom g & not x2 in dom g ) or ( not x1 in dom g & x2 in dom g ) or ( not x1 in dom g & not x2 in dom g ) ) ;
supposeA9: ( x1 in dom g & x2 in dom g ) ; ::_thesis: x1 = x2
then  ( (f +* g) . x1 = g . x1 & (f +* g) . x2 = g . x2 ) by Th13;
hence  x1 = x2 by A2, A6, A9, FUNCT_1:def_4; ::_thesis: verum
end;
supposeA10: ( x1 in dom g & not x2 in dom g ) ; ::_thesis: x1 = x2
then  x2 in dom f by A5, Th12;
then A11: f . x2 in rng f by FUNCT_1:def_3;
A12: g . x1 in rng g by A10, FUNCT_1:def_3;
 ( (f +* g) . x1 = g . x1 & (f +* g) . x2 = f . x2 ) by A10, Th11, Th13;
hence  x1 = x2 by A3, A6, A12, A11, XBOOLE_0:3; ::_thesis: verum
end;
supposeA13: ( not x1 in dom g & x2 in dom g ) ; ::_thesis: x1 = x2
then  x1 in dom f by A4, Th12;
then A14: f . x1 in rng f by FUNCT_1:def_3;
A15: g . x2 in rng g by A13, FUNCT_1:def_3;
 ( (f +* g) . x1 = f . x1 & (f +* g) . x2 = g . x2 ) by A13, Th11, Th13;
hence  x1 = x2 by A3, A6, A15, A14, XBOOLE_0:3; ::_thesis: verum
end;
supposeA16: ( not x1 in dom g & not x2 in dom g ) ; ::_thesis: x1 = x2
then  ( (f +* g) . x1 = f . x1 & (f +* g) . x2 = f . x2 ) by Th11;
hence  x1 = x2 by A1, A6, A7, A8, A16, FUNCT_1:def_4; ::_thesis: verum
end;
end;
end;

registration
let f, g be Function;
reduce(f +* g) +* g to f +* g;
reducibility
 (f +* g) +* g = f +* g
proof
thus (f +* g) +* g = f +* (g +* g) by Th14
.= f +* g ; ::_thesis: verum
end;
end;

theorem :: FUNCT_4:93
for f, g being Function holds (f +* g) +* g = f +* g ;

theorem :: FUNCT_4:94
for f, g, h being Function
for D being set st (f +* g) | D = h | D holds
(h +* g) | D = (f +* g) | D
proof
let f, g, h be Function; ::_thesis: for D being set st (f +* g) | D = h | D holds
(h +* g) | D = (f +* g) | D
let D be set ; ::_thesis: ( (f +* g) | D = h | D implies (h +* g) | D = (f +* g) | D )
assume A1: (f +* g) | D = h | D ; ::_thesis: (h +* g) | D = (f +* g) | D
A2: dom ((f +* g) | D) = (dom (f +* g)) /\ D by RELAT_1:61
.= ((dom f) \/ (dom g)) /\ D by Def1 ;
A3: dom ((h +* g) | D) = (dom (h +* g)) /\ D by RELAT_1:61
.= ((dom h) \/ (dom g)) /\ D by Def1 ;
then A4: dom ((h +* g) | D) = ((dom h) /\ D) \/ ((dom g) /\ D) by XBOOLE_1:23
.= (((dom f) \/ (dom g)) /\ D) \/ ((dom g) /\ D) by A1, A2, RELAT_1:61
.= (((dom f) \/ (dom g)) \/ (dom g)) /\ D by XBOOLE_1:23
.= ((dom f) \/ ((dom g) \/ (dom g))) /\ D by XBOOLE_1:4
.= ((dom f) \/ (dom g)) /\ D ;
now__::_thesis:_for_x_being_set_st_x_in_dom_((f_+*_g)_|_D)_holds_
((h_+*_g)_|_D)_._x_=_((f_+*_g)_|_D)_._x
let x be set ; ::_thesis: ( x in dom ((f +* g) | D) implies ((h +* g) | D) . b1 = ((f +* g) | D) . b1 )
assume A5: x in dom ((f +* g) | D) ; ::_thesis: ((h +* g) | D) . b1 = ((f +* g) | D) . b1
then A6: x in (dom f) \/ (dom g) by A2, XBOOLE_0:def_4;
A7: x in D by A2, A5, XBOOLE_0:def_4;
A8: ( x in (dom h) \/ (dom g) & ((h +* g) | D) . x = (h +* g) . x ) by A2, A3, A4, A5, FUNCT_1:47, XBOOLE_0:def_4;
percases ( x in dom g or not x in dom g ) ;
supposeA9: x in dom g ; ::_thesis: ((h +* g) | D) . b1 = ((f +* g) | D) . b1
((f +* g) | D) . x = (f +* g) . x by A5, FUNCT_1:47
.= g . x by A6, A9, Def1 ;
hence  ((h +* g) | D) . x = ((f +* g) | D) . x by A8, A9, Def1; ::_thesis: verum
end;
suppose not x in dom g ; ::_thesis: ((h +* g) | D) . b1 = ((f +* g) | D) . b1
hence ((h +* g) | D) . x = h . x by A8, Def1
.= ((f +* g) | D) . x by A1, A7, FUNCT_1:49 ;
::_thesis: verum
end;
end;
end;
hence  (h +* g) | D = (f +* g) | D by A2, A4, FUNCT_1:2; ::_thesis: verum
end;

theorem :: FUNCT_4:95
for f, g, h being Function
for D being set st f | D = h | D holds
(h +* g) | D = (f +* g) | D
proof
let f, g, h be Function; ::_thesis: for D being set st f | D = h | D holds
(h +* g) | D = (f +* g) | D
let D be set ; ::_thesis: ( f | D = h | D implies (h +* g) | D = (f +* g) | D )
assume A1: f | D = h | D ; ::_thesis: (h +* g) | D = (f +* g) | D
A2: dom ((f +* g) | D) = (dom (f +* g)) /\ D by RELAT_1:61
.= ((dom f) \/ (dom g)) /\ D by Def1 ;
A3: dom ((h +* g) | D) = (dom (h +* g)) /\ D by RELAT_1:61
.= ((dom h) \/ (dom g)) /\ D by Def1 ;
then A4: dom ((h +* g) | D) = ((dom h) /\ D) \/ ((dom g) /\ D) by XBOOLE_1:23
.= (dom (f | D)) \/ ((dom g) /\ D) by A1, RELAT_1:61
.= ((dom f) /\ D) \/ ((dom g) /\ D) by RELAT_1:61
.= ((dom f) \/ (dom g)) /\ D by XBOOLE_1:23 ;
now__::_thesis:_for_x_being_set_st_x_in_dom_((f_+*_g)_|_D)_holds_
((h_+*_g)_|_D)_._x_=_((f_+*_g)_|_D)_._x
let x be set ; ::_thesis: ( x in dom ((f +* g) | D) implies ((h +* g) | D) . b1 = ((f +* g) | D) . b1 )
assume A5: x in dom ((f +* g) | D) ; ::_thesis: ((h +* g) | D) . b1 = ((f +* g) | D) . b1
then A6: x in (dom f) \/ (dom g) by A2, XBOOLE_0:def_4;
A7: x in D by A2, A5, XBOOLE_0:def_4;
A8: ( x in (dom h) \/ (dom g) & ((h +* g) | D) . x = (h +* g) . x ) by A2, A3, A4, A5, FUNCT_1:47, XBOOLE_0:def_4;
percases ( x in dom g or not x in dom g ) ;
supposeA9: x in dom g ; ::_thesis: ((h +* g) | D) . b1 = ((f +* g) | D) . b1
((f +* g) | D) . x = (f +* g) . x by A5, FUNCT_1:47
.= g . x by A6, A9, Def1 ;
hence  ((h +* g) | D) . x = ((f +* g) | D) . x by A8, A9, Def1; ::_thesis: verum
end;
supposeA10: not x in dom g ; ::_thesis: ((f +* g) | D) . b1 = ((h +* g) | D) . b1
then A11: ((h +* g) | D) . x = h . x by A8, Def1
.= (h | D) . x by A7, FUNCT_1:49 ;
thus ((f +* g) | D) . x = (f +* g) . x by A5, FUNCT_1:47
.= f . x by A6, A10, Def1
.= ((h +* g) | D) . x by A1, A7, A11, FUNCT_1:49 ; ::_thesis: verum
end;
end;
end;
hence  (h +* g) | D = (f +* g) | D by A2, A4, FUNCT_1:2; ::_thesis: verum
end;

theorem Th96: :: FUNCT_4:96
for x being set holds x .--> x = id {x}
proof
let x be set ; ::_thesis: x .--> x = id {x}
 for y, z being set holds
( [y,z] in x .--> x iff ( y in {x} & y = z ) )
proof
let y, z be set ; ::_thesis: ( [y,z] in x .--> x iff ( y in {x} & y = z ) )
A1: x .--> x = {[x,x]} by ZFMISC_1:29;
thus  ( [y,z] in x .--> x implies ( y in {x} & y = z ) ) ::_thesis: ( y in {x} & y = z implies [y,z] in x .--> x )
proof
assume  [y,z] in x .--> x ; ::_thesis: ( y in {x} & y = z )
then A2: [y,z] = [x,x] by A1, TARSKI:def_1;
then  y = x by XTUPLE_0:1;
hence  ( y in {x} & y = z ) by A2, TARSKI:def_1, XTUPLE_0:1; ::_thesis: verum
end;
assume  y in {x} ; ::_thesis: ( not y = z or [y,z] in x .--> x )
then  y = x by TARSKI:def_1;
hence  ( not y = z or [y,z] in x .--> x ) by A1, TARSKI:def_1; ::_thesis: verum
end;
hence  x .--> x = id {x} by RELAT_1:def_10; ::_thesis: verum
end;

theorem Th97: :: FUNCT_4:97
for f, g being Function st f c= g holds
f +* g = g
proof
let f, g be Function; ::_thesis: ( f c= g implies f +* g = g )
assume A1: f c= g ; ::_thesis: f +* g = g
then  f tolerates g by PARTFUN1:54;
hence f +* g = f \/ g by Th30
.= g by A1, XBOOLE_1:12 ;
::_thesis: verum
end;

theorem Th98: :: FUNCT_4:98
for f, g being Function st f c= g holds
g +* f = g
proof
let f, g be Function; ::_thesis: ( f c= g implies g +* f = g )
assume A1: f c= g ; ::_thesis: g +* f = g
then  f tolerates g by PARTFUN1:54;
hence g +* f = f \/ g by Th30
.= g by A1, XBOOLE_1:12 ;
::_thesis: verum
end;

begin

definition
let f be Function;
let x, y be set ;
funcf +~ (x,y) ->  set  equals :: FUNCT_4:def 5
f +* ((x .--> y) * f);
coherence
 f +* ((x .--> y) * f) is set ;
end;

:: deftheorem  defines +~ FUNCT_4:def_5_:_
 for f being Function
for x, y being set holds f +~ (x,y) = f +* ((x .--> y) * f);

registration
let f be Function;
let x, y be set ;
clusterf +~ (x,y) ->  Relation-like Function-like ;
coherence
 ( f +~ (x,y) is Relation-like & f +~ (x,y) is Function-like ) ;
end;

theorem Th99: :: FUNCT_4:99
for f being Function
for x, y being set holds dom (f +~ (x,y)) = dom f
proof
let f be Function; ::_thesis: for x, y being set holds dom (f +~ (x,y)) = dom f
let x, y be set ; ::_thesis: dom (f +~ (x,y)) = dom f
thus  dom (f +~ (x,y)) = (dom f) \/ (dom ((x .--> y) * f)) by Def1
.= dom f by RELAT_1:25, XBOOLE_1:12 ; ::_thesis: verum
end;

theorem Th100: :: FUNCT_4:100
for f being Function
for x, y being set st x <> y holds
not x in rng (f +~ (x,y))
proof
let f be Function; ::_thesis: for x, y being set st x <> y holds
not x in rng (f +~ (x,y))
let x, y be set ; ::_thesis: ( x <> y implies not x in rng (f +~ (x,y)) )
assume A1: x <> y ; ::_thesis: not x in rng (f +~ (x,y))
assume  x in rng (f +~ (x,y)) ; ::_thesis: contradiction
then consider z being set  such that
A2: z in dom (f +~ (x,y)) and
A3: (f +~ (x,y)) . z = x by FUNCT_1:def_3;
A4: z in dom f by A2, Th99;
A5: now__::_thesis:_z_in_dom_((x_.-->_y)_*_f)
assume A6: not z in dom ((x .--> y) * f) ; ::_thesis: contradiction
then  f . z = x by A3, Th11;
then  f . z in dom (x .--> y) by FUNCOP_1:74;
hence  contradiction by A4, A6, FUNCT_1:11; ::_thesis: verum
end;
(x .--> y) . (f . z) = ((x .--> y) * f) . z by A4, FUNCT_1:13
.= x by A3, A5, Th13 ;
then  f . z <> x by A1, FUNCOP_1:72;
then  not f . z in dom (x .--> y) by FUNCOP_1:75;
hence  contradiction by A5, FUNCT_1:11; ::_thesis: verum
end;

theorem :: FUNCT_4:101
for f being Function
for x, y being set st x in rng f holds
y in rng (f +~ (x,y))
proof
let f be Function; ::_thesis: for x, y being set st x in rng f holds
y in rng (f +~ (x,y))
let x, y be set ; ::_thesis: ( x in rng f implies y in rng (f +~ (x,y)) )
assume  x in rng f ; ::_thesis: y in rng (f +~ (x,y))
then consider z being set  such that
A1: z in dom f and
A2: f . z = x by FUNCT_1:def_3;
A3: dom ((x .--> y) * f) c= dom (f +~ (x,y)) by Th10;
 x in dom (x .--> y) by FUNCOP_1:74;
then A4: z in dom ((x .--> y) * f) by A1, A2, FUNCT_1:11;
then (f +~ (x,y)) . z = ((x .--> y) * f) . z by Th13
.= (x .--> y) . (f . z) by A1, FUNCT_1:13
.= y by A2, FUNCOP_1:72 ;
hence  y in rng (f +~ (x,y)) by A4, A3, FUNCT_1:3; ::_thesis: verum
end;

theorem Th102: :: FUNCT_4:102
for f being Function
for x being set holds f +~ (x,x) = f
proof
let f be Function; ::_thesis: for x being set holds f +~ (x,x) = f
let x be set ; ::_thesis: f +~ (x,x) = f
thus f +~ (x,x) = f +* ((id {x}) * f) by Th96
.= f by Th98, RELAT_1:50 ; ::_thesis: verum
end;

theorem Th103: :: FUNCT_4:103
for f being Function
for x, y being set st not x in rng f holds
f +~ (x,y) = f
proof
let f be Function; ::_thesis: for x, y being set st not x in rng f holds
f +~ (x,y) = f
let x, y be set ; ::_thesis: ( not x in rng f implies f +~ (x,y) = f )
A1: dom (x .--> y) = {x} by FUNCOP_1:13;
assume  not x in rng f ; ::_thesis: f +~ (x,y) = f
then  dom (x .--> y) misses rng f by A1, ZFMISC_1:50;
then  (x .--> y) * f = {} by RELAT_1:44;
hence  f +~ (x,y) = f by Th21; ::_thesis: verum
end;

theorem :: FUNCT_4:104
for f being Function
for x, y being set holds rng (f +~ (x,y)) c= ((rng f) \ {x}) \/ {y}
proof
let f be Function; ::_thesis: for x, y being set holds rng (f +~ (x,y)) c= ((rng f) \ {x}) \/ {y}
let x, y be set ; ::_thesis: rng (f +~ (x,y)) c= ((rng f) \ {x}) \/ {y}
percases ( not x in rng f or ( x in rng f & x = y ) or x <> y ) ;
supposeA1: not x in rng f ; ::_thesis: rng (f +~ (x,y)) c= ((rng f) \ {x}) \/ {y}
then  f +~ (x,y) = f by Th103;
then  rng (f +~ (x,y)) = (rng f) \ {x} by A1, ZFMISC_1:57;
hence  rng (f +~ (x,y)) c= ((rng f) \ {x}) \/ {y} by XBOOLE_1:7; ::_thesis: verum
end;
supposethat A2: x in rng f and
A3: x = y ; ::_thesis: rng (f +~ (x,y)) c= ((rng f) \ {x}) \/ {y}
 f +~ (x,y) = f by A3, Th102;
hence  rng (f +~ (x,y)) c= ((rng f) \ {x}) \/ {y} by A2, A3, ZFMISC_1:116; ::_thesis: verum
end;
supposeA4: x <> y ; ::_thesis: rng (f +~ (x,y)) c= ((rng f) \ {x}) \/ {y}
 not x in rng (f +~ (x,y)) by A4, Th100;
then A5: (rng (f +~ (x,y))) \ {x} = rng (f +~ (x,y)) by ZFMISC_1:57;
 rng (x .--> y) = {y} by FUNCOP_1:8;
then A6: (rng f) \/ (rng ((x .--> y) * f)) c= (rng f) \/ {y} by RELAT_1:26, XBOOLE_1:9;
 rng (f +~ (x,y)) c= (rng f) \/ (rng ((x .--> y) * f)) by Th17;
then  rng (f +~ (x,y)) c= (rng f) \/ {y} by A6, XBOOLE_1:1;
then  rng (f +~ (x,y)) c= ((rng f) \/ {y}) \ {x} by A5, XBOOLE_1:33;
hence  rng (f +~ (x,y)) c= ((rng f) \ {x}) \/ {y} by A4, ZFMISC_1:123; ::_thesis: verum
end;
end;
end;

theorem :: FUNCT_4:105
for z being set
for f being Function
for x, y being set st f . z <> x holds
(f +~ (x,y)) . z = f . z
proof
let z be set ; ::_thesis: for f being Function
for x, y being set st f . z <> x holds
(f +~ (x,y)) . z = f . z
let f be Function; ::_thesis: for x, y being set st f . z <> x holds
(f +~ (x,y)) . z = f . z
let x, y be set ; ::_thesis: ( f . z <> x implies (f +~ (x,y)) . z = f . z )
assume  f . z <> x ; ::_thesis: (f +~ (x,y)) . z = f . z
then  not f . z in dom (x .--> y) by FUNCOP_1:75;
then  not z in dom ((x .--> y) * f) by FUNCT_1:11;
hence  (f +~ (x,y)) . z = f . z by Th11; ::_thesis: verum
end;

theorem :: FUNCT_4:106
for z being set
for f being Function
for x, y being set st z in dom f & f . z = x holds
(f +~ (x,y)) . z = y
proof
let z be set ; ::_thesis: for f being Function
for x, y being set st z in dom f & f . z = x holds
(f +~ (x,y)) . z = y
let f be Function; ::_thesis: for x, y being set st z in dom f & f . z = x holds
(f +~ (x,y)) . z = y
let x, y be set ; ::_thesis: ( z in dom f & f . z = x implies (f +~ (x,y)) . z = y )
assume that
A1: z in dom f and
A2: f . z = x ; ::_thesis: (f +~ (x,y)) . z = y
 f . z in dom (x .--> y) by A2, FUNCOP_1:74;
then A3: z in dom ((x .--> y) * f) by A1, FUNCT_1:11;
hence (f +~ (x,y)) . z = ((x .--> y) * f) . z by Th13
.= (x .--> y) . x by A2, A3, FUNCT_1:12
.= y by FUNCOP_1:72 ;
::_thesis: verum
end;

theorem :: FUNCT_4:107
for f being Function
for x, y being set st not x in dom f holds
f c= f +* (x .--> y)
proof
let f be Function; ::_thesis: for x, y being set st not x in dom f holds
f c= f +* (x .--> y)
let x, y be set ; ::_thesis: ( not x in dom f implies f c= f +* (x .--> y) )
assume  not x in dom f ; ::_thesis: f c= f +* (x .--> y)
then  dom f misses {x} by ZFMISC_1:50;
then  dom f misses dom (x .--> y) by FUNCOP_1:13;
hence  f c= f +* (x .--> y) by Th32; ::_thesis: verum
end;

theorem :: FUNCT_4:108
for X, Y being set
for f being PartFunc of X,Y
for x, y being set st x in X & y in Y holds
f +* (x .--> y) is PartFunc of X,Y
proof
let X, Y be set ; ::_thesis: for f being PartFunc of X,Y
for x, y being set st x in X & y in Y holds
f +* (x .--> y) is PartFunc of X,Y
let f be PartFunc of X,Y; ::_thesis: for x, y being set st x in X & y in Y holds
f +* (x .--> y) is PartFunc of X,Y
let x, y be set ; ::_thesis: ( x in X & y in Y implies f +* (x .--> y) is PartFunc of X,Y )
assume that
A1: x in X and
A2: y in Y ; ::_thesis: f +* (x .--> y) is PartFunc of X,Y
A3: {x} c= X by A1, ZFMISC_1:31;
 {y} c= Y by A2, ZFMISC_1:31;
then  rng (x .--> y) c= Y by FUNCOP_1:8;
then A4: (rng f) \/ (rng (x .--> y)) c= Y by XBOOLE_1:8;
 rng (f +* (x .--> y)) c= (rng f) \/ (rng (x .--> y)) by Th17;
then A5: rng (f +* (x .--> y)) c= Y by A4, XBOOLE_1:1;
dom (f +* (x .--> y)) = (dom f) \/ (dom (x .--> y)) by Def1
.= (dom f) \/ {x} by FUNCOP_1:13 ;
hence  f +* (x .--> y) is PartFunc of X,Y by A3, A5, RELSET_1:4, XBOOLE_1:8; ::_thesis: verum
end;

registration
let f be Function;
let g be non empty Function;
clusterf +* g ->  non empty ;
coherence
 not f +* g is empty
proof
 dom (f +* g) = (dom f) \/ (dom g) by Def1;
hence  not f +* g is empty ; ::_thesis: verum
end;
clusterg +* f ->  non empty ;
coherence
 not g +* f is empty
proof
 dom (g +* f) = (dom g) \/ (dom f) by Def1;
hence  not g +* f is empty ; ::_thesis: verum
end;
end;

registration
let f, g be non-empty Function;
clusterf +* g ->  non-empty ;
coherence
 f +* g is non-empty
proof
set h = f +* g;
A1: dom (f +* g) = (dom f) \/ (dom g) by Def1;
 not {} in rng (f +* g)
proof
assume  {} in rng (f +* g) ; ::_thesis: contradiction
then consider x being set  such that
A2: ( x in dom (f +* g) & {} = (f +* g) . x ) by FUNCT_1:def_3;
 ( not x in dom g or x in dom g ) ;
then  ( ( {} = f . x & x in dom f ) or ( {} = g . x & x in dom g ) ) by A1, A2, Def1, XBOOLE_0:def_3;
then  ( {} in rng f or {} in rng g ) by FUNCT_1:def_3;
hence  contradiction by RELAT_1:def_9; ::_thesis: verum
end;
hence  f +* g is non-empty by RELAT_1:def_9; ::_thesis: verum
end;
end;

definition
let X, Y be set ;
let f, g be PartFunc of X,Y;
:: original: +*
redefine funcf +* g ->  PartFunc of X,Y;
coherence
 f +* g is PartFunc of X,Y
proof
A1: dom (f +* g) c= (dom f) \/ (dom g) by Def1;
A2: dom (f +* g) c= X by A1, XBOOLE_1:1;
A3: rng (f +* g) c= (rng f) \/ (rng g) by Th17;
 rng (f +* g) c= Y by A3, XBOOLE_1:1;
then  f +* g is Relation of X,Y by A2, RELSET_1:4;
hence  f +* g is PartFunc of X,Y ; ::_thesis: verum
end;
end;

theorem :: FUNCT_4:109
for z, x, y being set holds dom ((x --> y) +* (x .--> z)) = succ x
proof
let z, x, y be set ; ::_thesis: dom ((x --> y) +* (x .--> z)) = succ x
thus  dom ((x --> y) +* (x .--> z)) = (dom (x --> y)) \/ (dom (x .--> z)) by Def1
.= x \/ (dom (x .--> z)) by FUNCOP_1:13
.= x \/ {x} by FUNCOP_1:13
.= succ x by ORDINAL1:def_1 ; ::_thesis: verum
end;

theorem :: FUNCT_4:110
for z, x, y being set holds dom (((x --> y) +* (x .--> z)) +* ((succ x) .--> z)) = succ (succ x)
proof
let z, x, y be set ; ::_thesis: dom (((x --> y) +* (x .--> z)) +* ((succ x) .--> z)) = succ (succ x)
thus  dom (((x --> y) +* (x .--> z)) +* ((succ x) .--> z)) = (dom ((x --> y) +* (x .--> z))) \/ (dom ((succ x) .--> z)) by Def1
.= ((dom (x --> y)) \/ (dom (x .--> z))) \/ (dom ((succ x) .--> z)) by Def1
.= (x \/ (dom (x .--> z))) \/ (dom ((succ x) .--> z)) by FUNCOP_1:13
.= (x \/ {x}) \/ (dom ((succ x) .--> z)) by FUNCOP_1:13
.= (x \/ {x}) \/ {(succ x)} by FUNCOP_1:13
.= (succ x) \/ {(succ x)} by ORDINAL1:def_1
.= succ (succ x) by ORDINAL1:def_1 ; ::_thesis: verum
end;

registration
let f, g be Function-yielding Function;
clusterf +* g ->  Function-yielding ;
coherence
 f +* g is Function-yielding
proof
let x be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not x in dom (f +* g) or (f +* g) . x is set )
assume  x in dom (f +* g) ; ::_thesis: (f +* g) . x is set
then A1: x in (dom f) \/ (dom g) by Def1;
percases ( x in dom g or ( x in dom f & not x in dom g ) ) by A1, XBOOLE_0:def_3;
suppose x in dom g ; ::_thesis: (f +* g) . x is set
then  (f +* g) . x = g . x by Th13;
hence  (f +* g) . x is Function ; ::_thesis: verum
end;
suppose ( x in dom f & not x in dom g ) ; ::_thesis: (f +* g) . x is set
then  (f +* g) . x = f . x by Th11;
hence  (f +* g) . x is Function ; ::_thesis: verum
end;
end;
end;
end;

registration
let I be set ;
let f, g be I -defined Function;
clusterf +* g -> I -defined ;
coherence
 f +* g is I -defined
proof
 dom (f +* g) = (dom f) \/ (dom g) by Def1;
then  dom (f +* g) c= I ;
hence  f +* g is I -defined by RELAT_1:def_18; ::_thesis: verum
end;
end;

registration
let I be set ;
let f be I -defined total Function;
let g be I -defined Function;
clusterf +* g -> I -defined total for I -defined Function;
coherence
 for b1 being I -defined Function st b1 = f +* g holds
b1 is total
proof
 dom f = I by PARTFUN1:def_2;
then  dom (f +* g) = I \/ (dom g) by Def1
.= I by XBOOLE_1:12 ;
hence  for b1 being I -defined Function st b1 = f +* g holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
clusterg +* f -> I -defined total for I -defined Function;
coherence
 for b1 being I -defined Function st b1 = g +* f holds
b1 is total
proof
 dom f = I by PARTFUN1:def_2;
then  dom (g +* f) = I \/ (dom g) by Def1
.= I by XBOOLE_1:12 ;
hence  for b1 being I -defined Function st b1 = g +* f holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;

registration
let I be set ;
let g, h be I -valued Function;
clusterg +* h -> I -valued ;
coherence
 g +* h is I -valued
proof
A1: rng (g +* h) c= (rng g) \/ (rng h) by Th17;
 rng (g +* h) c= I by A1, XBOOLE_1:1;
hence  g +* h is I -valued by RELAT_1:def_19; ::_thesis: verum
end;
end;

registration
let f be Function;
let g, h be f -compatible Function;
clusterg +* h -> f -compatible ;
coherence
 g +* h is f -compatible
proof
let x be set ; :: according to FUNCT_1:def_14 ::_thesis: ( not x in dom (g +* h) or (g +* h) . x in f . x )
assume A1: x in dom (g +* h) ; ::_thesis: (g +* h) . x in f . x
A2: dom (g +* h) = (dom g) \/ (dom h) by Def1;
percases ( ( x in dom g & not x in dom h ) or x in dom h ) by A1, A2, XBOOLE_0:def_3;
supposeA3: ( x in dom g & not x in dom h ) ; ::_thesis: (g +* h) . x in f . x
then  g . x in f . x by FUNCT_1:def_14;
hence  (g +* h) . x in f . x by A3, Th11; ::_thesis: verum
end;
supposeA4: x in dom h ; ::_thesis: (g +* h) . x in f . x
then  h . x in f . x by FUNCT_1:def_14;
hence  (g +* h) . x in f . x by A4, Th13; ::_thesis: verum
end;
end;
end;
end;

theorem :: FUNCT_4:111
for f being Function
for A being set holds (f | A) +* f = f by Th97, RELAT_1:59;

theorem :: FUNCT_4:112
for x, y being set
for R being Relation st dom R = {x} & rng R = {y} holds
R = x .--> y
proof
let x, y be set ; ::_thesis: for R being Relation st dom R = {x} & rng R = {y} holds
R = x .--> y
let R be Relation; ::_thesis: ( dom R = {x} & rng R = {y} implies R = x .--> y )
assume that
A1: dom R = {x} and
A2: rng R = {y} ; ::_thesis: R = x .--> y
set g = x .--> y;
A3: x .--> y = {[x,y]} by ZFMISC_1:29;
 for a, b being set holds
( [a,b] in R iff [a,b] in x .--> y )
proof
let a, b be set ; ::_thesis: ( [a,b] in R iff [a,b] in x .--> y )
hereby  ::_thesis: ( [a,b] in x .--> y implies [a,b] in R )
assume A4: [a,b] in R ; ::_thesis: [a,b] in x .--> y
then  b in rng R by XTUPLE_0:def_13;
then A5: b = y by A2, TARSKI:def_1;
 a in dom R by A4, XTUPLE_0:def_12;
then  a = x by A1, TARSKI:def_1;
hence  [a,b] in x .--> y by A3, A5, TARSKI:def_1; ::_thesis: verum
end;
assume  [a,b] in x .--> y ; ::_thesis: [a,b] in R
then A6: [a,b] = [x,y] by A3, TARSKI:def_1;
then A7: b = y by XTUPLE_0:1;
 a = x by A6, XTUPLE_0:1;
then  a in dom R by A1, TARSKI:def_1;
then consider z being set  such that
A8: [a,z] in R by XTUPLE_0:def_12;
 z in rng R by A8, XTUPLE_0:def_13;
hence  [a,b] in R by A2, A7, A8, TARSKI:def_1; ::_thesis: verum
end;
hence  R = x .--> y by RELAT_1:def_2; ::_thesis: verum
end;

theorem :: FUNCT_4:113
for f being Function
for x, y being set holds (f +* (x .--> y)) . x = y
proof
let f be Function; ::_thesis: for x, y being set holds (f +* (x .--> y)) . x = y
let x, y be set ; ::_thesis: (f +* (x .--> y)) . x = y
A1: x in {x} by TARSKI:def_1;
then  ( dom (x .--> y) = {x} & x in (dom f) \/ {x} ) by FUNCOP_1:13, XBOOLE_0:def_3;
hence (f +* (x .--> y)) . x = (x .--> y) . x by A1, Def1
.= y by FUNCOP_1:72 ;
::_thesis: verum
end;

theorem :: FUNCT_4:114
for z1, z2 being set
for f being Function
for x being set holds (f +* (x .--> z1)) +* (x .--> z2) = f +* (x .--> z2)
proof
let z1, z2 be set ; ::_thesis: for f being Function
for x being set holds (f +* (x .--> z1)) +* (x .--> z2) = f +* (x .--> z2)
let f be Function; ::_thesis: for x being set holds (f +* (x .--> z1)) +* (x .--> z2) = f +* (x .--> z2)
let x be set ; ::_thesis: (f +* (x .--> z1)) +* (x .--> z2) = f +* (x .--> z2)
A1: dom (x .--> z1) = {x} by FUNCOP_1:13
.= dom (x .--> z2) by FUNCOP_1:13 ;
thus (f +* (x .--> z1)) +* (x .--> z2) = f +* ((x .--> z1) +* (x .--> z2)) by Th14
.= f +* (x .--> z2) by A1, Th19 ; ::_thesis: verum
end;

registration
let A be non empty set ;
let a, b be Element of A;
let x, y be set ;
cluster(a,b) --> (x,y) -> A -defined ;
coherence
 (a,b) --> (x,y) is A -defined ;
end;

theorem :: FUNCT_4:115
for g, h, f being Function st dom g misses dom h holds
((f +* g) +* h) +* g = (f +* g) +* h
proof
let g, h, f be Function; ::_thesis: ( dom g misses dom h implies ((f +* g) +* h) +* g = (f +* g) +* h )
assume A1: dom g misses dom h ; ::_thesis: ((f +* g) +* h) +* g = (f +* g) +* h
thus ((f +* g) +* h) +* g = (f +* (g +* h)) +* g by Th14
.= f +* ((g +* h) +* g) by Th14
.= f +* ((h +* g) +* g) by A1, Th35
.= f +* (h +* g)
.= f +* (g +* h) by A1, Th35
.= (f +* g) +* h by Th14 ; ::_thesis: verum
end;

theorem :: FUNCT_4:116
for f, h, g being Function st dom f misses dom h & f c= g +* h holds
f c= g
proof
let f, h, g be Function; ::_thesis: ( dom f misses dom h & f c= g +* h implies f c= g )
assume that
A1: dom f misses dom h and
A2: f c= g +* h ; ::_thesis: f c= g
A3: (g +* h) | (dom f) = (g | (dom f)) +* (h | (dom f)) by Th71
.= (g | (dom f)) +* {} by A1, RELAT_1:66
.= g | (dom f) ;
 f | (dom f) = f ;
then  f c= g | (dom f) by A2, A3, RELAT_1:76;
hence  f c= g by RELAT_1:184; ::_thesis: verum
end;

theorem Th117: :: FUNCT_4:117
for f, h, g being Function st dom f misses dom h & f c= g holds
f c= g +* h
proof
let f, h, g be Function; ::_thesis: ( dom f misses dom h & f c= g implies f c= g +* h )
assume that
A1: dom f misses dom h and
A2: f c= g ; ::_thesis: f c= g +* h
A3: (g +* h) | (dom f) = (g | (dom f)) +* (h | (dom f)) by Th71
.= (g | (dom f)) +* {} by A1, RELAT_1:66
.= g | (dom f) ;
 f | (dom f) = f ;
then  f c= (g +* h) | (dom f) by A2, A3, RELAT_1:76;
hence  f c= g +* h by RELAT_1:184; ::_thesis: verum
end;

theorem :: FUNCT_4:118
for g, h, f being Function st dom g misses dom h holds
(f +* g) +* h = (f +* h) +* g
proof
let g, h, f be Function; ::_thesis: ( dom g misses dom h implies (f +* g) +* h = (f +* h) +* g )
assume A1: dom g misses dom h ; ::_thesis: (f +* g) +* h = (f +* h) +* g
thus (f +* g) +* h = f +* (g +* h) by Th14
.= f +* (h +* g) by A1, Th35
.= (f +* h) +* g by Th14 ; ::_thesis: verum
end;

theorem :: FUNCT_4:119
for f, g being Function st dom f misses dom g holds
(f +* g) \ g = f
proof
let f, g be Function; ::_thesis: ( dom f misses dom g implies (f +* g) \ g = f )
assume A1: dom f misses dom g ; ::_thesis: (f +* g) \ g = f
then A2: f misses g by RELAT_1:179;
thus (f +* g) \ g = (f \/ g) \ g by A1, Th31
.= f by A2, XBOOLE_1:88 ; ::_thesis: verum
end;

theorem :: FUNCT_4:120
for f, g being Function st dom f misses dom g holds
f \ g = f
proof
let f, g be Function; ::_thesis: ( dom f misses dom g implies f \ g = f )
assume  dom f misses dom g ; ::_thesis: f \ g = f
then  f misses g by RELAT_1:179;
hence  f \ g = f by XBOOLE_1:83; ::_thesis: verum
end;

theorem :: FUNCT_4:121
for g, h, f being Function st dom g misses dom h holds
(f \ g) +* h = (f +* h) \ g
proof
let g, h, f be Function; ::_thesis: ( dom g misses dom h implies (f \ g) +* h = (f +* h) \ g )
assume A1: dom g misses dom h ; ::_thesis: (f \ g) +* h = (f +* h) \ g
A2: dom (f +* h) = (dom f) \/ (dom h) by Def1;
A3: dom ((f \ g) +* h) = (dom (f \ g)) \/ (dom h) by Def1;
A4: dom ((f \ g) +* h) = dom ((f +* h) \ g)
proof
thus  dom ((f \ g) +* h) c= dom ((f +* h) \ g) :: according to XBOOLE_0:def_10 ::_thesis: dom ((f +* h) \ g) c= dom ((f \ g) +* h)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom ((f \ g) +* h) or x in dom ((f +* h) \ g) )
assume A5: x in dom ((f \ g) +* h) ; ::_thesis: x in dom ((f +* h) \ g)
percases ( ( x in dom (f \ g) & not x in dom h ) or x in dom h ) by A3, A5, XBOOLE_0:def_3;
supposethat A6: x in dom (f \ g) and
A7: not x in dom h ; ::_thesis: x in dom ((f +* h) \ g)
consider y being set  such that
A8: [x,y] in f \ g by A6, XTUPLE_0:def_12;
A9: x in dom f by A8, XTUPLE_0:def_12;
then A10: x in dom (f +* h) by A2, XBOOLE_0:def_3;
A11: not [x,y] in g by A8, XBOOLE_0:def_5;
A12: (f +* h) . x = f . x by A7, Th11;
 f . x = y by A8, A9, FUNCT_1:def_2;
then  [x,y] in f +* h by A12, A10, FUNCT_1:def_2;
then  [x,y] in (f +* h) \ g by A11, XBOOLE_0:def_5;
hence  x in dom ((f +* h) \ g) by XTUPLE_0:def_12; ::_thesis: verum
end;
supposeA13: x in dom h ; ::_thesis: x in dom ((f +* h) \ g)
then A14: not x in dom g by A1, XBOOLE_0:3;
 x in dom (f +* h) by A2, A13, XBOOLE_0:def_3;
then A15: x in (dom (f +* h)) \ (dom g) by A14, XBOOLE_0:def_5;
 (dom (f +* h)) \ (dom g) c= dom ((f +* h) \ g) by RELAT_1:3;
hence  x in dom ((f +* h) \ g) by A15; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom ((f +* h) \ g) or x in dom ((f \ g) +* h) )
assume  x in dom ((f +* h) \ g) ; ::_thesis: x in dom ((f \ g) +* h)
then consider y being set  such that
A16: [x,y] in (f +* h) \ g by XTUPLE_0:def_12;
A17: x in dom (f +* h) by A16, XTUPLE_0:def_12;
then A18: y = (f +* h) . x by A16, FUNCT_1:def_2;
percases ( ( x in dom f & not x in dom h ) or x in dom h ) by A2, A17, XBOOLE_0:def_3;
supposethat A19: x in dom f and
A20: not x in dom h ; ::_thesis: x in dom ((f \ g) +* h)
A21: not [x,y] in g by A16, XBOOLE_0:def_5;
 (f +* h) . x = f . x by A20, Th11;
then  [x,y] in f by A19, A18, FUNCT_1:def_2;
then  [x,y] in f \ g by A21, XBOOLE_0:def_5;
then  x in dom (f \ g) by XTUPLE_0:def_12;
hence  x in dom ((f \ g) +* h) by A3, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x in dom h ; ::_thesis: x in dom ((f \ g) +* h)
hence  x in dom ((f \ g) +* h) by A3, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
now__::_thesis:_for_x_being_set_st_x_in_dom_((f_\_g)_+*_h)_holds_
((f_\_g)_+*_h)_._x_=_((f_+*_h)_\_g)_._x
let x be set ; ::_thesis: ( x in dom ((f \ g) +* h) implies ((f \ g) +* h) . b1 = ((f +* h) \ g) . b1 )
assume A22: x in dom ((f \ g) +* h) ; ::_thesis: ((f \ g) +* h) . b1 = ((f +* h) \ g) . b1
percases ( ( x in dom (f \ g) & not x in dom h ) or x in dom h ) by A3, A22, XBOOLE_0:def_3;
supposethat A23: x in dom (f \ g) and
A24: not x in dom h ; ::_thesis: ((f \ g) +* h) . b1 = ((f +* h) \ g) . b1
thus ((f \ g) +* h) . x = (f \ g) . x by A24, Th11
.= f . x by A23, GRFUNC_1:2
.= (f +* h) . x by A24, Th11
.= ((f +* h) \ g) . x by A4, A22, GRFUNC_1:2 ; ::_thesis: verum
end;
supposeA25: x in dom h ; ::_thesis: ((f +* h) \ g) . b1 = ((f \ g) +* h) . b1
then A26: not x in dom g by A1, XBOOLE_0:3;
 x in dom (f +* h) by A25, A2, XBOOLE_0:def_3;
then  x in (dom (f +* h)) \ (dom g) by A26, XBOOLE_0:def_5;
hence ((f +* h) \ g) . x = (f +* h) . x by GRFUNC_1:32
.= h . x by A25, Th13
.= ((f \ g) +* h) . x by A25, Th13 ;
::_thesis: verum
end;
end;
end;
hence  (f \ g) +* h = (f +* h) \ g by A4, FUNCT_1:2; ::_thesis: verum
end;

theorem :: FUNCT_4:122
for f1, f2, g1, g2 being Function st f1 c= g1 & f2 c= g2 & dom f1 misses dom g2 holds
f1 +* f2 c= g1 +* g2
proof
let f1, f2, g1, g2 be Function; ::_thesis: ( f1 c= g1 & f2 c= g2 & dom f1 misses dom g2 implies f1 +* f2 c= g1 +* g2 )
assume that
A1: f1 c= g1 and
A2: f2 c= g2 and
A3: dom f1 misses dom g2 ; ::_thesis: f1 +* f2 c= g1 +* g2
A4: f1 c= g1 +* g2 by A1, A3, Th117;
 g2 c= g1 +* g2 by Th25;
then  f2 c= g1 +* g2 by A2, XBOOLE_1:1;
hence  f1 +* f2 c= g1 +* g2 by A4, Th87; ::_thesis: verum
end;

theorem Th123: :: FUNCT_4:123
for f, g, h being Function st f c= g holds
f +* h c= g +* h
proof
let f, g, h be Function; ::_thesis: ( f c= g implies f +* h c= g +* h )
assume A1: f c= g ; ::_thesis: f +* h c= g +* h
now__::_thesis:_(_dom_(f_+*_h)_c=_dom_(g_+*_h)_&_(_for_x_being_set_st_x_in_dom_(f_+*_h)_holds_
(f_+*_h)_._x_=_(g_+*_h)_._x_)_)
 ( dom (f +* h) = (dom f) \/ (dom h) & dom (g +* h) = (dom g) \/ (dom h) ) by Def1;
hence  dom (f +* h) c= dom (g +* h) by A1, RELAT_1:11, XBOOLE_1:9; ::_thesis: for x being set st x in dom (f +* h) holds
(f +* h) . b2 = (g +* h) . b2
let x be set ; ::_thesis: ( x in dom (f +* h) implies (f +* h) . b1 = (g +* h) . b1 )
assume  x in dom (f +* h) ; ::_thesis: (f +* h) . b1 = (g +* h) . b1
then A2: ( x in dom f or x in dom h ) by Th12;
percases ( x in dom h or not x in dom h ) ;
supposeA3: x in dom h ; ::_thesis: (f +* h) . b1 = (g +* h) . b1
hence (f +* h) . x = h . x by Th13
.= (g +* h) . x by A3, Th13 ;
::_thesis: verum
end;
supposeA4: not x in dom h ; ::_thesis: (f +* h) . b1 = (g +* h) . b1
then  ( (f +* h) . x = f . x & (g +* h) . x = g . x ) by Th11;
hence  (f +* h) . x = (g +* h) . x by A1, A2, A4, GRFUNC_1:2; ::_thesis: verum
end;
end;
end;
hence  f +* h c= g +* h by GRFUNC_1:2; ::_thesis: verum
end;

theorem :: FUNCT_4:124
for f, g, h being Function st f c= g & dom f misses dom h holds
f c= g +* h
proof
let f, g, h be Function; ::_thesis: ( f c= g & dom f misses dom h implies f c= g +* h )
assume  f c= g ; ::_thesis: ( not dom f misses dom h or f c= g +* h )
then A1: f +* h c= g +* h by Th123;
assume  dom f misses dom h ; ::_thesis: f c= g +* h
then  f c= f +* h by Th32;
hence  f c= g +* h by A1, XBOOLE_1:1; ::_thesis: verum
end;

registration
let x, y be set ;
clusterx .--> y ->  trivial ;
coherence
 x .--> y is trivial
proof
 x .--> y = {[x,y]} by ZFMISC_1:29;
hence  x .--> y is trivial ; ::_thesis: verum
end;
end;

theorem :: FUNCT_4:125
for f, g, h being Function st f tolerates g & g tolerates h & h tolerates f holds
f +* g tolerates h
proof
let f, g, h be Function; ::_thesis: ( f tolerates g & g tolerates h & h tolerates f implies f +* g tolerates h )
assume that
A1: f tolerates g and
A2: g tolerates h and
A3: h tolerates f ; ::_thesis: f +* g tolerates h
let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not x in (dom (f +* g)) /\ (dom h) or (f +* g) . x = h . x )
assume A4: x in (dom (f +* g)) /\ (dom h) ; ::_thesis: (f +* g) . x = h . x
then  x in dom (f +* g) by XBOOLE_0:def_4;
then A5: ( x in dom f or x in dom g ) by Th12;
 x in dom h by A4, XBOOLE_0:def_4;
then  ( ( x in (dom h) /\ (dom f) & (f +* g) . x = f . x ) or ( x in (dom g) /\ (dom h) & (f +* g) . x = g . x ) ) by A1, A5, Th13, Th15, XBOOLE_0:def_4;
hence  (f +* g) . x = h . x by A2, A3, PARTFUN1:def_4; ::_thesis: verum
end;