:: GRFUNC_1 semantic presentation

begin


theorem Th1: :: GRFUNC_1:1
for f being Function
for G being set st G c= f holds
G is Function ;

theorem Th2: :: GRFUNC_1:2
for f, g being Function holds
( f c= g iff ( dom f c= dom g & ( for x being set st x in dom f holds
f . x = g . x ) ) )
proof
let f, g be Function; ::_thesis: ( f c= g iff ( dom f c= dom g & ( for x being set st x in dom f holds
f . x = g . x ) ) )
thus  ( f c= g implies ( dom f c= dom g & ( for x being set st x in dom f holds
f . x = g . x ) ) ) ::_thesis: ( dom f c= dom g & ( for x being set st x in dom f holds
f . x = g . x ) implies f c= g )
proof
assume A1: f c= g ; ::_thesis: ( dom f c= dom g & ( for x being set st x in dom f holds
f . x = g . x ) )
hence  dom f c= dom g by RELAT_1:11; ::_thesis: for x being set st x in dom f holds
f . x = g . x
let x be set ; ::_thesis: ( x in dom f implies f . x = g . x )
assume  x in dom f ; ::_thesis: f . x = g . x
then  [x,(f . x)] in f by FUNCT_1:def_2;
hence  f . x = g . x by A1, FUNCT_1:1; ::_thesis: verum
end;
assume that
A2: dom f c= dom g and
A3: for x being set st x in dom f holds
f . x = g . x ; ::_thesis: f c= g
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [x,b1] in f or [x,b1] in g )
let y be set ; ::_thesis: ( not [x,y] in f or [x,y] in g )
assume A4: [x,y] in f ; ::_thesis: [x,y] in g
then A5: x in dom f by FUNCT_1:1;
 y = f . x by A4, FUNCT_1:1;
then  y = g . x by A3, A5;
hence  [x,y] in g by A2, A5, FUNCT_1:def_2; ::_thesis: verum
end;

theorem :: GRFUNC_1:3
for f, g being Function st dom f = dom g & f c= g holds
f = g
proof
let f, g be Function; ::_thesis: ( dom f = dom g & f c= g implies f = g )
assume that
A1: dom f = dom g and
A2: f c= g ; ::_thesis: f = g
 for x, y being set holds
( [x,y] in f iff [x,y] in g )
proof
let x, y be set ; ::_thesis: ( [x,y] in f iff [x,y] in g )
thus  ( [x,y] in f implies [x,y] in g ) by A2; ::_thesis: ( [x,y] in g implies [x,y] in f )
assume A3: [x,y] in g ; ::_thesis: [x,y] in f
then  x in dom f by A1, XTUPLE_0:def_12;
then  [x,(f . x)] in f by FUNCT_1:1;
hence  [x,y] in f by A2, A3, FUNCT_1:def_1; ::_thesis: verum
end;
hence  f = g by RELAT_1:def_2; ::_thesis: verum
end;

Lm1:  for x, y being set
for f, h being Function st (rng f) /\ (rng h) = {} & x in dom f & y in dom h holds
f . x <> h . y
proof
let x, y be set ; ::_thesis: for f, h being Function st (rng f) /\ (rng h) = {} & x in dom f & y in dom h holds
f . x <> h . y
let f, h be Function; ::_thesis: ( (rng f) /\ (rng h) = {} & x in dom f & y in dom h implies f . x <> h . y )
assume A1: (rng f) /\ (rng h) = {} ; ::_thesis: ( not x in dom f or not y in dom h or f . x <> h . y )
assume  ( x in dom f & y in dom h ) ; ::_thesis: f . x <> h . y
then  ( f . x in rng f & h . y in rng h ) by FUNCT_1:def_3;
hence  f . x <> h . y by A1, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem :: GRFUNC_1:4
for x, z being set
for g, f being Function st [x,z] in g * f holds
( [x,(f . x)] in f & [(f . x),z] in g )
proof
let x, z be set ; ::_thesis: for g, f being Function st [x,z] in g * f holds
( [x,(f . x)] in f & [(f . x),z] in g )
let g, f be Function; ::_thesis: ( [x,z] in g * f implies ( [x,(f . x)] in f & [(f . x),z] in g ) )
assume  [x,z] in g * f ; ::_thesis: ( [x,(f . x)] in f & [(f . x),z] in g )
then  ex y being set st
( [x,y] in f & [y,z] in g ) by RELAT_1:def_8;
hence  ( [x,(f . x)] in f & [(f . x),z] in g ) by FUNCT_1:1; ::_thesis: verum
end;

theorem :: GRFUNC_1:5
for x, y being set holds {[x,y]} is Function ;

