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