:: 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;