Lm2:  for x, y, x1, y1 being set st [x,y] in {[x1,y1]} holds
( x = x1 & y = y1 )
proof
let x, y, x1, y1 be set ; ::_thesis: ( [x,y] in {[x1,y1]} implies ( x = x1 & y = y1 ) )
assume  [x,y] in {[x1,y1]} ; ::_thesis: ( x = x1 & y = y1 )
then  [x,y] = [x1,y1] by TARSKI:def_1;
hence  ( x = x1 & y = y1 ) by XTUPLE_0:1; ::_thesis: verum
end;

theorem :: GRFUNC_1:6
for x, y being set
for f being Function st f = {[x,y]} holds
f . x = y
proof
let x, y be set ; ::_thesis: for f being Function st f = {[x,y]} holds
f . x = y
let f be Function; ::_thesis: ( f = {[x,y]} implies f . x = y )
assume  f = {[x,y]} ; ::_thesis: f . x = y
then  [x,y] in f by TARSKI:def_1;
hence  f . x = y by FUNCT_1:1; ::_thesis: verum
end;

theorem Th7: :: GRFUNC_1:7
for x being set
for f being Function st dom f = {x} holds
f = {[x,(f . x)]}
proof
let x be set ; ::_thesis: for f being Function st dom f = {x} holds
f = {[x,(f . x)]}
let f be Function; ::_thesis: ( dom f = {x} implies f = {[x,(f . x)]} )
reconsider g = {[x,(f . x)]} as Function ;
assume A1: dom f = {x} ; ::_thesis: f = {[x,(f . x)]}
 for y, z being set holds
( [y,z] in f iff [y,z] in g )
proof
let y, z be set ; ::_thesis: ( [y,z] in f iff [y,z] in g )
thus  ( [y,z] in f implies [y,z] in g ) ::_thesis: ( [y,z] in g implies [y,z] in f )
proof
assume A2: [y,z] in f ; ::_thesis: [y,z] in g
then  y in {x} by A1, XTUPLE_0:def_12;
then A3: y = x by TARSKI:def_1;
A4: rng f = {(f . x)} by A1, FUNCT_1:4;
 z in rng f by A2, XTUPLE_0:def_13;
then  z = f . x by A4, TARSKI:def_1;
hence  [y,z] in g by A3, TARSKI:def_1; ::_thesis: verum
end;
assume  [y,z] in g ; ::_thesis: [y,z] in f
then A5: ( y = x & z = f . x ) by Lm2;
 x in dom f by A1, TARSKI:def_1;
hence  [y,z] in f by A5, FUNCT_1:def_2; ::_thesis: verum
end;
hence  f = {[x,(f . x)]} by RELAT_1:def_2; ::_thesis: verum
end;

