:: FUNCOP_1 semantic presentation begin theorem Th1: :: FUNCOP_1:1 for A being set holds delta A = <:(id A),(id A):> proof let A be set ; ::_thesis: delta A = <:(id A),(id A):> thus delta A = (id [:A,A:]) * (delta A) by FUNCT_2:17 .= [:(id A),(id A):] * (delta A) by FUNCT_3:69 .= <:(id A),(id A):> by FUNCT_3:78 ; ::_thesis: verum end; definition let f be Function; funcf ~ -> Function means :Def1: :: FUNCOP_1:def 1 ( dom it = dom f & ( for x being set st x in dom f holds ( ( for y, z being set st f . x = [y,z] holds it . x = [z,y] ) & ( f . x = it . x or ex y, z being set st f . x = [y,z] ) ) ) ); existence ex b1 being Function st ( dom b1 = dom f & ( for x being set st x in dom f holds ( ( for y, z being set st f . x = [y,z] holds b1 . x = [z,y] ) & ( f . x = b1 . x or ex y, z being set st f . x = [y,z] ) ) ) ) proof defpred S1[ set , set ] means ( ( for y, z being set st f . \$1 = [y,z] holds \$2 = [z,y] ) & ( f . \$1 = \$2 or ex y, z being set st f . \$1 = [y,z] ) ); A1: now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ ex_y_being_set_st_S1[x,y] let x be set ; ::_thesis: ( x in dom f implies ex y being set st S1[x,y] ) assume x in dom f ; ::_thesis: ex y being set st S1[x,y] now__::_thesis:_ex_y1_being_set_st_ (_(_for_y,_z_being_set_st_f_._x_=_[y,z]_holds_ y1_=_[z,y]_)_&_(_f_._x_=_y1_or_ex_y,_z_being_set_st_f_._x_=_[y,z]_)_) percases ( ex y, z being set st f . x = [y,z] or for y, z being set holds not f . x = [y,z] ) ; supposeA2: ex y, z being set st f . x = [y,z] ; ::_thesis: ex y1 being set st ( ( for y, z being set st f . x = [y,z] holds y1 = [z,y] ) & ( f . x = y1 or ex y, z being set st f . x = [y,z] ) ) then consider y, z being set such that A3: f . x = [y,z] ; take y1 = [z,y]; ::_thesis: ( ( for y, z being set st f . x = [y,z] holds y1 = [z,y] ) & ( f . x = y1 or ex y, z being set st f . x = [y,z] ) ) thus for y, z being set st f . x = [y,z] holds y1 = [z,y] ::_thesis: ( f . x = y1 or ex y, z being set st f . x = [y,z] ) proof let y9, z9 be set ; ::_thesis: ( f . x = [y9,z9] implies y1 = [z9,y9] ) assume A4: f . x = [y9,z9] ; ::_thesis: y1 = [z9,y9] then z = z9 by A3, XTUPLE_0:1; hence y1 = [z9,y9] by A3, A4, XTUPLE_0:1; ::_thesis: verum end; thus ( f . x = y1 or ex y, z being set st f . x = [y,z] ) by A2; ::_thesis: verum end; supposeA5: for y, z being set holds not f . x = [y,z] ; ::_thesis: ex y1 being set st ( ( for y, z being set st f . x = [y,z] holds y1 = [z,y] ) & ( f . x = y1 or ex y, z being set st f . x = [y,z] ) ) take y1 = f . x; ::_thesis: ( ( for y, z being set st f . x = [y,z] holds y1 = [z,y] ) & ( f . x = y1 or ex y, z being set st f . x = [y,z] ) ) thus ( ( for y, z being set st f . x = [y,z] holds y1 = [z,y] ) & ( f . x = y1 or ex y, z being set st f . x = [y,z] ) ) by A5; ::_thesis: verum end; end; end; hence ex y being set st S1[x,y] ; ::_thesis: verum end; A6: now__::_thesis:_for_x,_y1,_y2_being_set_st_x_in_dom_f_&_S1[x,y1]_&_S1[x,y2]_holds_ y1_=_y2 let x, y1, y2 be set ; ::_thesis: ( x in dom f & S1[x,y1] & S1[x,y2] implies y1 = y2 ) assume x in dom f ; ::_thesis: ( S1[x,y1] & S1[x,y2] implies y1 = y2 ) assume that A7: S1[x,y1] and A8: S1[x,y2] ; ::_thesis: y1 = y2 now__::_thesis:_y1_=_y2 percases ( ex y, z being set st f . x = [y,z] or for y, z being set holds not f . x = [y,z] ) ; suppose ex y, z being set st f . x = [y,z] ; ::_thesis: y1 = y2 then consider y, z being set such that A9: f . x = [y,z] ; y1 = [z,y] by A7, A9; hence y1 = y2 by A8, A9; ::_thesis: verum end; suppose for y, z being set holds not f . x = [y,z] ; ::_thesis: y1 = y2 hence y1 = y2 by A7, A8; ::_thesis: verum end; end; end; hence y1 = y2 ; ::_thesis: verum end; thus ex g being Function st ( dom g = dom f & ( for x being set st x in dom f holds S1[x,g . x] ) ) from FUNCT_1:sch_2(A6, A1); ::_thesis: verum end; uniqueness for b1, b2 being Function st dom b1 = dom f & ( for x being set st x in dom f holds ( ( for y, z being set st f . x = [y,z] holds b1 . x = [z,y] ) & ( f . x = b1 . x or ex y, z being set st f . x = [y,z] ) ) ) & dom b2 = dom f & ( for x being set st x in dom f holds ( ( for y, z being set st f . x = [y,z] holds b2 . x = [z,y] ) & ( f . x = b2 . x or ex y, z being set st f . x = [y,z] ) ) ) holds b1 = b2 proof defpred S1[ Function] means for x being set st x in dom f holds ( ( for y, z being set st f . x = [y,z] holds \$1 . x = [z,y] ) & ( f . x = \$1 . x or ex y, z being set st f . x = [y,z] ) ); let g1, g2 be Function; ::_thesis: ( dom g1 = dom f & ( for x being set st x in dom f holds ( ( for y, z being set st f . x = [y,z] holds g1 . x = [z,y] ) & ( f . x = g1 . x or ex y, z being set st f . x = [y,z] ) ) ) & dom g2 = dom f & ( for x being set st x in dom f holds ( ( for y, z being set st f . x = [y,z] holds g2 . x = [z,y] ) & ( f . x = g2 . x or ex y, z being set st f . x = [y,z] ) ) ) implies g1 = g2 ) assume that A10: dom g1 = dom f and A11: S1[g1] and A12: dom g2 = dom f and A13: S1[g2] ; ::_thesis: g1 = g2 now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ g1_._x_=_g2_._x let x be set ; ::_thesis: ( x in dom f implies g1 . x = g2 . x ) assume A14: x in dom f ; ::_thesis: g1 . x = g2 . x now__::_thesis:_g1_._x_=_g2_._x percases ( ex y, z being set st f . x = [y,z] or for y, z being set holds not f . x = [y,z] ) ; suppose ex y, z being set st f . x = [y,z] ; ::_thesis: g1 . x = g2 . x then consider y, z being set such that A15: f . x = [y,z] ; g1 . x = [z,y] by A11, A14, A15; hence g1 . x = g2 . x by A13, A14, A15; ::_thesis: verum end; supposeA16: for y, z being set holds not f . x = [y,z] ; ::_thesis: g1 . x = g2 . x then g1 . x = f . x by A11, A14; hence g1 . x = g2 . x by A13, A14, A16; ::_thesis: verum end; end; end; hence g1 . x = g2 . x ; ::_thesis: verum end; hence g1 = g2 by A10, A12, FUNCT_1:2; ::_thesis: verum end; involutiveness for b1, b2 being Function st dom b1 = dom b2 & ( for x being set st x in dom b2 holds ( ( for y, z being set st b2 . x = [y,z] holds b1 . x = [z,y] ) & ( b2 . x = b1 . x or ex y, z being set st b2 . x = [y,z] ) ) ) holds ( dom b2 = dom b1 & ( for x being set st x in dom b1 holds ( ( for y, z being set st b1 . x = [y,z] holds b2 . x = [z,y] ) & ( b1 . x = b2 . x or ex y, z being set st b1 . x = [y,z] ) ) ) ) proof let g, f be Function; ::_thesis: ( dom g = dom f & ( for x being set st x in dom f holds ( ( for y, z being set st f . x = [y,z] holds g . x = [z,y] ) & ( f . x = g . x or ex y, z being set st f . x = [y,z] ) ) ) implies ( dom f = dom g & ( for x being set st x in dom g holds ( ( for y, z being set st g . x = [y,z] holds f . x = [z,y] ) & ( g . x = f . x or ex y, z being set st g . x = [y,z] ) ) ) ) ) assume that A17: dom g = dom f and A18: for x being set st x in dom f holds ( ( for y, z being set st f . x = [y,z] holds g . x = [z,y] ) & ( f . x = g . x or ex y, z being set st f . x = [y,z] ) ) ; ::_thesis: ( dom f = dom g & ( for x being set st x in dom g holds ( ( for y, z being set st g . x = [y,z] holds f . x = [z,y] ) & ( g . x = f . x or ex y, z being set st g . x = [y,z] ) ) ) ) thus dom f = dom g by A17; ::_thesis: for x being set st x in dom g holds ( ( for y, z being set st g . x = [y,z] holds f . x = [z,y] ) & ( g . x = f . x or ex y, z being set st g . x = [y,z] ) ) let x be set ; ::_thesis: ( x in dom g implies ( ( for y, z being set st g . x = [y,z] holds f . x = [z,y] ) & ( g . x = f . x or ex y, z being set st g . x = [y,z] ) ) ) assume A19: x in dom g ; ::_thesis: ( ( for y, z being set st g . x = [y,z] holds f . x = [z,y] ) & ( g . x = f . x or ex y, z being set st g . x = [y,z] ) ) thus for y, z being set st g . x = [y,z] holds f . x = [z,y] ::_thesis: ( g . x = f . x or ex y, z being set st g . x = [y,z] ) proof let y, z be set ; ::_thesis: ( g . x = [y,z] implies f . x = [z,y] ) assume A20: g . x = [y,z] ; ::_thesis: f . x = [z,y] percases ( ex z, y being set st f . x = [z,y] or for z, y being set holds not f . x = [z,y] ) ; suppose ex z, y being set st f . x = [z,y] ; ::_thesis: f . x = [z,y] then consider y1, y2 being set such that A21: f . x = [y1,y2] ; A22: g . x = [y2,y1] by A17, A18, A19, A21; then y = y2 by A20, XTUPLE_0:1; hence f . x = [z,y] by A20, A21, A22, XTUPLE_0:1; ::_thesis: verum end; suppose for z, y being set holds not f . x = [z,y] ; ::_thesis: f . x = [z,y] then f . x = g . x by A17, A18, A19; hence f . x = [z,y] by A17, A18, A19, A20; ::_thesis: verum end; end; end; assume g . x <> f . x ; ::_thesis: ex y, z being set st g . x = [y,z] then consider y, z being set such that A23: f . x = [y,z] by A17, A18, A19; take z ; ::_thesis: ex z being set st g . x = [z,z] take y ; ::_thesis: g . x = [z,y] thus g . x = [z,y] by A17, A18, A19, A23; ::_thesis: verum end; end; :: deftheorem Def1 defines ~ FUNCOP_1:def_1_:_ for f, b2 being Function holds ( b2 = f ~ iff ( dom b2 = dom f & ( for x being set st x in dom f holds ( ( for y, z being set st f . x = [y,z] holds b2 . x = [z,y] ) & ( f . x = b2 . x or ex y, z being set st f . x = [y,z] ) ) ) ) ); theorem Th2: :: FUNCOP_1:2 for f, g being Function holds <:f,g:> = <:g,f:> ~ proof let f, g be Function; ::_thesis: <:f,g:> = <:g,f:> ~ A1: dom <:f,g:> = (dom g) /\ (dom f) by FUNCT_3:def_7 .= dom <:g,f:> by FUNCT_3:def_7 ; A2: now__::_thesis:_for_x_being_set_st_x_in_dom_<:f,g:>_holds_ <:f,g:>_._x_=_(<:g,f:>_~)_._x 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 then A4: <:g,f:> . x = [(g . x),(f . x)] by A1, FUNCT_3:def_7; thus <:f,g:> . x = [(f . x),(g . x)] by A3, FUNCT_3:def_7 .= (<:g,f:> ~) . x by A1, A3, A4, Def1 ; ::_thesis: verum end; dom <:f,g:> = dom (<:g,f:> ~) by A1, Def1; hence <:f,g:> = <:g,f:> ~ by A2, FUNCT_1:2; ::_thesis: verum end; theorem Th3: :: FUNCOP_1:3 for f being Function for A being set holds (f | A) ~ = (f ~) | A proof let f be Function; ::_thesis: for A being set holds (f | A) ~ = (f ~) | A let A be set ; ::_thesis: (f | A) ~ = (f ~) | A A1: dom (f | A) = (dom f) /\ A by RELAT_1:61 .= (dom (f ~)) /\ A by Def1 .= dom ((f ~) | A) by RELAT_1:61 ; A2: now__::_thesis:_for_x_being_set_st_x_in_dom_((f_~)_|_A)_holds_ ((f_|_A)_~)_._x_=_((f_~)_|_A)_._x let x be set ; ::_thesis: ( x in dom ((f ~) | A) implies ((f | A) ~) . x = ((f ~) | A) . x ) assume A3: x in dom ((f ~) | A) ; ::_thesis: ((f | A) ~) . x = ((f ~) | A) . x A4: dom (f | A) c= dom f by RELAT_1:60; now__::_thesis:_((f_|_A)_~)_._x_=_((f_~)_|_A)_._x percases ( ex y, z being set st (f | A) . x = [y,z] or for y, z being set holds not (f | A) . x = [y,z] ) ; suppose ex y, z being set st (f | A) . x = [y,z] ; ::_thesis: ((f | A) ~) . x = ((f ~) | A) . x then consider y, z being set such that A5: (f | A) . x = [y,z] ; A6: f . x = [y,z] by A1, A3, A5, FUNCT_1:47; thus ((f | A) ~) . x = [z,y] by A1, A3, A5, Def1 .= (f ~) . x by A1, A3, A4, A6, Def1 .= ((f ~) | A) . x by A3, FUNCT_1:47 ; ::_thesis: verum end; supposeA7: for y, z being set holds not (f | A) . x = [y,z] ; ::_thesis: ((f | A) ~) . x = ((f ~) | A) . x A8: (f | A) . x = f . x by A1, A3, FUNCT_1:47; ((f | A) ~) . x = (f | A) . x by A1, A3, A7, Def1; hence ((f | A) ~) . x = (f ~) . x by A1, A3, A4, A7, A8, Def1 .= ((f ~) | A) . x by A3, FUNCT_1:47 ; ::_thesis: verum end; end; end; hence ((f | A) ~) . x = ((f ~) | A) . x ; ::_thesis: verum end; dom ((f | A) ~) = dom (f | A) by Def1; hence (f | A) ~ = (f ~) | A by A1, A2, FUNCT_1:2; ::_thesis: verum end; theorem :: FUNCOP_1:4 for A being set holds (delta A) ~ = delta A proof let A be set ; ::_thesis: (delta A) ~ = delta A thus (delta A) ~ = <:(id A),(id A):> ~ by Th1 .= <:(id A),(id A):> by Th2 .= delta A by Th1 ; ::_thesis: verum end; theorem Th5: :: FUNCOP_1:5 for f, g being Function for A being set holds <:f,g:> | A = <:(f | A),g:> proof let f, g be Function; ::_thesis: for A being set holds <:f,g:> | A = <:(f | A),g:> let A be set ; ::_thesis: <:f,g:> | A = <:(f | A),g:> A1: dom (<:f,g:> | A) = (dom <:f,g:>) /\ A by RELAT_1:61 .= ((dom f) /\ (dom g)) /\ A by FUNCT_3:def_7 .= ((dom f) /\ A) /\ (dom g) by XBOOLE_1:16 .= (dom (f | A)) /\ (dom g) by RELAT_1:61 ; now__::_thesis:_for_x_being_set_st_x_in_dom_(<:f,g:>_|_A)_holds_ (<:f,g:>_|_A)_._x_=_[((f_|_A)_._x),(g_._x)] A2: dom (<:f,g:> | A) c= dom <:f,g:> by RELAT_1:60; let x be set ; ::_thesis: ( x in dom (<:f,g:> | A) implies (<:f,g:> | A) . x = [((f | A) . x),(g . x)] ) assume A3: x in dom (<:f,g:> | A) ; ::_thesis: (<:f,g:> | A) . x = [((f | A) . x),(g . x)] A4: x in dom (f | A) by A1, A3, XBOOLE_0:def_4; thus (<:f,g:> | A) . x = <:f,g:> . x by A3, FUNCT_1:47 .= [(f . x),(g . x)] by A3, A2, FUNCT_3:def_7 .= [((f | A) . x),(g . x)] by A4, FUNCT_1:47 ; ::_thesis: verum end; hence <:f,g:> | A = <:(f | A),g:> by A1, FUNCT_3:def_7; ::_thesis: verum end; theorem Th6: :: FUNCOP_1:6 for f, g being Function for A being set holds <:f,g:> | A = <:f,(g | A):> proof let f, g be Function; ::_thesis: for A being set holds <:f,g:> | A = <:f,(g | A):> let A be set ; ::_thesis: <:f,g:> | A = <:f,(g | A):> thus <:f,g:> | A = (<:g,f:> ~) | A by Th2 .= (<:g,f:> | A) ~ by Th3 .= <:(g | A),f:> ~ by Th5 .= <:f,(g | A):> by Th2 ; ::_thesis: verum end; definition let A, z be set ; funcA --> z -> set equals :: FUNCOP_1:def 2 [:A,{z}:]; coherence [:A,{z}:] is set ; end; :: deftheorem defines --> FUNCOP_1:def_2_:_ for A, z being set holds A --> z = [:A,{z}:]; registration let A, z be set ; clusterA --> z -> Relation-like Function-like ; coherence ( A --> z is Function-like & A --> z is Relation-like ) proof thus A --> z is Function-like ::_thesis: A --> z is Relation-like proof let x be set ; :: according to FUNCT_1:def_1 ::_thesis: for b1, b2 being set holds ( not [x,b1] in A --> z or not [x,b2] in A --> z or b1 = b2 ) let y1, y2 be set ; ::_thesis: ( not [x,y1] in A --> z or not [x,y2] in A --> z or y1 = y2 ) assume that A1: [x,y1] in A --> z and A2: [x,y2] in A --> z ; ::_thesis: y1 = y2 y1 in {z} by A1, ZFMISC_1:87; then A3: y1 = z by TARSKI:def_1; y2 in {z} by A2, ZFMISC_1:87; hence y1 = y2 by A3, TARSKI:def_1; ::_thesis: verum end; thus for x being set st x in A --> z holds ex y1, y2 being set st [y1,y2] = x by RELAT_1:def_1; :: according to RELAT_1:def_1 ::_thesis: verum end; end; theorem Th7: :: FUNCOP_1:7 for A, x, z being set st x in A holds (A --> z) . x = z proof let A, x, z be set ; ::_thesis: ( x in A implies (A --> z) . x = z ) assume A1: x in A ; ::_thesis: (A --> z) . x = z z in {z} by TARSKI:def_1; then [x,z] in A --> z by A1, ZFMISC_1:87; hence (A --> z) . x = z by FUNCT_1:1; ::_thesis: verum end; theorem :: FUNCOP_1:8 for A, x being set st A <> {} holds rng (A --> x) = {x} by RELAT_1:160; theorem Th9: :: FUNCOP_1:9 for f being Function for x being set st rng f = {x} holds f = (dom f) --> x proof let f be Function; ::_thesis: for x being set st rng f = {x} holds f = (dom f) --> x let x be set ; ::_thesis: ( rng f = {x} implies f = (dom f) --> x ) assume A1: rng f = {x} ; ::_thesis: f = (dom f) --> x then dom f <> {} by RELAT_1:42; then ( dom ((dom f) --> x) = dom f & rng ((dom f) --> x) = {x} ) by RELAT_1:160; hence f = (dom f) --> x by A1, FUNCT_1:7; ::_thesis: verum end; registration let x be set ; cluster{} --> x -> empty ; coherence {} --> x is empty by ZFMISC_1:90; end; registration let x be set ; let A be empty set ; clusterA --> x -> empty ; coherence A --> x is empty ; end; registration let x be set ; let A be non empty set ; clusterA --> x -> non empty ; coherence not A --> x is empty ; end; theorem :: FUNCOP_1:10 for x being set holds ( dom ({} --> x) = {} & rng ({} --> x) = {} ) ; theorem Th11: :: FUNCOP_1:11 for f being Function for x being set st ( for z being set st z in dom f holds f . z = x ) holds f = (dom f) --> x proof let f be Function; ::_thesis: for x being set st ( for z being set st z in dom f holds f . z = x ) holds f = (dom f) --> x let x be set ; ::_thesis: ( ( for z being set st z in dom f holds f . z = x ) implies f = (dom f) --> x ) assume A1: for z being set st z in dom f holds f . z = x ; ::_thesis: f = (dom f) --> x now__::_thesis:_f_=_(dom_f)_-->_x percases ( dom f = {} or dom f <> {} ) ; supposeA2: dom f = {} ; ::_thesis: f = (dom f) --> x dom ({} --> x) = {} ; hence f = (dom f) --> x by A2; ::_thesis: verum end; supposeA3: dom f <> {} ; ::_thesis: f = (dom f) --> x set z = the Element of dom f; now__::_thesis:_for_y_being_set_holds_ (_(_y_in_{x}_implies_ex_y1_being_set_st_ (_y1_in_dom_f_&_y_=_f_._y1_)_)_&_(_ex_y1_being_set_st_ (_y1_in_dom_f_&_y_=_f_._y1_)_implies_y_in_{x}_)_) let y be set ; ::_thesis: ( ( y in {x} implies ex y1 being set st ( y1 in dom f & y = f . y1 ) ) & ( ex y1 being set st ( y1 in dom f & y = f . y1 ) implies y in {x} ) ) thus ( y in {x} implies ex y1 being set st ( y1 in dom f & y = f . y1 ) ) ::_thesis: ( ex y1 being set st ( y1 in dom f & y = f . y1 ) implies y in {x} ) proof assume y in {x} ; ::_thesis: ex y1 being set st ( y1 in dom f & y = f . y1 ) then y = x by TARSKI:def_1; then f . the Element of dom f = y by A1, A3; hence ex y1 being set st ( y1 in dom f & y = f . y1 ) by A3; ::_thesis: verum end; assume ex y1 being set st ( y1 in dom f & y = f . y1 ) ; ::_thesis: y in {x} then y = x by A1; hence y in {x} by TARSKI:def_1; ::_thesis: verum end; then rng f = {x} by FUNCT_1:def_3; hence f = (dom f) --> x by Th9; ::_thesis: verum end; end; end; hence f = (dom f) --> x ; ::_thesis: verum end; theorem Th12: :: FUNCOP_1:12 for A, x, B being set holds (A --> x) | B = (A /\ B) --> x proof let A, x, B be set ; ::_thesis: (A --> x) | B = (A /\ B) --> x A1: ( A = {} or A <> {} ) ; A2: ( A /\ B = {} or A /\ B <> {} ) ; A3: dom ((A --> x) | B) = (dom (A --> x)) /\ B by RELAT_1:61 .= A /\ B by A1, RELAT_1:160 .= dom ((A /\ B) --> x) by A2, RELAT_1:160 ; now__::_thesis:_for_z_being_set_st_z_in_dom_((A_/\_B)_-->_x)_holds_ ((A_-->_x)_|_B)_._z_=_((A_/\_B)_-->_x)_._z let z be set ; ::_thesis: ( z in dom ((A /\ B) --> x) implies ((A --> x) | B) . z = ((A /\ B) --> x) . z ) assume A4: z in dom ((A /\ B) --> x) ; ::_thesis: ((A --> x) | B) . z = ((A /\ B) --> x) . z ( A /\ B = {} or A /\ B <> {} ) ; then A5: z in A /\ B by A4, RELAT_1:160; then A6: z in A by XBOOLE_0:def_4; thus ((A --> x) | B) . z = (A --> x) . z by A3, A4, FUNCT_1:47 .= x by A6, Th7 .= ((A /\ B) --> x) . z by A5, Th7 ; ::_thesis: verum end; hence (A --> x) | B = (A /\ B) --> x by A3, FUNCT_1:2; ::_thesis: verum end; theorem Th13: :: FUNCOP_1:13 for A, x being set holds ( dom (A --> x) = A & rng (A --> x) c= {x} ) proof let A, x be set ; ::_thesis: ( dom (A --> x) = A & rng (A --> x) c= {x} ) now__::_thesis:_(_dom_(A_-->_x)_=_A_&_rng_(A_-->_x)_c=_{x}_) percases ( A = {} or A <> {} ) ; supposeA1: A = {} ; ::_thesis: ( dom (A --> x) = A & rng (A --> x) c= {x} ) rng ({} --> x) = {} ; hence ( dom (A --> x) = A & rng (A --> x) c= {x} ) by A1, XBOOLE_1:2; ::_thesis: verum end; suppose A <> {} ; ::_thesis: ( dom (A --> x) = A & rng (A --> x) c= {x} ) hence ( dom (A --> x) = A & rng (A --> x) c= {x} ) by RELAT_1:160; ::_thesis: verum end; end; end; hence ( dom (A --> x) = A & rng (A --> x) c= {x} ) ; ::_thesis: verum end; theorem Th14: :: FUNCOP_1:14 for A, x, B being set st x in B holds (A --> x) " B = A proof let A, x, B be set ; ::_thesis: ( x in B implies (A --> x) " B = A ) assume A1: x in B ; ::_thesis: (A --> x) " B = A now__::_thesis:_(A_-->_x)_"_B_=_A percases ( A = {} or A <> {} ) ; supposeA2: A = {} ; ::_thesis: (A --> x) " B = A thus (A --> x) " B = A by A2; ::_thesis: verum end; suppose A <> {} ; ::_thesis: (A --> x) " B = A then A3: rng (A --> x) = {x} by RELAT_1:160; {x} c= B by A1, ZFMISC_1:31; then {x} /\ B = {x} by XBOOLE_1:28; hence (A --> x) " B = (A --> x) " {x} by A3, RELAT_1:133 .= dom (A --> x) by A3, RELAT_1:134 .= A by Th13 ; ::_thesis: verum end; end; end; hence (A --> x) " B = A ; ::_thesis: verum end; theorem :: FUNCOP_1:15 for A, x being set holds (A --> x) " {x} = A proof let A, x be set ; ::_thesis: (A --> x) " {x} = A x in {x} by TARSKI:def_1; hence (A --> x) " {x} = A by Th14; ::_thesis: verum end; theorem :: FUNCOP_1:16 for A, x, B being set st not x in B holds (A --> x) " B = {} proof let A, x, B be set ; ::_thesis: ( not x in B implies (A --> x) " B = {} ) assume A1: not x in B ; ::_thesis: (A --> x) " B = {} rng (A --> x) c= {x} by Th13; then rng (A --> x) misses B by A1, XBOOLE_1:63, ZFMISC_1:50; hence (A --> x) " B = {} by RELAT_1:138; ::_thesis: verum end; theorem :: FUNCOP_1:17 for h being Function for A, x being set st x in dom h holds h * (A --> x) = A --> (h . x) proof let h be Function; ::_thesis: for A, x being set st x in dom h holds h * (A --> x) = A --> (h . x) let A, x be set ; ::_thesis: ( x in dom h implies h * (A --> x) = A --> (h . x) ) assume A1: x in dom h ; ::_thesis: h * (A --> x) = A --> (h . x) A2: now__::_thesis:_for_z_being_set_st_z_in_dom_(h_*_(A_-->_x))_holds_ (h_*_(A_-->_x))_._z_=_(A_-->_(h_._x))_._z let z be set ; ::_thesis: ( z in dom (h * (A --> x)) implies (h * (A --> x)) . z = (A --> (h . x)) . z ) assume A3: z in dom (h * (A --> x)) ; ::_thesis: (h * (A --> x)) . z = (A --> (h . x)) . z then z in dom (A --> x) by FUNCT_1:11; then A4: z in A by Th13; thus (h * (A --> x)) . z = h . ((A --> x) . z) by A3, FUNCT_1:12 .= h . x by A4, Th7 .= (A --> (h . x)) . z by A4, Th7 ; ::_thesis: verum end; dom (h * (A --> x)) = (A --> x) " (dom h) by RELAT_1:147 .= A by A1, Th14 .= dom (A --> (h . x)) by Th13 ; hence h * (A --> x) = A --> (h . x) by A2, FUNCT_1:2; ::_thesis: verum end; theorem :: FUNCOP_1:18 for h being Function for A, x being set st A <> {} & x in dom h holds dom (h * (A --> x)) <> {} proof let h be Function; ::_thesis: for A, x being set st A <> {} & x in dom h holds dom (h * (A --> x)) <> {} let A, x be set ; ::_thesis: ( A <> {} & x in dom h implies dom (h * (A --> x)) <> {} ) assume that A1: A <> {} and A2: x in dom h ; ::_thesis: dom (h * (A --> x)) <> {} set y = the Element of A; the Element of A in A by A1; then A3: the Element of A in dom (A --> x) by Th13; (A --> x) . the Element of A = x by A1, Th7; hence dom (h * (A --> x)) <> {} by A2, A3, FUNCT_1:11; ::_thesis: verum end; theorem :: FUNCOP_1:19 for h being Function for A, x being set holds (A --> x) * h = (h " A) --> x proof let h be Function; ::_thesis: for A, x being set holds (A --> x) * h = (h " A) --> x let A, x be set ; ::_thesis: (A --> x) * h = (h " A) --> x A1: dom ((A --> x) * h) = h " (dom (A --> x)) by RELAT_1:147 .= h " A by Th13 ; A2: now__::_thesis:_for_z_being_set_st_z_in_dom_((A_-->_x)_*_h)_holds_ ((A_-->_x)_*_h)_._z_=_((h_"_A)_-->_x)_._z let z be set ; ::_thesis: ( z in dom ((A --> x) * h) implies ((A --> x) * h) . z = ((h " A) --> x) . z ) assume A3: z in dom ((A --> x) * h) ; ::_thesis: ((A --> x) * h) . z = ((h " A) --> x) . z then h . z in dom (A --> x) by FUNCT_1:11; then A4: h . z in A by Th13; thus ((A --> x) * h) . z = (A --> x) . (h . z) by A3, FUNCT_1:12 .= x by A4, Th7 .= ((h " A) --> x) . z by A1, A3, Th7 ; ::_thesis: verum end; dom ((A --> x) * h) = dom ((h " A) --> x) by A1, Th13; hence (A --> x) * h = (h " A) --> x by A2, FUNCT_1:2; ::_thesis: verum end; theorem :: FUNCOP_1:20 for A, x, y being set holds (A --> [x,y]) ~ = A --> [y,x] proof let A, x, y be set ; ::_thesis: (A --> [x,y]) ~ = A --> [y,x] A1: dom ((A --> [x,y]) ~) = dom (A --> [x,y]) by Def1; then A2: dom ((A --> [x,y]) ~) = A by Th13; A3: now__::_thesis:_for_z_being_set_st_z_in_dom_((A_-->_[x,y])_~)_holds_ ((A_-->_[x,y])_~)_._z_=_(A_-->_[y,x])_._z let z be set ; ::_thesis: ( z in dom ((A --> [x,y]) ~) implies ((A --> [x,y]) ~) . z = (A --> [y,x]) . z ) assume A4: z in dom ((A --> [x,y]) ~) ; ::_thesis: ((A --> [x,y]) ~) . z = (A --> [y,x]) . z then (A --> [x,y]) . z = [x,y] by A2, Th7; hence ((A --> [x,y]) ~) . z = [y,x] by A1, A4, Def1 .= (A --> [y,x]) . z by A2, A4, Th7 ; ::_thesis: verum end; dom ((A --> [x,y]) ~) = dom (A --> [y,x]) by A2, Th13; hence (A --> [x,y]) ~ = A --> [y,x] by A3, FUNCT_1:2; ::_thesis: verum end; definition let F, f, g be Function; funcF .: (f,g) -> set equals :: FUNCOP_1:def 3 F * <:f,g:>; correctness coherence F * <:f,g:> is set ; ; end; :: deftheorem defines .: FUNCOP_1:def_3_:_ for F, f, g being Function holds F .: (f,g) = F * <:f,g:>; registration let F, f, g be Function; clusterF .: (f,g) -> Relation-like Function-like ; coherence ( F .: (f,g) is Function-like & F .: (f,g) is Relation-like ) ; end; Lm1: for f, g, F being Function for x being set st x in dom (F * <:f,g:>) holds (F * <:f,g:>) . x = F . ((f . x),(g . x)) proof let f, g, F be Function; ::_thesis: for x being set st x in dom (F * <:f,g:>) holds (F * <:f,g:>) . x = F . ((f . x),(g . x)) let x be set ; ::_thesis: ( x in dom (F * <:f,g:>) implies (F * <:f,g:>) . x = F . ((f . x),(g . x)) ) assume A1: x in dom (F * <:f,g:>) ; ::_thesis: (F * <:f,g:>) . x = F . ((f . x),(g . x)) then A2: x in dom <:f,g:> by FUNCT_1:11; thus (F * <:f,g:>) . x = F . (<:f,g:> . x) by A1, FUNCT_1:12 .= F . ((f . x),(g . x)) by A2, FUNCT_3:def_7 ; ::_thesis: verum end; theorem :: FUNCOP_1:21 for f, g, F, h being Function st dom h = dom (F .: (f,g)) & ( for z being set st z in dom (F .: (f,g)) holds h . z = F . ((f . z),(g . z)) ) holds h = F .: (f,g) proof let f, g, F, h be Function; ::_thesis: ( dom h = dom (F .: (f,g)) & ( for z being set st z in dom (F .: (f,g)) holds h . z = F . ((f . z),(g . z)) ) implies h = F .: (f,g) ) assume that A1: dom h = dom (F .: (f,g)) and A2: for z being set st z in dom (F .: (f,g)) holds h . z = F . ((f . z),(g . z)) ; ::_thesis: h = F .: (f,g) now__::_thesis:_for_z_being_set_st_z_in_dom_(F_.:_(f,g))_holds_ h_._z_=_(F_.:_(f,g))_._z let z be set ; ::_thesis: ( z in dom (F .: (f,g)) implies h . z = (F .: (f,g)) . z ) assume A3: z in dom (F .: (f,g)) ; ::_thesis: h . z = (F .: (f,g)) . z hence h . z = F . ((f . z),(g . z)) by A2 .= (F .: (f,g)) . z by A3, Lm1 ; ::_thesis: verum end; hence h = F .: (f,g) by A1, FUNCT_1:2; ::_thesis: verum end; theorem :: FUNCOP_1:22 for f, g, F being Function for x being set st x in dom (F .: (f,g)) holds (F .: (f,g)) . x = F . ((f . x),(g . x)) by Lm1; theorem Th23: :: FUNCOP_1:23 for f, g, h being Function for A being set for F being Function st f | A = g | A holds (F .: (f,h)) | A = (F .: (g,h)) | A proof let f, g, h be Function; ::_thesis: for A being set for F being Function st f | A = g | A holds (F .: (f,h)) | A = (F .: (g,h)) | A let A be set ; ::_thesis: for F being Function st f | A = g | A holds (F .: (f,h)) | A = (F .: (g,h)) | A let F be Function; ::_thesis: ( f | A = g | A implies (F .: (f,h)) | A = (F .: (g,h)) | A ) assume A1: f | A = g | A ; ::_thesis: (F .: (f,h)) | A = (F .: (g,h)) | A thus (F .: (f,h)) | A = F * (<:f,h:> | A) by RELAT_1:83 .= F * <:(f | A),h:> by Th5 .= F * (<:g,h:> | A) by A1, Th5 .= (F .: (g,h)) | A by RELAT_1:83 ; ::_thesis: verum end; theorem Th24: :: FUNCOP_1:24 for f, g, h being Function for A being set for F being Function st f | A = g | A holds (F .: (h,f)) | A = (F .: (h,g)) | A proof let f, g, h be Function; ::_thesis: for A being set for F being Function st f | A = g | A holds (F .: (h,f)) | A = (F .: (h,g)) | A let A be set ; ::_thesis: for F being Function st f | A = g | A holds (F .: (h,f)) | A = (F .: (h,g)) | A let F be Function; ::_thesis: ( f | A = g | A implies (F .: (h,f)) | A = (F .: (h,g)) | A ) assume A1: f | A = g | A ; ::_thesis: (F .: (h,f)) | A = (F .: (h,g)) | A thus (F .: (h,f)) | A = F * (<:h,f:> | A) by RELAT_1:83 .= F * <:h,(f | A):> by Th6 .= F * (<:h,g:> | A) by A1, Th6 .= (F .: (h,g)) | A by RELAT_1:83 ; ::_thesis: verum end; theorem Th25: :: FUNCOP_1:25 for f, g, h, F being Function holds (F .: (f,g)) * h = F .: ((f * h),(g * h)) proof let f, g, h, F be Function; ::_thesis: (F .: (f,g)) * h = F .: ((f * h),(g * h)) thus (F .: (f,g)) * h = F * (<:f,g:> * h) by RELAT_1:36 .= F .: ((f * h),(g * h)) by FUNCT_3:55 ; ::_thesis: verum end; definition let F, f be Function; let x be set ; funcF [:] (f,x) -> set equals :: FUNCOP_1:def 4 F * <:f,((dom f) --> x):>; correctness coherence F * <:f,((dom f) --> x):> is set ; ; end; :: deftheorem defines [:] FUNCOP_1:def_4_:_ for F, f being Function for x being set holds F [:] (f,x) = F * <:f,((dom f) --> x):>; registration let F, f be Function; let x be set ; clusterF [:] (f,x) -> Relation-like Function-like ; coherence ( F [:] (f,x) is Function-like & F [:] (f,x) is Relation-like ) ; end; theorem :: FUNCOP_1:26 for f, F being Function for x being set holds F [:] (f,x) = F .: (f,((dom f) --> x)) ; theorem Th27: :: FUNCOP_1:27 for f, F being Function for x, z being set st x in dom (F [:] (f,z)) holds (F [:] (f,z)) . x = F . ((f . x),z) proof let f, F be Function; ::_thesis: for x, z being set st x in dom (F [:] (f,z)) holds (F [:] (f,z)) . x = F . ((f . x),z) let x, z be set ; ::_thesis: ( x in dom (F [:] (f,z)) implies (F [:] (f,z)) . x = F . ((f . x),z) ) A1: dom <:f,((dom f) --> z):> = (dom f) /\ (dom ((dom f) --> z)) by FUNCT_3:def_7; assume A2: x in dom (F [:] (f,z)) ; ::_thesis: (F [:] (f,z)) . x = F . ((f . x),z) then x in dom <:f,((dom f) --> z):> by FUNCT_1:11; then A3: x in dom f by A1, XBOOLE_0:def_4; thus (F [:] (f,z)) . x = F . ((f . x),(((dom f) --> z) . x)) by A2, Lm1 .= F . ((f . x),z) by A3, Th7 ; ::_thesis: verum end; theorem :: FUNCOP_1:28 for f, g being Function for A being set for F being Function for x being set st f | A = g | A holds (F [:] (f,x)) | A = (F [:] (g,x)) | A proof let f, g be Function; ::_thesis: for A being set for F being Function for x being set st f | A = g | A holds (F [:] (f,x)) | A = (F [:] (g,x)) | A let A be set ; ::_thesis: for F being Function for x being set st f | A = g | A holds (F [:] (f,x)) | A = (F [:] (g,x)) | A let F be Function; ::_thesis: for x being set st f | A = g | A holds (F [:] (f,x)) | A = (F [:] (g,x)) | A let x be set ; ::_thesis: ( f | A = g | A implies (F [:] (f,x)) | A = (F [:] (g,x)) | A ) assume A1: f | A = g | A ; ::_thesis: (F [:] (f,x)) | A = (F [:] (g,x)) | A (dom f) /\ A = dom (f | A) by RELAT_1:61 .= (dom g) /\ A by A1, RELAT_1:61 ; then A2: ((dom f) --> x) | A = ((dom g) /\ A) --> x by Th12 .= ((dom g) --> x) | A by Th12 ; thus (F [:] (f,x)) | A = (F .: (f,((dom f) --> x))) | A .= (F .: (g,((dom f) --> x))) | A by A1, Th23 .= (F .: (g,((dom g) --> x))) | A by A2, Th24 .= (F [:] (g,x)) | A ; ::_thesis: verum end; theorem Th29: :: FUNCOP_1:29 for f, h, F being Function for x being set holds (F [:] (f,x)) * h = F [:] ((f * h),x) proof let f, h, F be Function; ::_thesis: for x being set holds (F [:] (f,x)) * h = F [:] ((f * h),x) let x be set ; ::_thesis: (F [:] (f,x)) * h = F [:] ((f * h),x) A1: dom ((dom f) --> x) = dom f by Th13; then A2: dom (((dom f) --> x) * h) = dom (f * h) by RELAT_1:163; A3: now__::_thesis:_for_z_being_set_st_z_in_dom_(((dom_f)_-->_x)_*_h)_holds_ (((dom_f)_-->_x)_*_h)_._z_=_x let z be set ; ::_thesis: ( z in dom (((dom f) --> x) * h) implies (((dom f) --> x) * h) . z = x ) assume A4: z in dom (((dom f) --> x) * h) ; ::_thesis: (((dom f) --> x) * h) . z = x then A5: h . z in dom ((dom f) --> x) by FUNCT_1:11; thus (((dom f) --> x) * h) . z = ((dom f) --> x) . (h . z) by A4, FUNCT_1:12 .= x by A1, A5, Th7 ; ::_thesis: verum end; thus (F [:] (f,x)) * h = (F .: (f,((dom f) --> x))) * h .= F .: ((f * h),(((dom f) --> x) * h)) by Th25 .= F [:] ((f * h),x) by A2, A3, Th11 ; ::_thesis: verum end; theorem :: FUNCOP_1:30 for f being Function for A being set for F being Function for x being set holds (F [:] (f,x)) * (id A) = F [:] ((f | A),x) proof let f be Function; ::_thesis: for A being set for F being Function for x being set holds (F [:] (f,x)) * (id A) = F [:] ((f | A),x) let A be set ; ::_thesis: for F being Function for x being set holds (F [:] (f,x)) * (id A) = F [:] ((f | A),x) let F be Function; ::_thesis: for x being set holds (F [:] (f,x)) * (id A) = F [:] ((f | A),x) let x be set ; ::_thesis: (F [:] (f,x)) * (id A) = F [:] ((f | A),x) thus (F [:] (f,x)) * (id A) = F [:] ((f * (id A)),x) by Th29 .= F [:] ((f | A),x) by RELAT_1:65 ; ::_thesis: verum end; definition let F be Function; let x be set ; let g be Function; funcF [;] (x,g) -> set equals :: FUNCOP_1:def 5 F * <:((dom g) --> x),g:>; correctness coherence F * <:((dom g) --> x),g:> is set ; ; end; :: deftheorem defines [;] FUNCOP_1:def_5_:_ for F being Function for x being set for g being Function holds F [;] (x,g) = F * <:((dom g) --> x),g:>; registration let F be Function; let x be set ; let g be Function; clusterF [;] (x,g) -> Relation-like Function-like ; coherence ( F [;] (x,g) is Function-like & F [;] (x,g) is Relation-like ) ; end; theorem :: FUNCOP_1:31 for g, F being Function for x being set holds F [;] (x,g) = F .: (((dom g) --> x),g) ; theorem Th32: :: FUNCOP_1:32 for f, F being Function for x, z being set st x in dom (F [;] (z,f)) holds (F [;] (z,f)) . x = F . (z,(f . x)) proof let f, F be Function; ::_thesis: for x, z being set st x in dom (F [;] (z,f)) holds (F [;] (z,f)) . x = F . (z,(f . x)) let x, z be set ; ::_thesis: ( x in dom (F [;] (z,f)) implies (F [;] (z,f)) . x = F . (z,(f . x)) ) A1: dom <:((dom f) --> z),f:> = (dom ((dom f) --> z)) /\ (dom f) by FUNCT_3:def_7; assume A2: x in dom (F [;] (z,f)) ; ::_thesis: (F [;] (z,f)) . x = F . (z,(f . x)) then x in dom <:((dom f) --> z),f:> by FUNCT_1:11; then A3: x in dom f by A1, XBOOLE_0:def_4; thus (F [;] (z,f)) . x = F . ((((dom f) --> z) . x),(f . x)) by A2, Lm1 .= F . (z,(f . x)) by A3, Th7 ; ::_thesis: verum end; theorem :: FUNCOP_1:33 for f, g being Function for A being set for F being Function for x being set st f | A = g | A holds (F [;] (x,f)) | A = (F [;] (x,g)) | A proof let f, g be Function; ::_thesis: for A being set for F being Function for x being set st f | A = g | A holds (F [;] (x,f)) | A = (F [;] (x,g)) | A let A be set ; ::_thesis: for F being Function for x being set st f | A = g | A holds (F [;] (x,f)) | A = (F [;] (x,g)) | A let F be Function; ::_thesis: for x being set st f | A = g | A holds (F [;] (x,f)) | A = (F [;] (x,g)) | A let x be set ; ::_thesis: ( f | A = g | A implies (F [;] (x,f)) | A = (F [;] (x,g)) | A ) assume A1: f | A = g | A ; ::_thesis: (F [;] (x,f)) | A = (F [;] (x,g)) | A (dom f) /\ A = dom (f | A) by RELAT_1:61 .= (dom g) /\ A by A1, RELAT_1:61 ; then A2: ((dom f) --> x) | A = ((dom g) /\ A) --> x by Th12 .= ((dom g) --> x) | A by Th12 ; thus (F [;] (x,f)) | A = (F .: (((dom f) --> x),f)) | A .= (F .: (((dom f) --> x),g)) | A by A1, Th24 .= (F .: (((dom g) --> x),g)) | A by A2, Th23 .= (F [;] (x,g)) | A ; ::_thesis: verum end; theorem Th34: :: FUNCOP_1:34 for f, h, F being Function for x being set holds (F [;] (x,f)) * h = F [;] (x,(f * h)) proof let f, h, F be Function; ::_thesis: for x being set holds (F [;] (x,f)) * h = F [;] (x,(f * h)) let x be set ; ::_thesis: (F [;] (x,f)) * h = F [;] (x,(f * h)) A1: dom ((dom f) --> x) = dom f by Th13; then A2: dom (((dom f) --> x) * h) = dom (f * h) by RELAT_1:163; A3: now__::_thesis:_for_z_being_set_st_z_in_dom_(((dom_f)_-->_x)_*_h)_holds_ (((dom_f)_-->_x)_*_h)_._z_=_x let z be set ; ::_thesis: ( z in dom (((dom f) --> x) * h) implies (((dom f) --> x) * h) . z = x ) assume A4: z in dom (((dom f) --> x) * h) ; ::_thesis: (((dom f) --> x) * h) . z = x then A5: h . z in dom ((dom f) --> x) by FUNCT_1:11; thus (((dom f) --> x) * h) . z = ((dom f) --> x) . (h . z) by A4, FUNCT_1:12 .= x by A1, A5, Th7 ; ::_thesis: verum end; thus (F [;] (x,f)) * h = (F .: (((dom f) --> x),f)) * h .= F .: ((((dom f) --> x) * h),(f * h)) by Th25 .= F [;] (x,(f * h)) by A2, A3, Th11 ; ::_thesis: verum end; theorem :: FUNCOP_1:35 for f being Function for A being set for F being Function for x being set holds (F [;] (x,f)) * (id A) = F [;] (x,(f | A)) proof let f be Function; ::_thesis: for A being set for F being Function for x being set holds (F [;] (x,f)) * (id A) = F [;] (x,(f | A)) let A be set ; ::_thesis: for F being Function for x being set holds (F [;] (x,f)) * (id A) = F [;] (x,(f | A)) let F be Function; ::_thesis: for x being set holds (F [;] (x,f)) * (id A) = F [;] (x,(f | A)) let x be set ; ::_thesis: (F [;] (x,f)) * (id A) = F [;] (x,(f | A)) thus (F [;] (x,f)) * (id A) = F [;] (x,(f * (id A))) by Th34 .= F [;] (x,(f | A)) by RELAT_1:65 ; ::_thesis: verum end; theorem Th36: :: FUNCOP_1:36 for X being non empty set for Y being set for F being BinOp of X for f, g being Function of Y,X holds F .: (f,g) is Function of Y,X proof let X be non empty set ; ::_thesis: for Y being set for F being BinOp of X for f, g being Function of Y,X holds F .: (f,g) is Function of Y,X let Y be set ; ::_thesis: for F being BinOp of X for f, g being Function of Y,X holds F .: (f,g) is Function of Y,X let F be BinOp of X; ::_thesis: for f, g being Function of Y,X holds F .: (f,g) is Function of Y,X let f, g be Function of Y,X; ::_thesis: F .: (f,g) is Function of Y,X F * <:f,g:> is Function of Y,X ; hence F .: (f,g) is Function of Y,X ; ::_thesis: verum end; definition let X be non empty set ; let Z be set ; let F be BinOp of X; let f, g be Function of Z,X; :: original: .: redefine funcF .: (f,g) -> Function of Z,X; coherence F .: (f,g) is Function of Z,X by Th36; end; theorem Th37: :: FUNCOP_1:37 for X, Y being non empty set for F being BinOp of X for f, g being Function of Y,X for z being Element of Y holds (F .: (f,g)) . z = F . ((f . z),(g . z)) proof let X, Y be non empty set ; ::_thesis: for F being BinOp of X for f, g being Function of Y,X for z being Element of Y holds (F .: (f,g)) . z = F . ((f . z),(g . z)) let F be BinOp of X; ::_thesis: for f, g being Function of Y,X for z being Element of Y holds (F .: (f,g)) . z = F . ((f . z),(g . z)) let f, g be Function of Y,X; ::_thesis: for z being Element of Y holds (F .: (f,g)) . z = F . ((f . z),(g . z)) let z be Element of Y; ::_thesis: (F .: (f,g)) . z = F . ((f . z),(g . z)) dom (F .: (f,g)) = Y by FUNCT_2:def_1; hence (F .: (f,g)) . z = F . ((f . z),(g . z)) by Lm1; ::_thesis: verum end; theorem Th38: :: FUNCOP_1:38 for X, Y being non empty set for F being BinOp of X for f, g, h being Function of Y,X st ( for z being Element of Y holds h . z = F . ((f . z),(g . z)) ) holds h = F .: (f,g) proof let X, Y be non empty set ; ::_thesis: for F being BinOp of X for f, g, h being Function of Y,X st ( for z being Element of Y holds h . z = F . ((f . z),(g . z)) ) holds h = F .: (f,g) let F be BinOp of X; ::_thesis: for f, g, h being Function of Y,X st ( for z being Element of Y holds h . z = F . ((f . z),(g . z)) ) holds h = F .: (f,g) let f, g, h be Function of Y,X; ::_thesis: ( ( for z being Element of Y holds h . z = F . ((f . z),(g . z)) ) implies h = F .: (f,g) ) assume A1: for z being Element of Y holds h . z = F . ((f . z),(g . z)) ; ::_thesis: h = F .: (f,g) now__::_thesis:_for_z_being_Element_of_Y_holds_h_._z_=_(F_.:_(f,g))_._z let z be Element of Y; ::_thesis: h . z = (F .: (f,g)) . z thus h . z = F . ((f . z),(g . z)) by A1 .= (F .: (f,g)) . z by Th37 ; ::_thesis: verum end; hence h = F .: (f,g) by FUNCT_2:63; ::_thesis: verum end; theorem :: FUNCOP_1:39 for X, Y being non empty set for F being BinOp of X for f being Function of Y,X for g being Function of X,X holds (F .: ((id X),g)) * f = F .: (f,(g * f)) proof let X, Y be non empty set ; ::_thesis: for F being BinOp of X for f being Function of Y,X for g being Function of X,X holds (F .: ((id X),g)) * f = F .: (f,(g * f)) let F be BinOp of X; ::_thesis: for f being Function of Y,X for g being Function of X,X holds (F .: ((id X),g)) * f = F .: (f,(g * f)) let f be Function of Y,X; ::_thesis: for g being Function of X,X holds (F .: ((id X),g)) * f = F .: (f,(g * f)) let g be Function of X,X; ::_thesis: (F .: ((id X),g)) * f = F .: (f,(g * f)) thus (F .: ((id X),g)) * f = F .: (((id X) * f),(g * f)) by Th25 .= F .: (f,(g * f)) by FUNCT_2:17 ; ::_thesis: verum end; theorem :: FUNCOP_1:40 for X, Y being non empty set for F being BinOp of X for f being Function of Y,X for g being Function of X,X holds (F .: (g,(id X))) * f = F .: ((g * f),f) proof let X, Y be non empty set ; ::_thesis: for F being BinOp of X for f being Function of Y,X for g being Function of X,X holds (F .: (g,(id X))) * f = F .: ((g * f),f) let F be BinOp of X; ::_thesis: for f being Function of Y,X for g being Function of X,X holds (F .: (g,(id X))) * f = F .: ((g * f),f) let f be Function of Y,X; ::_thesis: for g being Function of X,X holds (F .: (g,(id X))) * f = F .: ((g * f),f) let g be Function of X,X; ::_thesis: (F .: (g,(id X))) * f = F .: ((g * f),f) thus (F .: (g,(id X))) * f = F .: ((g * f),((id X) * f)) by Th25 .= F .: ((g * f),f) by FUNCT_2:17 ; ::_thesis: verum end; theorem :: FUNCOP_1:41 for X, Y being non empty set for F being BinOp of X for f being Function of Y,X holds (F .: ((id X),(id X))) * f = F .: (f,f) proof let X, Y be non empty set ; ::_thesis: for F being BinOp of X for f being Function of Y,X holds (F .: ((id X),(id X))) * f = F .: (f,f) let F be BinOp of X; ::_thesis: for f being Function of Y,X holds (F .: ((id X),(id X))) * f = F .: (f,f) let f be Function of Y,X; ::_thesis: (F .: ((id X),(id X))) * f = F .: (f,f) thus (F .: ((id X),(id X))) * f = F .: (((id X) * f),((id X) * f)) by Th25 .= F .: (((id X) * f),f) by FUNCT_2:17 .= F .: (f,f) by FUNCT_2:17 ; ::_thesis: verum end; theorem :: FUNCOP_1:42 for X being non empty set for F being BinOp of X for x being Element of X for g being Function of X,X holds (F .: ((id X),g)) . x = F . (x,(g . x)) proof let X be non empty set ; ::_thesis: for F being BinOp of X for x being Element of X for g being Function of X,X holds (F .: ((id X),g)) . x = F . (x,(g . x)) let F be BinOp of X; ::_thesis: for x being Element of X for g being Function of X,X holds (F .: ((id X),g)) . x = F . (x,(g . x)) let x be Element of X; ::_thesis: for g being Function of X,X holds (F .: ((id X),g)) . x = F . (x,(g . x)) let g be Function of X,X; ::_thesis: (F .: ((id X),g)) . x = F . (x,(g . x)) thus (F .: ((id X),g)) . x = F . (((id X) . x),(g . x)) by Th37 .= F . (x,(g . x)) by FUNCT_1:18 ; ::_thesis: verum end; theorem :: FUNCOP_1:43 for X being non empty set for F being BinOp of X for x being Element of X for g being Function of X,X holds (F .: (g,(id X))) . x = F . ((g . x),x) proof let X be non empty set ; ::_thesis: for F being BinOp of X for x being Element of X for g being Function of X,X holds (F .: (g,(id X))) . x = F . ((g . x),x) let F be BinOp of X; ::_thesis: for x being Element of X for g being Function of X,X holds (F .: (g,(id X))) . x = F . ((g . x),x) let x be Element of X; ::_thesis: for g being Function of X,X holds (F .: (g,(id X))) . x = F . ((g . x),x) let g be Function of X,X; ::_thesis: (F .: (g,(id X))) . x = F . ((g . x),x) thus (F .: (g,(id X))) . x = F . ((g . x),((id X) . x)) by Th37 .= F . ((g . x),x) by FUNCT_1:18 ; ::_thesis: verum end; theorem :: FUNCOP_1:44 for X being non empty set for F being BinOp of X for x being Element of X holds (F .: ((id X),(id X))) . x = F . (x,x) proof let X be non empty set ; ::_thesis: for F being BinOp of X for x being Element of X holds (F .: ((id X),(id X))) . x = F . (x,x) let F be BinOp of X; ::_thesis: for x being Element of X holds (F .: ((id X),(id X))) . x = F . (x,x) let x be Element of X; ::_thesis: (F .: ((id X),(id X))) . x = F . (x,x) thus (F .: ((id X),(id X))) . x = F . (((id X) . x),((id X) . x)) by Th37 .= F . (((id X) . x),x) by FUNCT_1:18 .= F . (x,x) by FUNCT_1:18 ; ::_thesis: verum end; theorem Th45: :: FUNCOP_1:45 for A, B, x being set st x in B holds A --> x is Function of A,B proof let A, B, x be set ; ::_thesis: ( x in B implies A --> x is Function of A,B ) A1: rng (A --> x) c= {x} by Th13; A2: dom (A --> x) = A by Th13; assume A3: x in B ; ::_thesis: A --> x is Function of A,B then {x} c= B by ZFMISC_1:31; then rng (A --> x) c= B by A1, XBOOLE_1:1; hence A --> x is Function of A,B by A3, A2, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; definition let I, i be set ; :: original: --> redefine funcI --> i -> Function of I,{i}; coherence I --> i is Function of I,{i} proof ( dom (I --> i) = I & rng (I --> i) c= {i} ) by Th13; hence I --> i is Function of I,{i} by FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; end; definition let B be non empty set ; let A be set ; let b be Element of B; :: original: --> redefine funcA --> b -> Function of A,B; coherence A --> b is Function of A,B by Th45; end; theorem :: FUNCOP_1:46 for A being set for X being non empty set for x being Element of X holds A --> x is Function of A,X ; theorem Th47: :: FUNCOP_1:47 for X being non empty set for Y being set for F being BinOp of X for f being Function of Y,X for x being Element of X holds F [:] (f,x) is Function of Y,X proof let X be non empty set ; ::_thesis: for Y being set for F being BinOp of X for f being Function of Y,X for x being Element of X holds F [:] (f,x) is Function of Y,X let Y be set ; ::_thesis: for F being BinOp of X for f being Function of Y,X for x being Element of X holds F [:] (f,x) is Function of Y,X let F be BinOp of X; ::_thesis: for f being Function of Y,X for x being Element of X holds F [:] (f,x) is Function of Y,X let f be Function of Y,X; ::_thesis: for x being Element of X holds F [:] (f,x) is Function of Y,X let x be Element of X; ::_thesis: F [:] (f,x) is Function of Y,X dom f = Y by FUNCT_2:def_1; then reconsider g = (dom f) --> x as Function of Y,X ; F * <:f,g:> is Function of Y,X ; hence F [:] (f,x) is Function of Y,X ; ::_thesis: verum end; definition let X be non empty set ; let Z be set ; let F be BinOp of X; let f be Function of Z,X; let x be Element of X; :: original: [:] redefine funcF [:] (f,x) -> Function of Z,X; coherence F [:] (f,x) is Function of Z,X by Th47; end; theorem Th48: :: FUNCOP_1:48 for X, Y being non empty set for F being BinOp of X for f being Function of Y,X for x being Element of X for y being Element of Y holds (F [:] (f,x)) . y = F . ((f . y),x) proof let X, Y be non empty set ; ::_thesis: for F being BinOp of X for f being Function of Y,X for x being Element of X for y being Element of Y holds (F [:] (f,x)) . y = F . ((f . y),x) let F be BinOp of X; ::_thesis: for f being Function of Y,X for x being Element of X for y being Element of Y holds (F [:] (f,x)) . y = F . ((f . y),x) let f be Function of Y,X; ::_thesis: for x being Element of X for y being Element of Y holds (F [:] (f,x)) . y = F . ((f . y),x) let x be Element of X; ::_thesis: for y being Element of Y holds (F [:] (f,x)) . y = F . ((f . y),x) let y be Element of Y; ::_thesis: (F [:] (f,x)) . y = F . ((f . y),x) dom (F [:] (f,x)) = Y by FUNCT_2:def_1; hence (F [:] (f,x)) . y = F . ((f . y),x) by Th27; ::_thesis: verum end; theorem Th49: :: FUNCOP_1:49 for X, Y being non empty set for F being BinOp of X for g, f being Function of Y,X for x being Element of X st ( for y being Element of Y holds g . y = F . ((f . y),x) ) holds g = F [:] (f,x) proof let X, Y be non empty set ; ::_thesis: for F being BinOp of X for g, f being Function of Y,X for x being Element of X st ( for y being Element of Y holds g . y = F . ((f . y),x) ) holds g = F [:] (f,x) let F be BinOp of X; ::_thesis: for g, f being Function of Y,X for x being Element of X st ( for y being Element of Y holds g . y = F . ((f . y),x) ) holds g = F [:] (f,x) let g, f be Function of Y,X; ::_thesis: for x being Element of X st ( for y being Element of Y holds g . y = F . ((f . y),x) ) holds g = F [:] (f,x) let x be Element of X; ::_thesis: ( ( for y being Element of Y holds g . y = F . ((f . y),x) ) implies g = F [:] (f,x) ) assume A1: for y being Element of Y holds g . y = F . ((f . y),x) ; ::_thesis: g = F [:] (f,x) now__::_thesis:_for_y_being_Element_of_Y_holds_g_._y_=_(F_[:]_(f,x))_._y let y be Element of Y; ::_thesis: g . y = (F [:] (f,x)) . y thus g . y = F . ((f . y),x) by A1 .= (F [:] (f,x)) . y by Th48 ; ::_thesis: verum end; hence g = F [:] (f,x) by FUNCT_2:63; ::_thesis: verum end; theorem :: FUNCOP_1:50 for X, Y being non empty set for F being BinOp of X for f being Function of Y,X for x being Element of X holds (F [:] ((id X),x)) * f = F [:] (f,x) proof let X, Y be non empty set ; ::_thesis: for F being BinOp of X for f being Function of Y,X for x being Element of X holds (F [:] ((id X),x)) * f = F [:] (f,x) let F be BinOp of X; ::_thesis: for f being Function of Y,X for x being Element of X holds (F [:] ((id X),x)) * f = F [:] (f,x) let f be Function of Y,X; ::_thesis: for x being Element of X holds (F [:] ((id X),x)) * f = F [:] (f,x) let x be Element of X; ::_thesis: (F [:] ((id X),x)) * f = F [:] (f,x) thus (F [:] ((id X),x)) * f = F [:] (((id X) * f),x) by Th29 .= F [:] (f,x) by FUNCT_2:17 ; ::_thesis: verum end; theorem :: FUNCOP_1:51 for X being non empty set for F being BinOp of X for x being Element of X holds (F [:] ((id X),x)) . x = F . (x,x) proof let X be non empty set ; ::_thesis: for F being BinOp of X for x being Element of X holds (F [:] ((id X),x)) . x = F . (x,x) let F be BinOp of X; ::_thesis: for x being Element of X holds (F [:] ((id X),x)) . x = F . (x,x) let x be Element of X; ::_thesis: (F [:] ((id X),x)) . x = F . (x,x) thus (F [:] ((id X),x)) . x = F . (((id X) . x),x) by Th48 .= F . (x,x) by FUNCT_1:18 ; ::_thesis: verum end; theorem Th52: :: FUNCOP_1:52 for X being non empty set for Y being set for F being BinOp of X for g being Function of Y,X for x being Element of X holds F [;] (x,g) is Function of Y,X proof let X be non empty set ; ::_thesis: for Y being set for F being BinOp of X for g being Function of Y,X for x being Element of X holds F [;] (x,g) is Function of Y,X let Y be set ; ::_thesis: for F being BinOp of X for g being Function of Y,X for x being Element of X holds F [;] (x,g) is Function of Y,X let F be BinOp of X; ::_thesis: for g being Function of Y,X for x being Element of X holds F [;] (x,g) is Function of Y,X let g be Function of Y,X; ::_thesis: for x being Element of X holds F [;] (x,g) is Function of Y,X let x be Element of X; ::_thesis: F [;] (x,g) is Function of Y,X dom g = Y by FUNCT_2:def_1; then reconsider f = (dom g) --> x as Function of Y,X ; F * <:f,g:> is Function of Y,X ; hence F [;] (x,g) is Function of Y,X ; ::_thesis: verum end; definition let X be non empty set ; let Z be set ; let F be BinOp of X; let x be Element of X; let g be Function of Z,X; :: original: [;] redefine funcF [;] (x,g) -> Function of Z,X; coherence F [;] (x,g) is Function of Z,X by Th52; end; theorem Th53: :: FUNCOP_1:53 for X, Y being non empty set for F being BinOp of X for f being Function of Y,X for x being Element of X for y being Element of Y holds (F [;] (x,f)) . y = F . (x,(f . y)) proof let X, Y be non empty set ; ::_thesis: for F being BinOp of X for f being Function of Y,X for x being Element of X for y being Element of Y holds (F [;] (x,f)) . y = F . (x,(f . y)) let F be BinOp of X; ::_thesis: for f being Function of Y,X for x being Element of X for y being Element of Y holds (F [;] (x,f)) . y = F . (x,(f . y)) let f be Function of Y,X; ::_thesis: for x being Element of X for y being Element of Y holds (F [;] (x,f)) . y = F . (x,(f . y)) let x be Element of X; ::_thesis: for y being Element of Y holds (F [;] (x,f)) . y = F . (x,(f . y)) let y be Element of Y; ::_thesis: (F [;] (x,f)) . y = F . (x,(f . y)) dom (F [;] (x,f)) = Y by FUNCT_2:def_1; hence (F [;] (x,f)) . y = F . (x,(f . y)) by Th32; ::_thesis: verum end; theorem Th54: :: FUNCOP_1:54 for X, Y being non empty set for F being BinOp of X for g, f being Function of Y,X for x being Element of X st ( for y being Element of Y holds g . y = F . (x,(f . y)) ) holds g = F [;] (x,f) proof let X, Y be non empty set ; ::_thesis: for F being BinOp of X for g, f being Function of Y,X for x being Element of X st ( for y being Element of Y holds g . y = F . (x,(f . y)) ) holds g = F [;] (x,f) let F be BinOp of X; ::_thesis: for g, f being Function of Y,X for x being Element of X st ( for y being Element of Y holds g . y = F . (x,(f . y)) ) holds g = F [;] (x,f) let g, f be Function of Y,X; ::_thesis: for x being Element of X st ( for y being Element of Y holds g . y = F . (x,(f . y)) ) holds g = F [;] (x,f) let x be Element of X; ::_thesis: ( ( for y being Element of Y holds g . y = F . (x,(f . y)) ) implies g = F [;] (x,f) ) assume A1: for y being Element of Y holds g . y = F . (x,(f . y)) ; ::_thesis: g = F [;] (x,f) now__::_thesis:_for_y_being_Element_of_Y_holds_g_._y_=_(F_[;]_(x,f))_._y let y be Element of Y; ::_thesis: g . y = (F [;] (x,f)) . y thus g . y = F . (x,(f . y)) by A1 .= (F [;] (x,f)) . y by Th53 ; ::_thesis: verum end; hence g = F [;] (x,f) by FUNCT_2:63; ::_thesis: verum end; theorem :: FUNCOP_1:55 for X being non empty set for Y being set for F being BinOp of X for f being Function of Y,X for x being Element of X holds (F [;] (x,(id X))) * f = F [;] (x,f) proof let X be non empty set ; ::_thesis: for Y being set for F being BinOp of X for f being Function of Y,X for x being Element of X holds (F [;] (x,(id X))) * f = F [;] (x,f) let Y be set ; ::_thesis: for F being BinOp of X for f being Function of Y,X for x being Element of X holds (F [;] (x,(id X))) * f = F [;] (x,f) let F be BinOp of X; ::_thesis: for f being Function of Y,X for x being Element of X holds (F [;] (x,(id X))) * f = F [;] (x,f) let f be Function of Y,X; ::_thesis: for x being Element of X holds (F [;] (x,(id X))) * f = F [;] (x,f) let x be Element of X; ::_thesis: (F [;] (x,(id X))) * f = F [;] (x,f) thus (F [;] (x,(id X))) * f = F [;] (x,((id X) * f)) by Th34 .= F [;] (x,f) by FUNCT_2:17 ; ::_thesis: verum end; theorem :: FUNCOP_1:56 for X being non empty set for F being BinOp of X for x being Element of X holds (F [;] (x,(id X))) . x = F . (x,x) proof let X be non empty set ; ::_thesis: for F being BinOp of X for x being Element of X holds (F [;] (x,(id X))) . x = F . (x,x) let F be BinOp of X; ::_thesis: for x being Element of X holds (F [;] (x,(id X))) . x = F . (x,x) let x be Element of X; ::_thesis: (F [;] (x,(id X))) . x = F . (x,x) thus (F [;] (x,(id X))) . x = F . (x,((id X) . x)) by Th53 .= F . (x,x) by FUNCT_1:18 ; ::_thesis: verum end; theorem :: FUNCOP_1:57 for X, Y, Z being non empty set for f being Function of X,[:Y,Z:] for x being Element of X holds (f ~) . x = [((f . x) `2),((f . x) `1)] proof let X, Y, Z be non empty set ; ::_thesis: for f being Function of X,[:Y,Z:] for x being Element of X holds (f ~) . x = [((f . x) `2),((f . x) `1)] let f be Function of X,[:Y,Z:]; ::_thesis: for x being Element of X holds (f ~) . x = [((f . x) `2),((f . x) `1)] let x be Element of X; ::_thesis: (f ~) . x = [((f . x) `2),((f . x) `1)] x in X ; then A1: x in dom f by FUNCT_2:def_1; f . x = [((f . x) `1),((f . x) `2)] by MCART_1:22; hence (f ~) . x = [((f . x) `2),((f . x) `1)] by A1, Def1; ::_thesis: verum end; definition let X, Y, Z be non empty set ; let f be Function of X,[:Y,Z:]; :: original: proj2 redefine func rng f -> Relation of Y,Z; coherence proj2 f is Relation of Y,Z by RELAT_1:def_19; end; definition let X, Y, Z be non empty set ; let f be Function of X,[:Y,Z:]; :: original: ~ redefine funcf ~ -> Function of X,[:Z,Y:]; coherence f ~ is Function of X,[:Z,Y:] proof A1: rng (f ~) c= [:Z,Y:] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (f ~) or x in [:Z,Y:] ) assume x in rng (f ~) ; ::_thesis: x in [:Z,Y:] then consider y being set such that A2: y in dom (f ~) and A3: x = (f ~) . y by FUNCT_1:def_3; A4: y in dom f by A2, Def1; then reconsider y = y as Element of X ; A5: f . y = [((f . y) `1),((f . y) `2)] by MCART_1:21; then (f ~) . y = [((f . y) `2),((f . y) `1)] by A4, Def1; hence x in [:Z,Y:] by A3, A5, ZFMISC_1:88; ::_thesis: verum end; X = dom f by FUNCT_2:def_1 .= dom (f ~) by Def1 ; hence f ~ is Function of X,[:Z,Y:] by A1, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; end; theorem :: FUNCOP_1:58 for X, Y, Z being non empty set for f being Function of X,[:Y,Z:] holds rng (f ~) = (rng f) ~ proof let X, Y, Z be non empty set ; ::_thesis: for f being Function of X,[:Y,Z:] holds rng (f ~) = (rng f) ~ let f be Function of X,[:Y,Z:]; ::_thesis: rng (f ~) = (rng f) ~ let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in rng (f ~) or [x,y] in (rng f) ~ ) & ( not [x,y] in (rng f) ~ or [x,y] in rng (f ~) ) ) thus ( [x,y] in rng (f ~) implies [x,y] in (rng f) ~ ) ::_thesis: ( not [x,y] in (rng f) ~ or [x,y] in rng (f ~) ) proof assume [x,y] in rng (f ~) ; ::_thesis: [x,y] in (rng f) ~ then consider z being set such that A1: z in dom (f ~) and A2: [x,y] = (f ~) . z by FUNCT_1:def_3; A3: z in dom f by A1, Def1; f . z = ((f ~) ~) . z .= [y,x] by A1, A2, Def1 ; then [y,x] in rng f by A3, FUNCT_1:def_3; hence [x,y] in (rng f) ~ by RELAT_1:def_7; ::_thesis: verum end; assume [x,y] in (rng f) ~ ; ::_thesis: [x,y] in rng (f ~) then [y,x] in rng f by RELAT_1:def_7; then consider z being set such that A4: ( z in dom f & [y,x] = f . z ) by FUNCT_1:def_3; ( z in dom (f ~) & (f ~) . z = [x,y] ) by A4, Def1; hence [x,y] in rng (f ~) by FUNCT_1:def_3; ::_thesis: verum end; theorem :: FUNCOP_1:59 for X being non empty set for Y being set for F being BinOp of X for f being Function of Y,X for x1, x2 being Element of X st F is associative holds F [:] ((F [;] (x1,f)),x2) = F [;] (x1,(F [:] (f,x2))) proof let X be non empty set ; ::_thesis: for Y being set for F being BinOp of X for f being Function of Y,X for x1, x2 being Element of X st F is associative holds F [:] ((F [;] (x1,f)),x2) = F [;] (x1,(F [:] (f,x2))) let Y be set ; ::_thesis: for F being BinOp of X for f being Function of Y,X for x1, x2 being Element of X st F is associative holds F [:] ((F [;] (x1,f)),x2) = F [;] (x1,(F [:] (f,x2))) let F be BinOp of X; ::_thesis: for f being Function of Y,X for x1, x2 being Element of X st F is associative holds F [:] ((F [;] (x1,f)),x2) = F [;] (x1,(F [:] (f,x2))) let f be Function of Y,X; ::_thesis: for x1, x2 being Element of X st F is associative holds F [:] ((F [;] (x1,f)),x2) = F [;] (x1,(F [:] (f,x2))) let x1, x2 be Element of X; ::_thesis: ( F is associative implies F [:] ((F [;] (x1,f)),x2) = F [;] (x1,(F [:] (f,x2))) ) assume A1: F is associative ; ::_thesis: F [:] ((F [;] (x1,f)),x2) = F [;] (x1,(F [:] (f,x2))) percases ( Y = {} or Y <> {} ) ; suppose Y = {} ; ::_thesis: F [:] ((F [;] (x1,f)),x2) = F [;] (x1,(F [:] (f,x2))) hence F [:] ((F [;] (x1,f)),x2) = F [;] (x1,(F [:] (f,x2))) ; ::_thesis: verum end; supposeA2: Y <> {} ; ::_thesis: F [:] ((F [;] (x1,f)),x2) = F [;] (x1,(F [:] (f,x2))) now__::_thesis:_for_y_being_Element_of_Y_holds_(F_[:]_((F_[;]_(x1,f)),x2))_._y_=_F_._(x1,((F_[:]_(f,x2))_._y)) let y be Element of Y; ::_thesis: (F [:] ((F [;] (x1,f)),x2)) . y = F . (x1,((F [:] (f,x2)) . y)) reconsider x3 = f . y as Element of X by A2, FUNCT_2:5; thus (F [:] ((F [;] (x1,f)),x2)) . y = F . (((F [;] (x1,f)) . y),x2) by A2, Th48 .= F . ((F . (x1,x3)),x2) by A2, Th53 .= F . (x1,(F . (x3,x2))) by A1, BINOP_1:def_3 .= F . (x1,((F [:] (f,x2)) . y)) by A2, Th48 ; ::_thesis: verum end; hence F [:] ((F [;] (x1,f)),x2) = F [;] (x1,(F [:] (f,x2))) by A2, Th54; ::_thesis: verum end; end; end; theorem :: FUNCOP_1:60 for X being non empty set for Y being set for F being BinOp of X for f, g being Function of Y,X for x being Element of X st F is associative holds F .: ((F [:] (f,x)),g) = F .: (f,(F [;] (x,g))) proof let X be non empty set ; ::_thesis: for Y being set for F being BinOp of X for f, g being Function of Y,X for x being Element of X st F is associative holds F .: ((F [:] (f,x)),g) = F .: (f,(F [;] (x,g))) let Y be set ; ::_thesis: for F being BinOp of X for f, g being Function of Y,X for x being Element of X st F is associative holds F .: ((F [:] (f,x)),g) = F .: (f,(F [;] (x,g))) let F be BinOp of X; ::_thesis: for f, g being Function of Y,X for x being Element of X st F is associative holds F .: ((F [:] (f,x)),g) = F .: (f,(F [;] (x,g))) let f, g be Function of Y,X; ::_thesis: for x being Element of X st F is associative holds F .: ((F [:] (f,x)),g) = F .: (f,(F [;] (x,g))) let x be Element of X; ::_thesis: ( F is associative implies F .: ((F [:] (f,x)),g) = F .: (f,(F [;] (x,g))) ) assume A1: F is associative ; ::_thesis: F .: ((F [:] (f,x)),g) = F .: (f,(F [;] (x,g))) percases ( Y = {} or Y <> {} ) ; suppose Y = {} ; ::_thesis: F .: ((F [:] (f,x)),g) = F .: (f,(F [;] (x,g))) hence F .: ((F [:] (f,x)),g) = F .: (f,(F [;] (x,g))) ; ::_thesis: verum end; supposeA2: Y <> {} ; ::_thesis: F .: ((F [:] (f,x)),g) = F .: (f,(F [;] (x,g))) now__::_thesis:_for_y_being_Element_of_Y_holds_(F_.:_((F_[:]_(f,x)),g))_._y_=_F_._((f_._y),((F_[;]_(x,g))_._y)) let y be Element of Y; ::_thesis: (F .: ((F [:] (f,x)),g)) . y = F . ((f . y),((F [;] (x,g)) . y)) reconsider x1 = f . y, x2 = g . y as Element of X by A2, FUNCT_2:5; thus (F .: ((F [:] (f,x)),g)) . y = F . (((F [:] (f,x)) . y),(g . y)) by A2, Th37 .= F . ((F . (x1,x)),x2) by A2, Th48 .= F . (x1,(F . (x,x2))) by A1, BINOP_1:def_3 .= F . ((f . y),((F [;] (x,g)) . y)) by A2, Th53 ; ::_thesis: verum end; hence F .: ((F [:] (f,x)),g) = F .: (f,(F [;] (x,g))) by A2, Th38; ::_thesis: verum end; end; end; theorem :: FUNCOP_1:61 for X being non empty set for Y being set for F being BinOp of X for f, g, h being Function of Y,X st F is associative holds F .: ((F .: (f,g)),h) = F .: (f,(F .: (g,h))) proof let X be non empty set ; ::_thesis: for Y being set for F being BinOp of X for f, g, h being Function of Y,X st F is associative holds F .: ((F .: (f,g)),h) = F .: (f,(F .: (g,h))) let Y be set ; ::_thesis: for F being BinOp of X for f, g, h being Function of Y,X st F is associative holds F .: ((F .: (f,g)),h) = F .: (f,(F .: (g,h))) let F be BinOp of X; ::_thesis: for f, g, h being Function of Y,X st F is associative holds F .: ((F .: (f,g)),h) = F .: (f,(F .: (g,h))) let f, g, h be Function of Y,X; ::_thesis: ( F is associative implies F .: ((F .: (f,g)),h) = F .: (f,(F .: (g,h))) ) assume A1: F is associative ; ::_thesis: F .: ((F .: (f,g)),h) = F .: (f,(F .: (g,h))) percases ( Y = {} or Y <> {} ) ; suppose Y = {} ; ::_thesis: F .: ((F .: (f,g)),h) = F .: (f,(F .: (g,h))) hence F .: ((F .: (f,g)),h) = F .: (f,(F .: (g,h))) ; ::_thesis: verum end; supposeA2: Y <> {} ; ::_thesis: F .: ((F .: (f,g)),h) = F .: (f,(F .: (g,h))) now__::_thesis:_for_y_being_Element_of_Y_holds_(F_.:_((F_.:_(f,g)),h))_._y_=_F_._((f_._y),((F_.:_(g,h))_._y)) let y be Element of Y; ::_thesis: (F .: ((F .: (f,g)),h)) . y = F . ((f . y),((F .: (g,h)) . y)) reconsider x1 = f . y, x2 = g . y, x3 = h . y as Element of X by A2, FUNCT_2:5; thus (F .: ((F .: (f,g)),h)) . y = F . (((F .: (f,g)) . y),(h . y)) by A2, Th37 .= F . ((F . ((f . y),(g . y))),(h . y)) by A2, Th37 .= F . (x1,(F . (x2,x3))) by A1, BINOP_1:def_3 .= F . ((f . y),((F .: (g,h)) . y)) by A2, Th37 ; ::_thesis: verum end; hence F .: ((F .: (f,g)),h) = F .: (f,(F .: (g,h))) by A2, Th38; ::_thesis: verum end; end; end; theorem :: FUNCOP_1:62 for X being non empty set for Y being set for F being BinOp of X for f being Function of Y,X for x1, x2 being Element of X st F is associative holds F [;] ((F . (x1,x2)),f) = F [;] (x1,(F [;] (x2,f))) proof let X be non empty set ; ::_thesis: for Y being set for F being BinOp of X for f being Function of Y,X for x1, x2 being Element of X st F is associative holds F [;] ((F . (x1,x2)),f) = F [;] (x1,(F [;] (x2,f))) let Y be set ; ::_thesis: for F being BinOp of X for f being Function of Y,X for x1, x2 being Element of X st F is associative holds F [;] ((F . (x1,x2)),f) = F [;] (x1,(F [;] (x2,f))) let F be BinOp of X; ::_thesis: for f being Function of Y,X for x1, x2 being Element of X st F is associative holds F [;] ((F . (x1,x2)),f) = F [;] (x1,(F [;] (x2,f))) let f be Function of Y,X; ::_thesis: for x1, x2 being Element of X st F is associative holds F [;] ((F . (x1,x2)),f) = F [;] (x1,(F [;] (x2,f))) let x1, x2 be Element of X; ::_thesis: ( F is associative implies F [;] ((F . (x1,x2)),f) = F [;] (x1,(F [;] (x2,f))) ) assume A1: F is associative ; ::_thesis: F [;] ((F . (x1,x2)),f) = F [;] (x1,(F [;] (x2,f))) percases ( Y = {} or Y <> {} ) ; suppose Y = {} ; ::_thesis: F [;] ((F . (x1,x2)),f) = F [;] (x1,(F [;] (x2,f))) hence F [;] ((F . (x1,x2)),f) = F [;] (x1,(F [;] (x2,f))) ; ::_thesis: verum end; supposeA2: Y <> {} ; ::_thesis: F [;] ((F . (x1,x2)),f) = F [;] (x1,(F [;] (x2,f))) now__::_thesis:_for_y_being_Element_of_Y_holds_(F_[;]_((F_._(x1,x2)),f))_._y_=_F_._(x1,((F_[;]_(x2,f))_._y)) let y be Element of Y; ::_thesis: (F [;] ((F . (x1,x2)),f)) . y = F . (x1,((F [;] (x2,f)) . y)) reconsider x3 = f . y as Element of X by A2, FUNCT_2:5; thus (F [;] ((F . (x1,x2)),f)) . y = F . ((F . (x1,x2)),(f . y)) by A2, Th53 .= F . (x1,(F . (x2,x3))) by A1, BINOP_1:def_3 .= F . (x1,((F [;] (x2,f)) . y)) by A2, Th53 ; ::_thesis: verum end; hence F [;] ((F . (x1,x2)),f) = F [;] (x1,(F [;] (x2,f))) by A2, Th54; ::_thesis: verum end; end; end; theorem :: FUNCOP_1:63 for X being non empty set for Y being set for F being BinOp of X for f being Function of Y,X for x1, x2 being Element of X st F is associative holds F [:] (f,(F . (x1,x2))) = F [:] ((F [:] (f,x1)),x2) proof let X be non empty set ; ::_thesis: for Y being set for F being BinOp of X for f being Function of Y,X for x1, x2 being Element of X st F is associative holds F [:] (f,(F . (x1,x2))) = F [:] ((F [:] (f,x1)),x2) let Y be set ; ::_thesis: for F being BinOp of X for f being Function of Y,X for x1, x2 being Element of X st F is associative holds F [:] (f,(F . (x1,x2))) = F [:] ((F [:] (f,x1)),x2) let F be BinOp of X; ::_thesis: for f being Function of Y,X for x1, x2 being Element of X st F is associative holds F [:] (f,(F . (x1,x2))) = F [:] ((F [:] (f,x1)),x2) let f be Function of Y,X; ::_thesis: for x1, x2 being Element of X st F is associative holds F [:] (f,(F . (x1,x2))) = F [:] ((F [:] (f,x1)),x2) let x1, x2 be Element of X; ::_thesis: ( F is associative implies F [:] (f,(F . (x1,x2))) = F [:] ((F [:] (f,x1)),x2) ) assume A1: F is associative ; ::_thesis: F [:] (f,(F . (x1,x2))) = F [:] ((F [:] (f,x1)),x2) percases ( Y = {} or Y <> {} ) ; suppose Y = {} ; ::_thesis: F [:] (f,(F . (x1,x2))) = F [:] ((F [:] (f,x1)),x2) hence F [:] (f,(F . (x1,x2))) = F [:] ((F [:] (f,x1)),x2) ; ::_thesis: verum end; supposeA2: Y <> {} ; ::_thesis: F [:] (f,(F . (x1,x2))) = F [:] ((F [:] (f,x1)),x2) now__::_thesis:_for_y_being_Element_of_Y_holds_(F_[:]_(f,(F_._(x1,x2))))_._y_=_F_._(((F_[:]_(f,x1))_._y),x2) let y be Element of Y; ::_thesis: (F [:] (f,(F . (x1,x2)))) . y = F . (((F [:] (f,x1)) . y),x2) reconsider x3 = f . y as Element of X by A2, FUNCT_2:5; thus (F [:] (f,(F . (x1,x2)))) . y = F . ((f . y),(F . (x1,x2))) by A2, Th48 .= F . ((F . (x3,x1)),x2) by A1, BINOP_1:def_3 .= F . (((F [:] (f,x1)) . y),x2) by A2, Th48 ; ::_thesis: verum end; hence F [:] (f,(F . (x1,x2))) = F [:] ((F [:] (f,x1)),x2) by A2, Th49; ::_thesis: verum end; end; end; theorem :: FUNCOP_1:64 for X being non empty set for Y being set for F being BinOp of X for f being Function of Y,X for x being Element of X st F is commutative holds F [;] (x,f) = F [:] (f,x) proof let X be non empty set ; ::_thesis: for Y being set for F being BinOp of X for f being Function of Y,X for x being Element of X st F is commutative holds F [;] (x,f) = F [:] (f,x) let Y be set ; ::_thesis: for F being BinOp of X for f being Function of Y,X for x being Element of X st F is commutative holds F [;] (x,f) = F [:] (f,x) let F be BinOp of X; ::_thesis: for f being Function of Y,X for x being Element of X st F is commutative holds F [;] (x,f) = F [:] (f,x) let f be Function of Y,X; ::_thesis: for x being Element of X st F is commutative holds F [;] (x,f) = F [:] (f,x) let x be Element of X; ::_thesis: ( F is commutative implies F [;] (x,f) = F [:] (f,x) ) assume A1: F is commutative ; ::_thesis: F [;] (x,f) = F [:] (f,x) percases ( Y = {} or Y <> {} ) ; suppose Y = {} ; ::_thesis: F [;] (x,f) = F [:] (f,x) hence F [;] (x,f) = F [:] (f,x) ; ::_thesis: verum end; supposeA2: Y <> {} ; ::_thesis: F [;] (x,f) = F [:] (f,x) now__::_thesis:_for_y_being_Element_of_Y_holds_(F_[;]_(x,f))_._y_=_F_._((f_._y),x) let y be Element of Y; ::_thesis: (F [;] (x,f)) . y = F . ((f . y),x) reconsider x1 = f . y as Element of X by A2, FUNCT_2:5; thus (F [;] (x,f)) . y = F . (x,x1) by A2, Th53 .= F . ((f . y),x) by A1, BINOP_1:def_2 ; ::_thesis: verum end; hence F [;] (x,f) = F [:] (f,x) by A2, Th49; ::_thesis: verum end; end; end; theorem :: FUNCOP_1:65 for X being non empty set for Y being set for F being BinOp of X for f, g being Function of Y,X st F is commutative holds F .: (f,g) = F .: (g,f) proof let X be non empty set ; ::_thesis: for Y being set for F being BinOp of X for f, g being Function of Y,X st F is commutative holds F .: (f,g) = F .: (g,f) let Y be set ; ::_thesis: for F being BinOp of X for f, g being Function of Y,X st F is commutative holds F .: (f,g) = F .: (g,f) let F be BinOp of X; ::_thesis: for f, g being Function of Y,X st F is commutative holds F .: (f,g) = F .: (g,f) let f, g be Function of Y,X; ::_thesis: ( F is commutative implies F .: (f,g) = F .: (g,f) ) assume A1: F is commutative ; ::_thesis: F .: (f,g) = F .: (g,f) percases ( Y = {} or Y <> {} ) ; suppose Y = {} ; ::_thesis: F .: (f,g) = F .: (g,f) hence F .: (f,g) = F .: (g,f) ; ::_thesis: verum end; supposeA2: Y <> {} ; ::_thesis: F .: (f,g) = F .: (g,f) now__::_thesis:_for_y_being_Element_of_Y_holds_(F_.:_(f,g))_._y_=_F_._((g_._y),(f_._y)) let y be Element of Y; ::_thesis: (F .: (f,g)) . y = F . ((g . y),(f . y)) reconsider x1 = f . y, x2 = g . y as Element of X by A2, FUNCT_2:5; thus (F .: (f,g)) . y = F . (x1,x2) by A2, Th37 .= F . ((g . y),(f . y)) by A1, BINOP_1:def_2 ; ::_thesis: verum end; hence F .: (f,g) = F .: (g,f) by A2, Th38; ::_thesis: verum end; end; end; theorem :: FUNCOP_1:66 for X being non empty set for Y being set for F being BinOp of X for f being Function of Y,X st F is idempotent holds F .: (f,f) = f proof let X be non empty set ; ::_thesis: for Y being set for F being BinOp of X for f being Function of Y,X st F is idempotent holds F .: (f,f) = f let Y be set ; ::_thesis: for F being BinOp of X for f being Function of Y,X st F is idempotent holds F .: (f,f) = f let F be BinOp of X; ::_thesis: for f being Function of Y,X st F is idempotent holds F .: (f,f) = f let f be Function of Y,X; ::_thesis: ( F is idempotent implies F .: (f,f) = f ) assume A1: F is idempotent ; ::_thesis: F .: (f,f) = f percases ( Y = {} or Y <> {} ) ; supposeA2: Y = {} ; ::_thesis: F .: (f,f) = f hence F .: (f,f) = {} .= f by A2 ; ::_thesis: verum end; supposeA3: Y <> {} ; ::_thesis: F .: (f,f) = f now__::_thesis:_for_y_being_Element_of_Y_holds_f_._y_=_F_._((f_._y),(f_._y)) let y be Element of Y; ::_thesis: f . y = F . ((f . y),(f . y)) reconsider x = f . y as Element of X by A3, FUNCT_2:5; thus f . y = F . (x,x) by A1 .= F . ((f . y),(f . y)) ; ::_thesis: verum end; hence F .: (f,f) = f by A3, Th38; ::_thesis: verum end; end; end; theorem :: FUNCOP_1:67 for X, Y being non empty set for F being BinOp of X for f being Function of Y,X for y being Element of Y st F is idempotent holds (F [;] ((f . y),f)) . y = f . y proof let X, Y be non empty set ; ::_thesis: for F being BinOp of X for f being Function of Y,X for y being Element of Y st F is idempotent holds (F [;] ((f . y),f)) . y = f . y let F be BinOp of X; ::_thesis: for f being Function of Y,X for y being Element of Y st F is idempotent holds (F [;] ((f . y),f)) . y = f . y let f be Function of Y,X; ::_thesis: for y being Element of Y st F is idempotent holds (F [;] ((f . y),f)) . y = f . y let y be Element of Y; ::_thesis: ( F is idempotent implies (F [;] ((f . y),f)) . y = f . y ) assume A1: F is idempotent ; ::_thesis: (F [;] ((f . y),f)) . y = f . y thus (F [;] ((f . y),f)) . y = F . ((f . y),(f . y)) by Th53 .= f . y by A1 ; ::_thesis: verum end; theorem :: FUNCOP_1:68 for X, Y being non empty set for F being BinOp of X for f being Function of Y,X for y being Element of Y st F is idempotent holds (F [:] (f,(f . y))) . y = f . y proof let X, Y be non empty set ; ::_thesis: for F being BinOp of X for f being Function of Y,X for y being Element of Y st F is idempotent holds (F [:] (f,(f . y))) . y = f . y let F be BinOp of X; ::_thesis: for f being Function of Y,X for y being Element of Y st F is idempotent holds (F [:] (f,(f . y))) . y = f . y let f be Function of Y,X; ::_thesis: for y being Element of Y st F is idempotent holds (F [:] (f,(f . y))) . y = f . y let y be Element of Y; ::_thesis: ( F is idempotent implies (F [:] (f,(f . y))) . y = f . y ) assume A1: F is idempotent ; ::_thesis: (F [:] (f,(f . y))) . y = f . y thus (F [:] (f,(f . y))) . y = F . ((f . y),(f . y)) by Th48 .= f . y by A1 ; ::_thesis: verum end; theorem :: FUNCOP_1:69 for F, f, g being Function st [:(rng f),(rng g):] c= dom F holds dom (F .: (f,g)) = (dom f) /\ (dom g) proof let F, f, g be Function; ::_thesis: ( [:(rng f),(rng g):] c= dom F implies dom (F .: (f,g)) = (dom f) /\ (dom g) ) assume A1: [:(rng f),(rng g):] c= dom F ; ::_thesis: dom (F .: (f,g)) = (dom f) /\ (dom g) rng <:f,g:> c= [:(rng f),(rng g):] by FUNCT_3:51; hence dom (F .: (f,g)) = dom <:f,g:> by A1, RELAT_1:27, XBOOLE_1:1 .= (dom f) /\ (dom g) by FUNCT_3:def_7 ; ::_thesis: verum end; definition let IT be Function; attrIT is Function-yielding means :Def6: :: FUNCOP_1:def 6 for x being set st x in dom IT holds IT . x is Function; end; :: deftheorem Def6 defines Function-yielding FUNCOP_1:def_6_:_ for IT being Function holds ( IT is Function-yielding iff for x being set st x in dom IT holds IT . x is Function ); registration cluster Relation-like Function-like Function-yielding for set ; existence ex b1 being Function st b1 is Function-yielding proof take the set --> the Function ; ::_thesis: the set --> the Function is Function-yielding let x be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( x in dom ( the set --> the Function) implies ( the set --> the Function) . x is Function ) thus ( x in dom ( the set --> the Function) implies ( the set --> the Function) . x is Function ) ; ::_thesis: verum end; end; registration let B be Function-yielding Function; let j be set ; clusterB . j -> Relation-like Function-like ; coherence ( B . j is Function-like & B . j is Relation-like ) proof percases ( j in dom B or not j in dom B ) ; suppose j in dom B ; ::_thesis: ( B . j is Function-like & B . j is Relation-like ) hence ( B . j is Function-like & B . j is Relation-like ) by Def6; ::_thesis: verum end; suppose not j in dom B ; ::_thesis: ( B . j is Function-like & B . j is Relation-like ) hence ( B . j is Function-like & B . j is Relation-like ) by FUNCT_1:def_2; ::_thesis: verum end; end; end; end; registration let F be Function-yielding Function; let f be Function; clusterf * F -> Function-yielding ; coherence F * f is Function-yielding proof thus F * f is Function-yielding ::_thesis: verum proof let x be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( x in dom (F * f) implies (F * f) . x is Function ) assume x in dom (F * f) ; ::_thesis: (F * f) . x is Function then (F * f) . x = F . (f . x) by FUNCT_1:12; hence (F * f) . x is Function ; ::_thesis: verum end; end; end; registration let B be set ; let c be non empty set ; clusterB --> c -> non-empty ; coherence B --> c is non-empty proof not {} in rng (B --> c) by TARSKI:def_1; hence B --> c is non-empty by RELAT_1:def_9; ::_thesis: verum end; end; theorem :: FUNCOP_1:70 for z being set for X, Y being non empty set for x being Element of X for y being Element of Y holds ([:X,Y:] --> z) . (x,y) = z proof let z be set ; ::_thesis: for X, Y being non empty set for x being Element of X for y being Element of Y holds ([:X,Y:] --> z) . (x,y) = z let X, Y be non empty set ; ::_thesis: for x being Element of X for y being Element of Y holds ([:X,Y:] --> z) . (x,y) = z let x be Element of X; ::_thesis: for y being Element of Y holds ([:X,Y:] --> z) . (x,y) = z let y be Element of Y; ::_thesis: ([:X,Y:] --> z) . (x,y) = z [x,y] in [:X,Y:] by ZFMISC_1:87; hence ([:X,Y:] --> z) . (x,y) = z by Th7; ::_thesis: verum end; definition let a, b, c be set ; func(a,b) .--> c -> Function equals :: FUNCOP_1:def 7 {[a,b]} --> c; coherence {[a,b]} --> c is Function ; end; :: deftheorem defines .--> FUNCOP_1:def_7_:_ for a, b, c being set holds (a,b) .--> c = {[a,b]} --> c; theorem :: FUNCOP_1:71 for a, b, c being set holds ((a,b) .--> c) . (a,b) = c proof let a, b, c be set ; ::_thesis: ((a,b) .--> c) . (a,b) = c [a,b] in {[a,b]} by TARSKI:def_1; hence ((a,b) .--> c) . (a,b) = c by Th7; ::_thesis: verum end; definition let x, y, a, b be set ; func IFEQ (x,y,a,b) -> set equals :Def8: :: FUNCOP_1:def 8 a if x = y otherwise b; correctness coherence ( ( x = y implies a is set ) & ( not x = y implies b is set ) ); consistency for b1 being set holds verum; ; end; :: deftheorem Def8 defines IFEQ FUNCOP_1:def_8_:_ for x, y, a, b being set holds ( ( x = y implies IFEQ (x,y,a,b) = a ) & ( not x = y implies IFEQ (x,y,a,b) = b ) ); definition let D be set ; let x, y be set ; let a, b be Element of D; :: original: IFEQ redefine func IFEQ (x,y,a,b) -> Element of D; coherence IFEQ (x,y,a,b) is Element of D proof ( x = y or x <> y ) ; hence IFEQ (x,y,a,b) is Element of D by Def8; ::_thesis: verum end; end; definition let x, y be set ; funcx .--> y -> set equals :: FUNCOP_1:def 9 {x} --> y; coherence {x} --> y is set ; end; :: deftheorem defines .--> FUNCOP_1:def_9_:_ for x, y being set holds x .--> y = {x} --> y; registration let x, y be set ; clusterx .--> y -> Relation-like Function-like ; coherence ( x .--> y is Function-like & x .--> y is Relation-like ) ; end; registration let x, y be set ; clusterx .--> y -> one-to-one ; coherence x .--> y is one-to-one proof let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in proj1 (x .--> y) or not x2 in proj1 (x .--> y) or not (x .--> y) . x1 = (x .--> y) . x2 or x1 = x2 ) set f = x .--> y; assume that A1: x1 in dom (x .--> y) and A2: x2 in dom (x .--> y) ; ::_thesis: ( not (x .--> y) . x1 = (x .--> y) . x2 or x1 = x2 ) A3: dom (x .--> y) = {x} by Th13; then x1 = x by A1, TARSKI:def_1; hence ( not (x .--> y) . x1 = (x .--> y) . x2 or x1 = x2 ) by A3, A2, TARSKI:def_1; ::_thesis: verum end; end; theorem Th72: :: FUNCOP_1:72 for x, y being set holds (x .--> y) . x = y proof let x, y be set ; ::_thesis: (x .--> y) . x = y x in {x} by TARSKI:def_1; hence (x .--> y) . x = y by Th7; ::_thesis: verum end; theorem :: FUNCOP_1:73 for a, b being set for f being Function holds ( a .--> b c= f iff ( a in dom f & f . a = b ) ) proof let a, b be set ; ::_thesis: for f being Function holds ( a .--> b c= f iff ( a in dom f & f . a = b ) ) let f be Function; ::_thesis: ( a .--> b c= f iff ( a in dom f & f . a = b ) ) A1: dom (a .--> b) = {a} by Th13; then A2: a in dom (a .--> b) by TARSKI:def_1; hereby ::_thesis: ( a in dom f & f . a = b implies a .--> b c= f ) assume A3: a .--> b c= f ; ::_thesis: ( a in dom f & f . a = b ) then {a} c= dom f by A1, GRFUNC_1:2; hence a in dom f by ZFMISC_1:31; ::_thesis: f . a = b thus f . a = (a .--> b) . a by A2, A3, GRFUNC_1:2 .= b by Th72 ; ::_thesis: verum end; assume that A4: a in dom f and A5: f . a = b ; ::_thesis: a .--> b c= f A6: now__::_thesis:_for_x_being_set_st_x_in_dom_(a_.-->_b)_holds_ (a_.-->_b)_._x_=_f_._x let x be set ; ::_thesis: ( x in dom (a .--> b) implies (a .--> b) . x = f . x ) assume x in dom (a .--> b) ; ::_thesis: (a .--> b) . x = f . x then x = a by A1, TARSKI:def_1; hence (a .--> b) . x = f . x by A5, Th72; ::_thesis: verum end; dom (a .--> b) c= dom f by A1, A4, ZFMISC_1:31; hence a .--> b c= f by A6, GRFUNC_1:2; ::_thesis: verum end; notation let o, m, r be set ; synonym (o,m) :-> r for (o,m) .--> r; end; Lm2: for o, m, r being set holds (o,m) :-> r is Function of [:{o},{m}:],{r} proof let o, m, r be set ; ::_thesis: (o,m) :-> r is Function of [:{o},{m}:],{r} dom ((o,m) :-> r) = {[o,m]} by Th13 .= [:{o},{m}:] by ZFMISC_1:29 ; hence (o,m) :-> r is Function of [:{o},{m}:],{r} by FUNCT_2:def_1; ::_thesis: verum end; definition let o, m, r be set ; :: original: .--> redefine func(o,m) :-> r -> Function of [:{o},{m}:],{r} means :: FUNCOP_1:def 10 verum; coherence (o,m) .--> r is Function of [:{o},{m}:],{r} by Lm2; compatibility for b1 being Function of [:{o},{m}:],{r} holds ( b1 = (o,m) .--> r iff verum ) proof let f be Function of [:{o},{m}:],{r}; ::_thesis: ( f = (o,m) .--> r iff verum ) (o,m) .--> r is Function of [:{o},{m}:],{r} by Lm2; hence ( f = (o,m) .--> r iff verum ) by FUNCT_2:51; ::_thesis: verum end; end; :: deftheorem defines :-> FUNCOP_1:def_10_:_ for o, m, r being set for b4 being Function of [:{o},{m}:],{r} holds ( b4 = (o,m) :-> r iff verum ); theorem :: FUNCOP_1:74 for x, y being set holds x in dom (x .--> y) proof let x, y be set ; ::_thesis: x in dom (x .--> y) dom (x .--> y) = {x} by Th13; hence x in dom (x .--> y) by TARSKI:def_1; ::_thesis: verum end; theorem :: FUNCOP_1:75 for z, x, y being set st z in dom (x .--> y) holds z = x proof let z, x, y be set ; ::_thesis: ( z in dom (x .--> y) implies z = x ) dom (x .--> y) = {x} by Th13; hence ( z in dom (x .--> y) implies z = x ) by TARSKI:def_1; ::_thesis: verum end; theorem :: FUNCOP_1:76 for A, x, y being set st not x in A holds (x .--> y) | A = {} proof let A, x, y be set ; ::_thesis: ( not x in A implies (x .--> y) | A = {} ) assume not x in A ; ::_thesis: (x .--> y) | A = {} then {x} misses A by ZFMISC_1:50; then dom (x .--> y) misses A by Th13; hence (x .--> y) | A = {} by RELAT_1:66; ::_thesis: verum end; notation let x, y be set ; synonym x :-> y for x .--> y; end; definition let m, o be set ; :: original: .--> redefine funcm :-> o -> Function of {m},{o}; coherence m .--> o is Function of {m},{o} ; end; theorem :: FUNCOP_1:77 for a, b, c being set for x being Element of {a} for y being Element of {b} holds ((a,b) :-> c) . (x,y) = c by TARSKI:def_1; registration let f be Function-yielding Function; let C be set ; clusterf | C -> Function-yielding ; coherence f | C is Function-yielding proof let i be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( i in dom (f | C) implies (f | C) . i is Function ) f . i is Function ; hence ( i in dom (f | C) implies (f | C) . i is Function ) by FUNCT_1:47; ::_thesis: verum end; end; registration let A be set ; let f be Function; clusterA --> f -> Function-yielding ; coherence A --> f is Function-yielding proof let a be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( a in dom (A --> f) implies (A --> f) . a is Function ) thus ( a in dom (A --> f) implies (A --> f) . a is Function ) ; ::_thesis: verum end; end; registration let X, a be set ; clusterX --> a -> constant ; coherence X --> a is constant proof let x, y be set ; :: according to FUNCT_1:def_10 ::_thesis: ( not x in proj1 (X --> a) or not y in proj1 (X --> a) or (X --> a) . x = (X --> a) . y ) assume that A1: x in dom (X --> a) and A2: y in dom (X --> a) ; ::_thesis: (X --> a) . x = (X --> a) . y thus (X --> a) . x = a by A1, Th7 .= (X --> a) . y by A2, Th7 ; ::_thesis: verum end; end; registration cluster Relation-like Function-like constant non empty for set ; existence ex b1 being Function st ( not b1 is empty & b1 is constant ) proof take {{}} --> {} ; ::_thesis: ( not {{}} --> {} is empty & {{}} --> {} is constant ) thus ( not {{}} --> {} is empty & {{}} --> {} is constant ) ; ::_thesis: verum end; end; registration let f be constant Function; let X be set ; clusterf | X -> constant ; coherence f | X is constant proof let x, y be set ; :: according to FUNCT_1:def_10 ::_thesis: ( not x in proj1 (f | X) or not y in proj1 (f | X) or (f | X) . x = (f | X) . y ) A1: dom (f | X) c= dom f by RELAT_1:60; assume that A2: x in dom (f | X) and A3: y in dom (f | X) ; ::_thesis: (f | X) . x = (f | X) . y thus (f | X) . x = f . x by A2, FUNCT_1:47 .= f . y by A1, A2, A3, FUNCT_1:def_10 .= (f | X) . y by A3, FUNCT_1:47 ; ::_thesis: verum end; end; theorem :: FUNCOP_1:78 for f being constant non empty Function ex y being set st for x being set st x in dom f holds f . x = y proof let f be constant non empty Function; ::_thesis: ex y being set st for x being set st x in dom f holds f . x = y consider y being set such that A1: y in rng f by XBOOLE_0:def_1; take y ; ::_thesis: for x being set st x in dom f holds f . x = y ex x0 being set st ( x0 in dom f & f . x0 = y ) by A1, FUNCT_1:def_3; hence for x being set st x in dom f holds f . x = y by FUNCT_1:def_10; ::_thesis: verum end; theorem :: FUNCOP_1:79 for X being non empty set for x being set holds the_value_of (X --> x) = x proof let X be non empty set ; ::_thesis: for x being set holds the_value_of (X --> x) = x let x be set ; ::_thesis: the_value_of (X --> x) = x set f = X --> x; ex i being set st ( i in dom (X --> x) & the_value_of (X --> x) = (X --> x) . i ) by FUNCT_1:def_12; hence the_value_of (X --> x) = x by Th7; ::_thesis: verum end; theorem :: FUNCOP_1:80 for f being constant Function holds f = (dom f) --> (the_value_of f) proof let f be constant Function; ::_thesis: f = (dom f) --> (the_value_of f) thus dom ((dom f) --> (the_value_of f)) = dom f by Th13; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds ( not b1 in proj1 f or f . b1 = ((dom f) --> (the_value_of f)) . b1 ) let x be set ; ::_thesis: ( not x in proj1 f or f . x = ((dom f) --> (the_value_of f)) . x ) assume A1: x in dom f ; ::_thesis: f . x = ((dom f) --> (the_value_of f)) . x then ( f <> {} & ((dom f) --> (the_value_of f)) . x = the_value_of f ) by Th7; hence f . x = ((dom f) --> (the_value_of f)) . x by A1, FUNCT_1:def_12; ::_thesis: verum end; registration let X be set ; let Y be non empty set ; cluster Relation-like X -defined Y -valued Function-like total for Element of bool [:X,Y:]; existence ex b1 being PartFunc of X,Y st b1 is total proof consider y being set such that A1: y in Y by XBOOLE_0:def_1; reconsider y = y as Element of Y by A1; take X --> y ; ::_thesis: X --> y is total thus X --> y is total ; ::_thesis: verum end; end; registration let I, A be set ; clusterI --> A -> I -defined ; coherence I --> A is I -defined ; end; registration let I, A be set ; clusterI .--> A -> {I} -defined ; coherence I .--> A is {I} -defined ; end; theorem :: FUNCOP_1:81 for A, B, x being set holds (A --> x) .: B c= {x} ; registration let I be set ; let f be Function; clusterI .--> f -> Function-yielding ; coherence I .--> f is Function-yielding ; end; registration let I be set ; cluster Relation-like non-empty I -defined Function-like total for set ; existence ex b1 being non-empty I -defined Function st b1 is total proof take I --> 1 ; ::_thesis: I --> 1 is total thus I --> 1 is total ; ::_thesis: verum end; end; theorem Th82: :: FUNCOP_1:82 for x, y being set holds x .--> y is_isomorphism_of {[x,x]},{[y,y]} proof let x, y be set ; ::_thesis: x .--> y is_isomorphism_of {[x,x]},{[y,y]} set F = x .--> y; set R = {[x,x]}; set S = {[y,y]}; A1: field {[x,x]} = {x} by RELAT_1:173; hence dom (x .--> y) = field {[x,x]} by Th13; :: according to WELLORD1:def_7 ::_thesis: ( proj2 (x .--> y) = field {[y,y]} & x .--> y is one-to-one & ( for b1, b2 being set holds ( ( not [b1,b2] in {[x,x]} or ( b1 in field {[x,x]} & b2 in field {[x,x]} & [((x .--> y) . b1),((x .--> y) . b2)] in {[y,y]} ) ) & ( not b1 in field {[x,x]} or not b2 in field {[x,x]} or not [((x .--> y) . b1),((x .--> y) . b2)] in {[y,y]} or [b1,b2] in {[x,x]} ) ) ) ) field {[y,y]} = {y} by RELAT_1:173; hence rng (x .--> y) = field {[y,y]} by RELAT_1:160; ::_thesis: ( x .--> y is one-to-one & ( for b1, b2 being set holds ( ( not [b1,b2] in {[x,x]} or ( b1 in field {[x,x]} & b2 in field {[x,x]} & [((x .--> y) . b1),((x .--> y) . b2)] in {[y,y]} ) ) & ( not b1 in field {[x,x]} or not b2 in field {[x,x]} or not [((x .--> y) . b1),((x .--> y) . b2)] in {[y,y]} or [b1,b2] in {[x,x]} ) ) ) ) thus x .--> y is one-to-one ; ::_thesis: for b1, b2 being set holds ( ( not [b1,b2] in {[x,x]} or ( b1 in field {[x,x]} & b2 in field {[x,x]} & [((x .--> y) . b1),((x .--> y) . b2)] in {[y,y]} ) ) & ( not b1 in field {[x,x]} or not b2 in field {[x,x]} or not [((x .--> y) . b1),((x .--> y) . b2)] in {[y,y]} or [b1,b2] in {[x,x]} ) ) let a, b be set ; ::_thesis: ( ( not [a,b] in {[x,x]} or ( a in field {[x,x]} & b in field {[x,x]} & [((x .--> y) . a),((x .--> y) . b)] in {[y,y]} ) ) & ( not a in field {[x,x]} or not b in field {[x,x]} or not [((x .--> y) . a),((x .--> y) . b)] in {[y,y]} or [a,b] in {[x,x]} ) ) hereby ::_thesis: ( not a in field {[x,x]} or not b in field {[x,x]} or not [((x .--> y) . a),((x .--> y) . b)] in {[y,y]} or [a,b] in {[x,x]} ) assume [a,b] in {[x,x]} ; ::_thesis: ( a in field {[x,x]} & b in field {[x,x]} & [((x .--> y) . a),((x .--> y) . b)] in {[y,y]} ) then [a,b] = [x,x] by TARSKI:def_1; then A2: ( a = x & b = x ) by XTUPLE_0:1; hence ( a in field {[x,x]} & b in field {[x,x]} ) by A1, TARSKI:def_1; ::_thesis: [((x .--> y) . a),((x .--> y) . b)] in {[y,y]} (x .--> y) . x = y by Th72; hence [((x .--> y) . a),((x .--> y) . b)] in {[y,y]} by A2, TARSKI:def_1; ::_thesis: verum end; assume ( a in field {[x,x]} & b in field {[x,x]} ) ; ::_thesis: ( not [((x .--> y) . a),((x .--> y) . b)] in {[y,y]} or [a,b] in {[x,x]} ) then ( a = x & b = x ) by A1, TARSKI:def_1; hence ( not [((x .--> y) . a),((x .--> y) . b)] in {[y,y]} or [a,b] in {[x,x]} ) by TARSKI:def_1; ::_thesis: verum end; theorem :: FUNCOP_1:83 for x, y being set holds {[x,x]},{[y,y]} are_isomorphic proof let x, y be set ; ::_thesis: {[x,x]},{[y,y]} are_isomorphic take x .--> y ; :: according to WELLORD1:def_8 ::_thesis: x .--> y is_isomorphism_of {[x,x]},{[y,y]} thus x .--> y is_isomorphism_of {[x,x]},{[y,y]} by Th82; ::_thesis: verum end; registration let I, A be set ; clusterI --> A -> I -defined total for I -defined Function; coherence for b1 being I -defined Function st b1 = I --> A holds b1 is total ; end; theorem :: FUNCOP_1:84 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 ) assume x in dom f ; ::_thesis: x .--> (f . x) c= f then [x,(f . x)] in f by FUNCT_1:1; then {[x,(f . x)]} c= f by ZFMISC_1:31; hence x .--> (f . x) c= f by ZFMISC_1:29; ::_thesis: verum end; registration let A be non empty set ; let x be set ; let i be Element of A; clusterx .--> i -> A -valued ; coherence x .--> i is A -valued proof rng (x .--> i) = {i} by RELAT_1:160; hence rng (x .--> i) c= A by ZFMISC_1:31; :: according to RELAT_1:def_19 ::_thesis: verum end; end; theorem :: FUNCOP_1:85 for X being non empty set for F being BinOp of X for Y being set for f, g being Function of Y,X for x being Element of X st F is associative holds F .: ((F [;] (x,f)),g) = F [;] (x,(F .: (f,g))) proof let X be non empty set ; ::_thesis: for F being BinOp of X for Y being set for f, g being Function of Y,X for x being Element of X st F is associative holds F .: ((F [;] (x,f)),g) = F [;] (x,(F .: (f,g))) let F be BinOp of X; ::_thesis: for Y being set for f, g being Function of Y,X for x being Element of X st F is associative holds F .: ((F [;] (x,f)),g) = F [;] (x,(F .: (f,g))) let Y be set ; ::_thesis: for f, g being Function of Y,X for x being Element of X st F is associative holds F .: ((F [;] (x,f)),g) = F [;] (x,(F .: (f,g))) let f, g be Function of Y,X; ::_thesis: for x being Element of X st F is associative holds F .: ((F [;] (x,f)),g) = F [;] (x,(F .: (f,g))) let x be Element of X; ::_thesis: ( F is associative implies F .: ((F [;] (x,f)),g) = F [;] (x,(F .: (f,g))) ) assume A1: F is associative ; ::_thesis: F .: ((F [;] (x,f)),g) = F [;] (x,(F .: (f,g))) percases ( Y = {} or Y <> {} ) ; suppose Y = {} ; ::_thesis: F .: ((F [;] (x,f)),g) = F [;] (x,(F .: (f,g))) hence F .: ((F [;] (x,f)),g) = F [;] (x,(F .: (f,g))) ; ::_thesis: verum end; supposeA2: Y <> {} ; ::_thesis: F .: ((F [;] (x,f)),g) = F [;] (x,(F .: (f,g))) now__::_thesis:_for_y_being_Element_of_Y_holds_(F_[;]_(x,(F_.:_(f,g))))_._y_=_F_._(((F_[;]_(x,f))_._y),(g_._y)) let y be Element of Y; ::_thesis: (F [;] (x,(F .: (f,g)))) . y = F . (((F [;] (x,f)) . y),(g . y)) reconsider x1 = f . y, x2 = g . y as Element of X by A2, FUNCT_2:5; thus (F [;] (x,(F .: (f,g)))) . y = F . (x,((F .: (f,g)) . y)) by A2, Th53 .= F . (x,(F . (x1,x2))) by A2, Th37 .= F . ((F . (x,x1)),x2) by A1, BINOP_1:def_3 .= F . (((F [;] (x,f)) . y),(g . y)) by A2, Th53 ; ::_thesis: verum end; hence F .: ((F [;] (x,f)),g) = F [;] (x,(F .: (f,g))) by A2, Th38; ::_thesis: verum end; end; end; registration let A be set ; let B be non empty set ; let x be Element of B; clusterA --> x -> B -valued ; coherence A --> x is B -valued ; end; registration let A be non empty set ; let x be Element of A; let y be set ; clusterx .--> y -> A -defined ; coherence x .--> y is A -defined proof dom (x .--> y) = {x} by Th13; hence dom (x .--> y) c= A by ZFMISC_1:31; :: according to RELAT_1:def_18 ::_thesis: verum end; end; theorem :: FUNCOP_1:86 for x, y, A being set st x in A holds (x .--> y) | A = x .--> y proof let x, y, A be set ; ::_thesis: ( x in A implies (x .--> y) | A = x .--> y ) assume x in A ; ::_thesis: (x .--> y) | A = x .--> y then {x} c= A by ZFMISC_1:31; then dom (x .--> y) c= A by Th13; hence (x .--> y) | A = x .--> y by RELAT_1:68; ::_thesis: verum end; registration let Y be functional set ; cluster Relation-like Y -valued Function-like -> Function-yielding for set ; coherence for b1 being Function st b1 is Y -valued holds b1 is Function-yielding proof let f be Function; ::_thesis: ( f is Y -valued implies f is Function-yielding ) assume A1: f is Y -valued ; ::_thesis: f is Function-yielding let x be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( x in dom f implies f . x is Function ) thus ( x in dom f implies f . x is Function ) by A1; ::_thesis: verum end; end; definition let IT be Function; attrIT is Relation-yielding means :: FUNCOP_1:def 11 for x being set st x in dom IT holds IT . x is Relation; end; :: deftheorem defines Relation-yielding FUNCOP_1:def_11_:_ for IT being Function holds ( IT is Relation-yielding iff for x being set st x in dom IT holds IT . x is Relation ); registration cluster Relation-like Function-like Function-yielding -> Relation-yielding for set ; coherence for b1 being Function st b1 is Function-yielding holds b1 is Relation-yielding proof let f be Function; ::_thesis: ( f is Function-yielding implies f is Relation-yielding ) assume A1: f is Function-yielding ; ::_thesis: f is Relation-yielding let x be set ; :: according to FUNCOP_1:def_11 ::_thesis: ( x in dom f implies f . x is Relation ) thus ( x in dom f implies f . x is Relation ) by A1; ::_thesis: verum end; end; registration cluster Relation-like Function-like empty -> Function-yielding for set ; coherence for b1 being Function st b1 is empty holds b1 is Function-yielding proof let f be Function; ::_thesis: ( f is empty implies f is Function-yielding ) assume A1: f is empty ; ::_thesis: f is Function-yielding let x be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( x in dom f implies f . x is Function ) thus ( x in dom f implies f . x is Function ) by A1; ::_thesis: verum end; end; theorem :: FUNCOP_1:87 for X, Y, x, y being set holds ( X --> x tolerates Y --> y iff ( x = y or X misses Y ) ) proof let X, Y, x, y be set ; ::_thesis: ( X --> x tolerates Y --> y iff ( x = y or X misses Y ) ) set f = X --> x; set g = Y --> y; A1: dom (Y --> y) = Y by Th13; A2: dom (X --> x) = X by Th13; thus ( not X --> x tolerates Y --> y or x = y or X misses Y ) ::_thesis: ( ( x = y or X misses Y ) implies X --> x tolerates Y --> y ) proof assume that A3: for z being set st z in (dom (X --> x)) /\ (dom (Y --> y)) holds (X --> x) . z = (Y --> y) . z and A4: x <> y ; :: according to PARTFUN1:def_4 ::_thesis: X misses Y assume X meets Y ; ::_thesis: contradiction then consider z being set such that A5: z in X and A6: z in Y by XBOOLE_0:3; A7: (X --> x) . z = x by A5, Th7; A8: (Y --> y) . z = y by A6, Th7; z in X /\ Y by A5, A6, XBOOLE_0:def_4; hence contradiction by A2, A1, A3, A4, A7, A8; ::_thesis: verum end; assume A9: ( x = y or X misses Y ) ; ::_thesis: X --> x tolerates Y --> y let z be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not z in (proj1 (X --> x)) /\ (proj1 (Y --> y)) or (X --> x) . z = (Y --> y) . z ) assume A10: z in (dom (X --> x)) /\ (dom (Y --> y)) ; ::_thesis: (X --> x) . z = (Y --> y) . z then A11: z in Y ; A12: z in X by A2, A10, XBOOLE_0:def_4; then (X --> x) . z = x by Th7; hence (X --> x) . z = (Y --> y) . z by A9, A12, A11, Th7, XBOOLE_0:3; ::_thesis: verum end; theorem Th88: :: FUNCOP_1:88 for x, y being set holds rng (x .--> y) = {y} proof let x, y be set ; ::_thesis: rng (x .--> y) = {y} dom (x .--> y) = {x} by Th13; hence rng (x .--> y) = {((x .--> y) . x)} by FUNCT_1:4 .= {y} by Th72 ; ::_thesis: verum end; theorem :: FUNCOP_1:89 for z, A, x, y being set st z in A holds (A --> x) * (y .--> z) = y .--> x proof let z, A, x, y be set ; ::_thesis: ( z in A implies (A --> x) * (y .--> z) = y .--> x ) assume A1: z in A ; ::_thesis: (A --> x) * (y .--> z) = y .--> x A2: dom (y .--> z) = {y} by Th13 .= dom (y .--> x) by Th13 ; rng (y .--> z) = {z} by Th88; then rng (y .--> z) c= A by A1, ZFMISC_1:31; then rng (y .--> z) c= dom (A --> x) by Th13; hence dom ((A --> x) * (y .--> z)) = dom (y .--> x) by A2, RELAT_1:27; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds ( not b1 in proj1 ((A --> x) * (y .--> z)) or ((A --> x) * (y .--> z)) . b1 = (y .--> x) . b1 ) let e be set ; ::_thesis: ( not e in proj1 ((A --> x) * (y .--> z)) or ((A --> x) * (y .--> z)) . e = (y .--> x) . e ) assume A3: e in dom ((A --> x) * (y .--> z)) ; ::_thesis: ((A --> x) * (y .--> z)) . e = (y .--> x) . e thus ((A --> x) * (y .--> z)) . e = (A --> x) . ((y .--> z) . e) by A3, FUNCT_1:12 .= (A --> x) . z by A3, Th7 .= x by A1, Th7 .= (y .--> x) . e by A3, Th7 ; ::_thesis: verum end;