theorem :: GRFUNC_1:8
for x1, y1, x2, y2 being set holds
( {[x1,y1],[x2,y2]} is Function iff ( x1 = x2 implies y1 = y2 ) )
proof
let x1, y1, x2, y2 be set ; ::_thesis: ( {[x1,y1],[x2,y2]} is Function iff ( x1 = x2 implies y1 = y2 ) )
thus  ( {[x1,y1],[x2,y2]} is Function & x1 = x2 implies y1 = y2 ) ::_thesis: ( ( x1 = x2 implies y1 = y2 ) implies {[x1,y1],[x2,y2]} is Function )
proof
A1: ( [x1,y1] in {[x1,y1],[x2,y2]} & [x2,y2] in {[x1,y1],[x2,y2]} ) by TARSKI:def_2;
assume  {[x1,y1],[x2,y2]} is Function ; ::_thesis: ( not x1 = x2 or y1 = y2 )
hence  ( not x1 = x2 or y1 = y2 ) by A1, FUNCT_1:def_1; ::_thesis: verum
end;
assume A2: ( x1 = x2 implies y1 = y2 ) ; ::_thesis: {[x1,y1],[x2,y2]} is Function
now__::_thesis:_(_(_for_p_being_set_st_p_in_{[x1,y1],[x2,y2]}_holds_
ex_x,_y_being_set_st_[x,y]_=_p_)_&_(_for_x,_z1,_z2_being_set_st_[x,z1]_in_{[x1,y1],[x2,y2]}_&_[x,z2]_in_{[x1,y1],[x2,y2]}_holds_
z1_=_z2_)_)
thus  for p being set st p in {[x1,y1],[x2,y2]} holds
ex x, y being set st [x,y] = p ::_thesis: for x, z1, z2 being set st [x,z1] in {[x1,y1],[x2,y2]} & [x,z2] in {[x1,y1],[x2,y2]} holds
z1 = z2
proof
let p be set ; ::_thesis: ( p in {[x1,y1],[x2,y2]} implies ex x, y being set st [x,y] = p )
assume  p in {[x1,y1],[x2,y2]} ; ::_thesis: ex x, y being set st [x,y] = p
then  ( p = [x1,y1] or p = [x2,y2] ) by TARSKI:def_2;
hence  ex x, y being set st [x,y] = p ; ::_thesis: verum
end;
let x, z1, z2 be set ; ::_thesis: ( [x,z1] in {[x1,y1],[x2,y2]} & [x,z2] in {[x1,y1],[x2,y2]} implies z1 = z2 )
A3: ( ( not ( [x,z1] = [x1,y1] & [x,z2] = [x1,y1] ) & not ( [x,z1] = [x2,y2] & [x,z2] = [x2,y2] ) ) or ( z1 = y1 & z2 = y1 ) or ( z1 = y2 & z2 = y2 ) ) by XTUPLE_0:1;
A4: now__::_thesis:_(_(_(_[x,z1]_=_[x1,y1]_&_[x,z2]_=_[x2,y2]_)_or_(_[x,z1]_=_[x2,y2]_&_[x,z2]_=_[x1,y1]_)_)_implies_z1_=_z2_)
assume A5: ( ( [x,z1] = [x1,y1] & [x,z2] = [x2,y2] ) or ( [x,z1] = [x2,y2] & [x,z2] = [x1,y1] ) ) ; ::_thesis: z1 = z2
then  ( x = x1 & x = x2 ) by XTUPLE_0:1;
hence  z1 = z2 by A2, A5, XTUPLE_0:1; ::_thesis: verum
end;
assume  ( [x,z1] in {[x1,y1],[x2,y2]} & [x,z2] in {[x1,y1],[x2,y2]} ) ; ::_thesis: z1 = z2
hence  z1 = z2 by A3, A4, TARSKI:def_2; ::_thesis: verum
end;
hence  {[x1,y1],[x2,y2]} is Function by FUNCT_1:def_1; ::_thesis: verum
end;

theorem Th9: :: GRFUNC_1:9
for f being Function holds
( f is one-to-one iff for x1, x2, y being set st [x1,y] in f & [x2,y] in f holds
x1 = x2 )
proof
let f be Function; ::_thesis: ( f is one-to-one iff for x1, x2, y being set st [x1,y] in f & [x2,y] in f holds
x1 = x2 )
thus  ( f is one-to-one implies for x1, x2, y being set st [x1,y] in f & [x2,y] in f holds
x1 = x2 ) ::_thesis: ( ( for x1, x2, y being set st [x1,y] in f & [x2,y] in f holds
x1 = x2 ) implies f is one-to-one )
proof
assume A1: f is one-to-one ; ::_thesis: for x1, x2, y being set st [x1,y] in f & [x2,y] in f holds
x1 = x2
let x1, x2, y be set ; ::_thesis: ( [x1,y] in f & [x2,y] in f implies x1 = x2 )
assume A2: ( [x1,y] in f & [x2,y] in f ) ; ::_thesis: x1 = x2
then A3: ( f . x1 = y & f . x2 = y ) by FUNCT_1:1;
 ( x1 in dom f & x2 in dom f ) by A2, FUNCT_1:1;
hence  x1 = x2 by A1, A3, FUNCT_1:def_4; ::_thesis: verum
end;
assume A4: for x1, x2, y being set st [x1,y] in f & [x2,y] in f holds
x1 = x2 ; ::_thesis: f is one-to-one
let x1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x1 in proj1 f or not b1 in proj1 f or not f . x1 = f . b1 or x1 = b1 )
let x2 be set ; ::_thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume  ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; ::_thesis: x1 = x2
then  ( [x1,(f . x1)] in f & [x2,(f . x1)] in f ) by FUNCT_1:1;
hence  x1 = x2 by A4; ::_thesis: verum
end;

theorem Th10: :: GRFUNC_1:10
for g, f being Function st g c= f & f is one-to-one holds
g is one-to-one
proof
let g, f be Function; ::_thesis: ( g c= f & f is one-to-one implies g is one-to-one )
assume  ( g c= f & f is one-to-one ) ; ::_thesis: g is one-to-one
then  for x1, x2, y being set st [x1,y] in g & [x2,y] in g holds
x1 = x2 by Th9;
hence  g is one-to-one by Th9; ::_thesis: verum
end;

registration
let f be Function;
let X be set ;
clusterf /\ X ->  Function-like ;
coherence
 f /\ X is Function-like by Th1, XBOOLE_1:17;
end;

theorem :: GRFUNC_1:11
for x being set
for f, g being Function st x in dom (f /\ g) holds
(f /\ g) . x = f . x
proof
let x be set ; ::_thesis: for f, g being Function st x in dom (f /\ g) holds
(f /\ g) . x = f . x
let f, g be Function; ::_thesis: ( x in dom (f /\ g) implies (f /\ g) . x = f . x )
set y = (f /\ g) . x;
assume  x in dom (f /\ g) ; ::_thesis: (f /\ g) . x = f . x
then  [x,((f /\ g) . x)] in f /\ g by FUNCT_1:def_2;
then  [x,((f /\ g) . x)] in f by XBOOLE_0:def_4;
hence  (f /\ g) . x = f . x by FUNCT_1:1; ::_thesis: verum
end;

theorem :: GRFUNC_1:12
for f, g being Function st f is one-to-one holds
f /\ g is one-to-one by Th10, XBOOLE_1:17;

theorem :: GRFUNC_1:13
for f, g being Function st dom f misses dom g holds
f \/ g is Function
proof
let f, g be Function; ::_thesis: ( dom f misses dom g implies f \/ g is Function )
assume A1: (dom f) /\ (dom g) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: f \/ g is Function
now__::_thesis:_(_(_for_p_being_set_st_p_in_f_\/_g_holds_
ex_x,_y_being_set_st_[x,y]_=_p_)_&_(_for_x,_y1,_y2_being_set_st_[x,y1]_in_f_\/_g_&_[x,y2]_in_f_\/_g_holds_
y1_=_y2_)_)
thus  for p being set st p in f \/ g holds
ex x, y being set st [x,y] = p by RELAT_1:def_1; ::_thesis: for x, y1, y2 being set st [x,y1] in f \/ g & [x,y2] in f \/ g holds
y1 = y2
let x, y1, y2 be set ; ::_thesis: ( [x,y1] in f \/ g & [x,y2] in f \/ g implies y1 = y2 )
assume  [x,y1] in f \/ g ; ::_thesis: ( [x,y2] in f \/ g implies y1 = y2 )
then A2: ( [x,y1] in f or [x,y1] in g ) by XBOOLE_0:def_3;
assume  [x,y2] in f \/ g ; ::_thesis: y1 = y2
then A3: ( [x,y2] in f or [x,y2] in g ) by XBOOLE_0:def_3;
 ( not x in dom f or not x in dom g ) by A1, XBOOLE_0:def_4;
hence  y1 = y2 by A2, A3, FUNCT_1:def_1, XTUPLE_0:def_12; ::_thesis: verum
end;
hence  f \/ g is Function by FUNCT_1:def_1; ::_thesis: verum
end;

theorem :: GRFUNC_1:14
for f, h, g being Function st f c= h & g c= h holds
f \/ g is Function by Th1, XBOOLE_1:8;

Lm3:  for x being set
for h, f, g being Function st h = f \/ g holds
( x in dom h iff ( x in dom f or x in dom g ) )
proof
let x be set ; ::_thesis: for h, f, g being Function st h = f \/ g holds
( x in dom h iff ( x in dom f or x in dom g ) )
let h, f, g be Function; ::_thesis: ( h = f \/ g implies ( x in dom h iff ( x in dom f or x in dom g ) ) )
assume A1: h = f \/ g ; ::_thesis: ( x in dom h iff ( x in dom f or x in dom g ) )
thus  ( not x in dom h or x in dom f or x in dom g ) ::_thesis: ( ( x in dom f or x in dom g ) implies x in dom h )
proof
assume  x in dom h ; ::_thesis: ( x in dom f or x in dom g )
then  [x,(h . x)] in h by FUNCT_1:def_2;
then  ( [x,(h . x)] in f or [x,(h . x)] in g ) by A1, XBOOLE_0:def_3;
hence  ( x in dom f or x in dom g ) by XTUPLE_0:def_12; ::_thesis: verum
end;
assume  ( x in dom f or x in dom g ) ; ::_thesis: x in dom h
then  ( [x,(f . x)] in f or [x,(g . x)] in g ) by FUNCT_1:def_2;
then  ( [x,(f . x)] in h or [x,(g . x)] in h ) by A1, XBOOLE_0:def_3;
hence  x in dom h by XTUPLE_0:def_12; ::_thesis: verum
end;

theorem Th15: :: GRFUNC_1:15
for x being set
for g, h, f being Function st x in dom g & h = f \/ g holds
h . x = g . x
proof
let x be set ; ::_thesis: for g, h, f being Function st x in dom g & h = f \/ g holds
h . x = g . x
let g, h, f be Function; ::_thesis: ( x in dom g & h = f \/ g implies h . x = g . x )
assume  x in dom g ; ::_thesis: ( not h = f \/ g or h . x = g . x )
then  [x,(g . x)] in g by FUNCT_1:def_2;
then  ( h = f \/ g implies [x,(g . x)] in h ) by XBOOLE_0:def_3;
hence  ( not h = f \/ g or h . x = g . x ) by FUNCT_1:1; ::_thesis: verum
end;

theorem :: GRFUNC_1:16
for x being set
for h, f, g being Function st x in dom h & h = f \/ g & not h . x = f . x holds
h . x = g . x
proof
let x be set ; ::_thesis: for h, f, g being Function st x in dom h & h = f \/ g & not h . x = f . x holds
h . x = g . x
let h, f, g be Function; ::_thesis: ( x in dom h & h = f \/ g & not h . x = f . x implies h . x = g . x )
assume  x in dom h ; ::_thesis: ( not h = f \/ g or h . x = f . x or h . x = g . x )
then  [x,(h . x)] in h by FUNCT_1:def_2;
then  ( not h = f \/ g or [x,(h . x)] in f or [x,(h . x)] in g ) by XBOOLE_0:def_3;
hence  ( not h = f \/ g or h . x = f . x or h . x = g . x ) by FUNCT_1:1; ::_thesis: verum
end;

theorem :: GRFUNC_1:17
for f, g, h being Function st f is one-to-one & g is one-to-one & h = f \/ g & rng f misses rng g holds
h is one-to-one
proof
let f, g, h be Function; ::_thesis: ( f is one-to-one & g is one-to-one & h = f \/ g & rng f misses rng g implies h is one-to-one )
assume that
A1: ( f is one-to-one & g is one-to-one ) and
A2: h = f \/ g and
A3: (rng f) /\ (rng g) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: h is one-to-one
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_h_&_x2_in_dom_h_&_h_._x1_=_h_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom h & x2 in dom h & h . x1 = h . x2 implies x1 = x2 )
assume that
A4: ( x1 in dom h & x2 in dom h ) and
A5: h . x1 = h . x2 ; ::_thesis: x1 = x2
A6: now__::_thesis:_(_(_(_x1_in_dom_f_&_x2_in_dom_g_)_or_(_x1_in_dom_g_&_x2_in_dom_f_)_)_implies_x1_=_x2_)
assume  ( ( x1 in dom f & x2 in dom g ) or ( x1 in dom g & x2 in dom f ) ) ; ::_thesis: x1 = x2
then  ( ( h . x1 = f . x1 & h . x2 = g . x2 & f . x1 <> g . x2 ) or ( h . x1 = g . x1 & h . x2 = f . x2 & f . x2 <> g . x1 ) ) by A2, A3, Lm1, Th15;
hence  x1 = x2 by A5; ::_thesis: verum
end;
A7: ( x1 in dom g & x2 in dom g implies ( h . x1 = g . x1 & h . x2 = g . x2 ) ) by A2, Th15;
 ( x1 in dom f & x2 in dom f implies ( h . x1 = f . x1 & h . x2 = f . x2 ) ) by A2, Th15;
then  ( ( ( x1 in dom f & x2 in dom f ) or ( x1 in dom g & x2 in dom g ) ) implies x1 = x2 ) by A1, A5, A7, FUNCT_1:def_4;
hence  x1 = x2 by A2, A4, A6, Lm3; ::_thesis: verum
end;
hence  h is one-to-one by FUNCT_1:def_4; ::_thesis: verum
end;

theorem :: GRFUNC_1:18
canceled;

theorem :: GRFUNC_1:19
canceled;

theorem :: GRFUNC_1:20
for f being Function st f is one-to-one holds
for x, y being set holds
( [y,x] in f " iff [x,y] in f )
proof
let f be Function; ::_thesis: ( f is one-to-one implies for x, y being set holds
( [y,x] in f " iff [x,y] in f ) )
assume A1: f is one-to-one ; ::_thesis: for x, y being set holds
( [y,x] in f " iff [x,y] in f )
let x, y be set ; ::_thesis: ( [y,x] in f " iff [x,y] in f )
 dom (f ") = rng f by A1, FUNCT_1:33;
then  ( y in dom (f ") & x = (f ") . y iff ( x in dom f & y = f . x ) ) by A1, FUNCT_1:32;
hence  ( [y,x] in f " iff [x,y] in f ) by FUNCT_1:1; ::_thesis: verum
end;

theorem :: GRFUNC_1:21
for f being Function st f = {} holds
f " = {}
proof
let f be Function; ::_thesis: ( f = {} implies f " = {} )
assume  f = {} ; ::_thesis: f " = {}
then  dom (f ") = {} by FUNCT_1:33, RELAT_1:38;
hence  f " = {} ; ::_thesis: verum
end;

theorem :: GRFUNC_1:22
for x, X being set
for f being Function holds
( ( x in dom f & x in X ) iff [x,(f . x)] in f | X )
proof
let x, X be set ; ::_thesis: for f being Function holds
( ( x in dom f & x in X ) iff [x,(f . x)] in f | X )
let f be Function; ::_thesis: ( ( x in dom f & x in X ) iff [x,(f . x)] in f | X )
 ( x in dom f iff [x,(f . x)] in f ) by FUNCT_1:def_2, XTUPLE_0:def_12;
hence  ( ( x in dom f & x in X ) iff [x,(f . x)] in f | X ) by RELAT_1:def_11; ::_thesis: verum
end;

theorem Th23: :: GRFUNC_1:23
for g, f being Function st g c= f holds
f | (dom g) = g
proof
let g, f be Function; ::_thesis: ( g c= f implies f | (dom g) = g )
assume A1: g c= f ; ::_thesis: f | (dom g) = g
 for x, y being set st [x,y] in f | (dom g) holds
[x,y] in g
proof
let x, y be set ; ::_thesis: ( [x,y] in f | (dom g) implies [x,y] in g )
assume A2: [x,y] in f | (dom g) ; ::_thesis: [x,y] in g
then  x in dom g by RELAT_1:def_11;
then A3: [x,(g . x)] in g by FUNCT_1:def_2;
 [x,y] in f by A2, RELAT_1:def_11;
hence  [x,y] in g by A1, A3, FUNCT_1:def_1; ::_thesis: verum
end;
then A4: f | (dom g) c= g by RELAT_1:def_3;
 g | (dom g) c= f | (dom g) by A1, RELAT_1:76;
then  g c= f | (dom g) ;
hence  f | (dom g) = g by A4, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: GRFUNC_1:24
for x, Y being set
for f being Function holds
( ( x in dom f & f . x in Y ) iff [x,(f . x)] in Y |` f )
proof
let x, Y be set ; ::_thesis: for f being Function holds
( ( x in dom f & f . x in Y ) iff [x,(f . x)] in Y |` f )
let f be Function; ::_thesis: ( ( x in dom f & f . x in Y ) iff [x,(f . x)] in Y |` f )
 ( x in dom f iff [x,(f . x)] in f ) by FUNCT_1:def_2, XTUPLE_0:def_12;
hence  ( ( x in dom f & f . x in Y ) iff [x,(f . x)] in Y |` f ) by RELAT_1:def_12; ::_thesis: verum
end;

theorem :: GRFUNC_1:25
for g, f being Function st g c= f & f is one-to-one holds
(rng g) |` f = g
proof
let g, f be Function; ::_thesis: ( g c= f & f is one-to-one implies (rng g) |` f = g )
assume A1: g c= f ; ::_thesis: ( not f is one-to-one or (rng g) |` f = g )
assume A2: f is one-to-one ; ::_thesis: (rng g) |` f = g
 for x, y being set st [x,y] in (rng g) |` f holds
[x,y] in g
proof
let x, y be set ; ::_thesis: ( [x,y] in (rng g) |` f implies [x,y] in g )
assume A3: [x,y] in (rng g) |` f ; ::_thesis: [x,y] in g
then  y in rng g by RELAT_1:def_12;
then A4: ex x1 being set st [x1,y] in g by XTUPLE_0:def_13;
 [x,y] in f by A3, RELAT_1:def_12;
hence  [x,y] in g by A1, A2, A4, Th9; ::_thesis: verum
end;
then A5: (rng g) |` f c= g by RELAT_1:def_3;
 (rng g) |` g c= (rng g) |` f by A1, RELAT_1:101;
then  g c= (rng g) |` f ;
hence  (rng g) |` f = g by A5, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: GRFUNC_1:26
for x, Y being set
for f being Function holds
( x in f " Y iff ( [x,(f . x)] in f & f . x in Y ) )
proof
let x, Y be set ; ::_thesis: for f being Function holds
( x in f " Y iff ( [x,(f . x)] in f & f . x in Y ) )
let f be Function; ::_thesis: ( x in f " Y iff ( [x,(f . x)] in f & f . x in Y ) )
thus  ( x in f " Y implies ( [x,(f . x)] in f & f . x in Y ) ) ::_thesis: ( [x,(f . x)] in f & f . x in Y implies x in f " Y )
proof
assume  x in f " Y ; ::_thesis: ( [x,(f . x)] in f & f . x in Y )
then  ex y being set st
( [x,y] in f & y in Y ) by RELAT_1:def_14;
hence  ( [x,(f . x)] in f & f . x in Y ) by FUNCT_1:1; ::_thesis: verum
end;
thus  ( [x,(f . x)] in f & f . x in Y implies x in f " Y ) by RELAT_1:def_14; ::_thesis: verum
end;

begin

theorem :: GRFUNC_1:27
for X being set
for f, g being Function st X c= dom f & f c= g holds
f | X = g | X
proof
let X be set ; ::_thesis: for f, g being Function st X c= dom f & f c= g holds
f | X = g | X
let f, g be Function; ::_thesis: ( X c= dom f & f c= g implies f | X = g | X )
assume A1: X c= dom f ; ::_thesis: ( not f c= g or f | X = g | X )
assume  f c= g ; ::_thesis: f | X = g | X
hence f | X = (g | (dom f)) | X by Th23
.= g | ((dom f) /\ X) by RELAT_1:71
.= g | X by A1, XBOOLE_1:28 ;
::_thesis: verum
end;

theorem Th28: :: GRFUNC_1:28
for f being Function
for x being set st x in dom f holds
f | {x} = {[x,(f . x)]}
proof
let f be Function; ::_thesis: for x being set st x in dom f holds
f | {x} = {[x,(f . x)]}
let x be set ; ::_thesis: ( x in dom f implies f | {x} = {[x,(f . x)]} )
assume A1: x in dom f ; ::_thesis: f | {x} = {[x,(f . x)]}
A2: x in {x} by TARSKI:def_1;
dom (f | {x}) = (dom f) /\ {x} by RELAT_1:61
.= {x} by A1, ZFMISC_1:46 ;
hence f | {x} = {[x,((f | {x}) . x)]} by Th7
.= {[x,(f . x)]} by A2, FUNCT_1:49 ;
::_thesis: verum
end;

theorem Th29: :: GRFUNC_1:29
for f, g being Function
for x being set st dom f = dom g & f . x = g . x holds
f | {x} = g | {x}
proof
let f, g be Function; ::_thesis: for x being set st dom f = dom g & f . x = g . x holds
f | {x} = g | {x}
let x be set ; ::_thesis: ( dom f = dom g & f . x = g . x implies f | {x} = g | {x} )
assume that
A1: dom f = dom g and
A2: f . x = g . x ; ::_thesis: f | {x} = g | {x}
percases ( x in dom f or not x in dom f ) ;
supposeA3: x in dom f ; ::_thesis: f | {x} = g | {x}
hence f | {x} = {[x,(g . x)]} by A2, Th28
.= g | {x} by A1, A3, Th28 ;
::_thesis: verum
end;
suppose not x in dom f ; ::_thesis: f | {x} = g | {x}
then A4: {x} misses dom f by ZFMISC_1:50;
hence f | {x} = {} by RELAT_1:66
.= g | {x} by A1, A4, RELAT_1:66 ;
::_thesis: verum
end;
end;
end;

theorem Th30: :: GRFUNC_1:30
for f, g being Function
for x, y being set st dom f = dom g & f . x = g . x & f . y = g . y holds
f | {x,y} = g | {x,y}
proof
let f, g be Function; ::_thesis: for x, y being set st dom f = dom g & f . x = g . x & f . y = g . y holds
f | {x,y} = g | {x,y}
let x, y be set ; ::_thesis: ( dom f = dom g & f . x = g . x & f . y = g . y implies f | {x,y} = g | {x,y} )
assume  ( dom f = dom g & f . x = g . x & f . y = g . y ) ; ::_thesis: f | {x,y} = g | {x,y}
then A1: ( f | {x} = g | {x} & f | {y} = g | {y} ) by Th29;
 {x,y} = {x} \/ {y} by ENUMSET1:1;
hence  f | {x,y} = g | {x,y} by A1, RELAT_1:150; ::_thesis: verum
end;

theorem :: GRFUNC_1:31
for f, g being Function
for x, y, z being set st dom f = dom g & f . x = g . x & f . y = g . y & f . z = g . z holds
f | {x,y,z} = g | {x,y,z}
proof
let f, g be Function; ::_thesis: for x, y, z being set st dom f = dom g & f . x = g . x & f . y = g . y & f . z = g . z holds
f | {x,y,z} = g | {x,y,z}
let x, y, z be set ; ::_thesis: ( dom f = dom g & f . x = g . x & f . y = g . y & f . z = g . z implies f | {x,y,z} = g | {x,y,z} )
assume  ( dom f = dom g & f . x = g . x & f . y = g . y & f . z = g . z ) ; ::_thesis: f | {x,y,z} = g | {x,y,z}
then A1: ( f | {x,y} = g | {x,y} & f | {z} = g | {z} ) by Th29, Th30;
 {x,y,z} = {x,y} \/ {z} by ENUMSET1:3;
hence  f | {x,y,z} = g | {x,y,z} by A1, RELAT_1:150; ::_thesis: verum
end;

registration
let f be Function;
let A be set ;
clusterf \ A ->  Function-like ;
coherence
 f \ A is Function-like ;
end;

theorem :: GRFUNC_1:32
for x being set
for f, g being Function st x in (dom f) \ (dom g) holds
(f \ g) . x = f . x
proof
let x be set ; ::_thesis: for f, g being Function st x in (dom f) \ (dom g) holds
(f \ g) . x = f . x
let f, g be Function; ::_thesis: ( x in (dom f) \ (dom g) implies (f \ g) . x = f . x )
assume A1: x in (dom f) \ (dom g) ; ::_thesis: (f \ g) . x = f . x
 ( f \ g c= f & (dom f) \ (dom g) c= dom (f \ g) ) by RELAT_1:3;
hence  (f \ g) . x = f . x by A1, Th2; ::_thesis: verum
end;

theorem :: GRFUNC_1:33
for f, g, h being Function st f c= g & f c= h holds
g | (dom f) = h | (dom f)
proof
let f, g, h be Function; ::_thesis: ( f c= g & f c= h implies g | (dom f) = h | (dom f) )
assume that
A1: f c= g and
A2: f c= h ; ::_thesis: g | (dom f) = h | (dom f)
thus g | (dom f) = f by A1, Th23
.= h | (dom f) by A2, Th23 ; ::_thesis: verum
end;

registration
let f be Function;
let g be Subset of f;
cluster Relation-like Function-like g -compatible  -> f -compatible for set ;
coherence
 for b1 being Function st b1 is g -compatible holds
b1 is f -compatible
proof
let F be Function; ::_thesis: ( F is g -compatible implies F is f -compatible )
assume A1: F is g -compatible ; ::_thesis: F is f -compatible
let x be set ; :: according to FUNCT_1:def_14 ::_thesis: ( not x in proj1 F or F . x in f . x )
assume  x in dom F ; ::_thesis: F . x in f . x
then A2: F . x in g . x by A1, FUNCT_1:def_14;
then  x in dom g by FUNCT_1:def_2;
hence  F . x in f . x by A2, Th2; ::_thesis: verum
end;
end;

theorem Th34: :: GRFUNC_1:34
for g, f being Function st g c= f holds
g = f | (dom g)
proof
let g, f be Function; ::_thesis: ( g c= f implies g = f | (dom g) )
assume A1: g c= f ; ::_thesis: g = f | (dom g)
then  dom g c= dom f by RELAT_1:11;
hence  dom g = dom (f | (dom g)) by RELAT_1:62; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds
( not b1 in proj1 g or g . b1 = (f | (dom g)) . b1 )
let x be set ; ::_thesis: ( not x in proj1 g or g . x = (f | (dom g)) . x )
assume A2: x in dom g ; ::_thesis: g . x = (f | (dom g)) . x
hence g . x = f . x by A1, Th2
.= (f | (dom g)) . x by A2, FUNCT_1:49 ;
::_thesis: verum
end;

registration
let f be Function;
let g be f -compatible Function;
cluster  -> f -compatible for Element of K10(g);
coherence
 for b1 being Subset of g holds b1 is f -compatible
proof
let h be Subset of g; ::_thesis: h is f -compatible
 h = g | (dom h) by Th34;
hence  h is f -compatible ; ::_thesis: verum
end;
end;

theorem :: GRFUNC_1:35
for x, X being set
for g, f being Function st g c= f & x in X & X /\ (dom f) c= dom g holds
f . x = g . x
proof
let x, X be set ; ::_thesis: for g, f being Function st g c= f & x in X & X /\ (dom f) c= dom g holds
f . x = g . x
let g, f be Function; ::_thesis: ( g c= f & x in X & X /\ (dom f) c= dom g implies f . x = g . x )
assume that
A1: g c= f and
A2: x in X and
A3: X /\ (dom f) c= dom g ; ::_thesis: f . x = g . x
percases ( x in dom g or not x in dom g ) ;
suppose x in dom g ; ::_thesis: f . x = g . x
hence  f . x = g . x by A1, Th2; ::_thesis: verum
end;
supposeA4: not x in dom g ; ::_thesis: f . x = g . x
then  not x in X /\ (dom f) by A3;
then  not x in dom f by A2, XBOOLE_0:def_4;
hence f . x = {} by FUNCT_1:def_2
.= g . x by A4, FUNCT_1:def_2 ;
::_thesis: verum
end;
end;
end;