:: FUNCT_1 semantic presentation

begin


definition
let X be set ;
attrX is Function-like  means :Def1: :: FUNCT_1:def 1
 for x, y1, y2 being set st [x,y1] in X & [x,y2] in X holds
y1 = y2;
end;

:: deftheorem Def1 defines Function-like FUNCT_1:def_1_:_
 for X being set holds
( X is Function-like iff for x, y1, y2 being set st [x,y1] in X & [x,y2] in X holds
y1 = y2 );

registration
cluster empty  ->  Function-like for set ;
coherence
 for b1 being set st b1 is empty holds
b1 is Function-like
proof
let f be set ; ::_thesis: ( f is empty implies f is Function-like )
assume  f is empty ; ::_thesis: f is Function-like
hence  for x, y1, y2 being set st [x,y1] in f & [x,y2] in f holds
y1 = y2 ; :: according to FUNCT_1:def_1 ::_thesis: verum
end;
end;

registration
cluster Relation-like Function-like for set ;
existence
 ex b1 being Relation st b1 is Function-like
proof
take  {} ; ::_thesis: {} is Function-like
thus  {} is Function-like ; ::_thesis: verum
end;
end;

definition
mode Function is Function-like Relation;
end;

registration
let a, b be set ;
cluster{[a,b]} ->  Function-like ;
coherence
 {[a,b]} is Function-like
proof
set X = {[a,b]};
A1: [:{a},{b}:] = {[a,b]} by ZFMISC_1:29;
 for x, y1, y2 being set st [x,y1] in {[a,b]} & [x,y2] in {[a,b]} holds
y1 = y2
proof
let x, y1, y2 be set ; ::_thesis: ( [x,y1] in {[a,b]} & [x,y2] in {[a,b]} implies y1 = y2 )
assume that
A2: [x,y1] in {[a,b]} and
A3: [x,y2] in {[a,b]} ; ::_thesis: y1 = y2
 y1 = b by A1, A2, ZFMISC_1:28;
hence  y1 = y2 by A1, A3, ZFMISC_1:28; ::_thesis: verum
end;
hence  {[a,b]} is Function-like by Def1; ::_thesis: verum
end;
end;


scheme :: FUNCT_1:sch 1
GraphFunc{ F1() ->  set , P1[ set , set ] } :
 ex f being Function st
for x, y being set holds
( [x,y] in f iff ( x in F1() & P1[x,y] ) )
provided
A1: for x, y1, y2 being set st P1[x,y1] & P1[x,y2] holds
y1 = y2
proof
consider Y being set  such that
A2: for y being set holds
( y in Y iff ex x being set st
( x in F1() & P1[x,y] ) ) from TARSKI:sch_1(A1);
defpred S1[ set ] means  ex x, y being set st
( [x,y] = $1 & P1[x,y] );
consider F being set  such that
A3: for p being set holds
( p in F iff ( p in [:F1(),Y:] & S1[p] ) ) from XBOOLE_0:sch_1();
now__::_thesis:_(_(_for_p_being_set_st_p_in_F_holds_
ex_x,_y_being_set_st_[x,y]_=_p_)_&_(_for_x,_y1,_y2_being_set_st_[x,y1]_in_F_&_[x,y2]_in_F_holds_
y1_=_y2_)_)
thus  for p being set st p in F holds
ex x, y being set st [x,y] = p ::_thesis: for x, y1, y2 being set st [x,y1] in F & [x,y2] in F holds
y1 = y2
proof
let p be set ; ::_thesis: ( p in F implies ex x, y being set st [x,y] = p )
 ( p in F implies ex x, y being set st
( [x,y] = p & P1[x,y] ) ) by A3;
hence  ( p in F implies ex x, y being set st [x,y] = p ) ; ::_thesis: verum
end;
let x, y1, y2 be set ; ::_thesis: ( [x,y1] in F & [x,y2] in F implies y1 = y2 )
assume  [x,y1] in F ; ::_thesis: ( [x,y2] in F implies y1 = y2 )
then consider x1, z1 being set  such that
A4: [x1,z1] = [x,y1] and
A5: P1[x1,z1] by A3;
A6: ( x = x1 & z1 = y1 ) by A4, XTUPLE_0:1;
assume  [x,y2] in F ; ::_thesis: y1 = y2
then consider x2, z2 being set  such that
A7: [x2,z2] = [x,y2] and
A8: P1[x2,z2] by A3;
 ( x = x2 & z2 = y2 ) by A7, XTUPLE_0:1;
hence  y1 = y2 by A1, A5, A8, A6; ::_thesis: verum
end;
then reconsider f = F as Function by Def1, RELAT_1:def_1;
take  f ; ::_thesis: for x, y being set holds
( [x,y] in f iff ( x in F1() & P1[x,y] ) )
let x, y be set ; ::_thesis: ( [x,y] in f iff ( x in F1() & P1[x,y] ) )
thus  ( [x,y] in f implies ( x in F1() & P1[x,y] ) ) ::_thesis: ( x in F1() & P1[x,y] implies [x,y] in f )
proof
assume A9: [x,y] in f ; ::_thesis: ( x in F1() & P1[x,y] )
then consider x1, y1 being set  such that
A10: [x1,y1] = [x,y] and
A11: P1[x1,y1] by A3;
 [x,y] in [:F1(),Y:] by A3, A9;
hence  x in F1() by ZFMISC_1:87; ::_thesis: P1[x,y]
 x1 = x by A10, XTUPLE_0:1;
hence  P1[x,y] by A10, A11, XTUPLE_0:1; ::_thesis: verum
end;
assume that
A12: x in F1() and
A13: P1[x,y] ; ::_thesis: [x,y] in f
 y in Y by A2, A12, A13;
then  [x,y] in [:F1(),Y:] by A12, ZFMISC_1:87;
hence  [x,y] in f by A3, A13; ::_thesis: verum
end;

definition
let f be Function;
let x be set ;
funcf . x ->  set  means :Def2: :: FUNCT_1:def 2
[x,it] in f if x in dom f
otherwise it = {} ;
existence
 ( ( x in dom f implies ex b1 being set st [x,b1] in f ) & ( not x in dom f implies ex b1 being set st b1 = {} ) ) by XTUPLE_0:def_12;
uniqueness
 for b1, b2 being set holds
( ( x in dom f & [x,b1] in f & [x,b2] in f implies b1 = b2 ) & ( not x in dom f & b1 = {} & b2 = {} implies b1 = b2 ) ) by Def1;
consistency
 for b1 being set holds verum ;
end;

:: deftheorem Def2 defines . FUNCT_1:def_2_:_
 for f being Function
for x, b3 being set holds
( ( x in dom f implies ( b3 = f . x iff [x,b3] in f ) ) & ( not x in dom f implies ( b3 = f . x iff b3 = {} ) ) );

theorem Th1: :: FUNCT_1:1
for x, y being set
for f being Function holds
( [x,y] in f iff ( x in dom f & y = f . x ) )
proof
let x, y be set ; ::_thesis: for f being Function holds
( [x,y] in f iff ( x in dom f & y = f . x ) )
let f be Function; ::_thesis: ( [x,y] in f iff ( x in dom f & y = f . x ) )
thus  ( [x,y] in f implies ( x in dom f & y = f . x ) ) ::_thesis: ( x in dom f & y = f . x implies [x,y] in f )
proof
assume A1: [x,y] in f ; ::_thesis: ( x in dom f & y = f . x )
hence  x in dom f by XTUPLE_0:def_12; ::_thesis: y = f . x
hence  y = f . x by A1, Def2; ::_thesis: verum
end;
thus  ( x in dom f & y = f . x implies [x,y] in f ) by Def2; ::_thesis: verum
end;

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

definition
let f be Function;
redefine func rng f means :Def3: :: FUNCT_1:def 3
 for y being set holds
( y in it iff ex x being set st
( x in dom f & y = f . x ) );
compatibility
 for b1 being set holds
( b1 = rng f iff for y being set holds
( y in b1 iff ex x being set st
( x in dom f & y = f . x ) ) )
proof
let Y be set ; ::_thesis: ( Y = rng f iff for y being set holds
( y in Y iff ex x being set st
( x in dom f & y = f . x ) ) )
hereby  ::_thesis: ( ( for y being set holds
( y in Y iff ex x being set st
( x in dom f & y = f . x ) ) ) implies Y = rng f )
assume A1: Y = rng f ; ::_thesis: for y being set holds
( ( y in Y implies ex x being set st
( x in dom f & y = f . x ) ) & ( ex x being set st
( x in dom f & y = f . x ) implies y in Y ) )
let y be set ; ::_thesis: ( ( y in Y implies ex x being set st
( x in dom f & y = f . x ) ) & ( ex x being set st
( x in dom f & y = f . x ) implies y in Y ) )
hereby  ::_thesis: ( ex x being set st
( x in dom f & y = f . x ) implies y in Y )
assume  y in Y ; ::_thesis: ex x being set st
( x in dom f & y = f . x )
then consider x being set  such that
A2: [x,y] in f by A1, XTUPLE_0:def_13;
take x = x; ::_thesis: ( x in dom f & y = f . x )
thus  ( x in dom f & y = f . x ) by A2, Th1; ::_thesis: verum
end;
given x being set  such that A3: ( x in dom f & y = f . x ) ; ::_thesis: y in Y
 [x,y] in f by A3, Def2;
hence  y in Y by A1, XTUPLE_0:def_13; ::_thesis: verum
end;
assume A4: for y being set holds
( y in Y iff ex x being set st
( x in dom f & y = f . x ) ) ; ::_thesis: Y = rng f
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: rng f c= Y
let y be set ; ::_thesis: ( y in Y implies y in rng f )
assume  y in Y ; ::_thesis: y in rng f
then consider x being set  such that
A5: ( x in dom f & y = f . x ) by A4;
 [x,y] in f by A5, Def2;
hence  y in rng f by XTUPLE_0:def_13; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in Y )
assume  y in rng f ; ::_thesis: y in Y
then consider x being set  such that
A6: [x,y] in f by XTUPLE_0:def_13;
 ( x in dom f & y = f . x ) by A6, Th1;
hence  y in Y by A4; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines rng FUNCT_1:def_3_:_
 for f being Function
for b2 being set holds
( b2 = rng f iff for y being set holds
( y in b2 iff ex x being set st
( x in dom f & y = f . x ) ) );

theorem :: FUNCT_1:3
for x being set
for f being Function st x in dom f holds
f . x in rng f by Def3;

theorem Th4: :: FUNCT_1:4
for x being set
for f being Function st dom f = {x} holds
rng f = {(f . x)}
proof
let x be set ; ::_thesis: for f being Function st dom f = {x} holds
rng f = {(f . x)}
let f be Function; ::_thesis: ( dom f = {x} implies rng f = {(f . x)} )
assume A1: dom f = {x} ; ::_thesis: rng f = {(f . x)}
 for y being set holds
( y in rng f iff y in {(f . x)} )
proof
let y be set ; ::_thesis: ( y in rng f iff y in {(f . x)} )
thus  ( y in rng f implies y in {(f . x)} ) ::_thesis: ( y in {(f . x)} implies y in rng f )
proof
assume  y in rng f ; ::_thesis: y in {(f . x)}
then consider z being set  such that
A2: z in dom f and
A3: y = f . z by Def3;
 z = x by A1, A2, TARSKI:def_1;
hence  y in {(f . x)} by A3, TARSKI:def_1; ::_thesis: verum
end;
assume  y in {(f . x)} ; ::_thesis: y in rng f
then A4: y = f . x by TARSKI:def_1;
 x in dom f by A1, TARSKI:def_1;
hence  y in rng f by A4, Def3; ::_thesis: verum
end;
hence  rng f = {(f . x)} by TARSKI:1; ::_thesis: verum
end;

scheme :: FUNCT_1:sch 2
FuncEx{ F1() ->  set , P1[ set , set ] } :
 ex f being Function st
( dom f = F1() & ( for x being set st x in F1() holds
P1[x,f . x] ) )
provided
A1: for x, y1, y2 being set st x in F1() & P1[x,y1] & P1[x,y2] holds
y1 = y2 and
A2: for x being set st x in F1() holds
ex y being set st P1[x,y]
proof
defpred S1[ set , set ] means ( $1 in F1() & P1[$1,$2] );
A3: for x, y1, y2 being set st S1[x,y1] & S1[x,y2] holds
y1 = y2 by A1;
consider f being Function such that
A4: for x, y being set holds
( [x,y] in f iff ( x in F1() & S1[x,y] ) ) from FUNCT_1:sch_1(A3);
take  f ; ::_thesis: ( dom f = F1() & ( for x being set st x in F1() holds
P1[x,f . x] ) )
 for x being set holds
( x in dom f iff x in F1() )
proof
let x be set ; ::_thesis: ( x in dom f iff x in F1() )
thus  ( x in dom f implies x in F1() ) ::_thesis: ( x in F1() implies x in dom f )
proof
assume  x in dom f ; ::_thesis: x in F1()
then  ex y being set st [x,y] in f by XTUPLE_0:def_12;
hence  x in F1() by A4; ::_thesis: verum
end;
assume A5: x in F1() ; ::_thesis: x in dom f
then consider y being set  such that
A6: P1[x,y] by A2;
 [x,y] in f by A4, A5, A6;
hence  x in dom f by XTUPLE_0:def_12; ::_thesis: verum
end;
hence A7: dom f = F1() by TARSKI:1; ::_thesis: for x being set st x in F1() holds
P1[x,f . x]
let x be set ; ::_thesis: ( x in F1() implies P1[x,f . x] )
assume A8: x in F1() ; ::_thesis: P1[x,f . x]
then consider y being set  such that
A9: P1[x,y] by A2;
 [x,y] in f by A4, A8, A9;
hence  P1[x,f . x] by A7, A8, A9, Def2; ::_thesis: verum
end;

scheme :: FUNCT_1:sch 3
Lambda{ F1() ->  set , F2( set ) ->  set } :
 ex f being Function st
( dom f = F1() & ( for x being set st x in F1() holds
f . x = F2(x) ) )
proof
defpred S1[ set , set ] means $2 = F2($1);
A1: for x being set st x in F1() holds
ex y being set st S1[x,y] ;
A2: for x, y1, y2 being set st x in F1() & S1[x,y1] & S1[x,y2] holds
y1 = y2 ;
thus  ex f being Function st
( dom f = F1() & ( for x being set st x in F1() holds
S1[x,f . x] ) ) from FUNCT_1:sch_2(A2, A1); ::_thesis: verum
end;

theorem Th5: :: FUNCT_1:5
for X being set st X <> {} holds
for y being set ex f being Function st
( dom f = X & rng f = {y} )
proof
let X be set ; ::_thesis: ( X <> {} implies for y being set ex f being Function st
( dom f = X & rng f = {y} ) )
assume A1: X <> {} ; ::_thesis: for y being set ex f being Function st
( dom f = X & rng f = {y} )
let y be set ; ::_thesis: ex f being Function st
( dom f = X & rng f = {y} )
deffunc H1( set ) ->  set = y;
consider f being Function such that
A2: dom f = X and
A3: for x being set st x in X holds
f . x = H1(x) from FUNCT_1:sch_3();
take  f ; ::_thesis: ( dom f = X & rng f = {y} )
thus  dom f = X by A2; ::_thesis: rng f = {y}
 for y1 being set holds
( y1 in rng f iff y1 = y )
proof
let y1 be set ; ::_thesis: ( y1 in rng f iff y1 = y )
A4: now__::_thesis:_(_y1_=_y_implies_y1_in_rng_f_)
set x = the Element of X;
assume A5: y1 = y ; ::_thesis: y1 in rng f
 f . the Element of X = y by A1, A3;
hence  y1 in rng f by A1, A2, A5, Def3; ::_thesis: verum
end;
now__::_thesis:_(_y1_in_rng_f_implies_y1_=_y_)
assume  y1 in rng f ; ::_thesis: y1 = y
then  ex x being set st
( x in dom f & y1 = f . x ) by Def3;
hence  y1 = y by A2, A3; ::_thesis: verum
end;
hence  ( y1 in rng f iff y1 = y ) by A4; ::_thesis: verum
end;
hence  rng f = {y} by TARSKI:def_1; ::_thesis: verum
end;

theorem :: FUNCT_1:6
for X being set st ( for f, g being Function st dom f = X & dom g = X holds
f = g ) holds
X = {}
proof
let X be set ; ::_thesis: ( ( for f, g being Function st dom f = X & dom g = X holds
f = g ) implies X = {} )
deffunc H1( set ) ->  set = {} ;
assume A1: for f, g being Function st dom f = X & dom g = X holds
f = g ; ::_thesis: X = {}
set x = the Element of X;
consider f being Function such that
A2: dom f = X and
A3: for x being set st x in X holds
f . x = H1(x) from FUNCT_1:sch_3();
assume A4: not X = {} ; ::_thesis: contradiction
then A5: f . the Element of X = {} by A3;
deffunc H2( set ) ->  set = 1;
consider g being Function such that
A6: dom g = X and
A7: for x being set st x in X holds
g . x = H2(x) from FUNCT_1:sch_3();
 g . the Element of X = 1 by A4, A7;
hence  contradiction by A1, A2, A6, A5; ::_thesis: verum
end;

theorem :: FUNCT_1:7
for y being set
for f, g being Function st dom f = dom g & rng f = {y} & rng g = {y} holds
f = g
proof
let y be set ; ::_thesis: for f, g being Function st dom f = dom g & rng f = {y} & rng g = {y} holds
f = g
let f, g be Function; ::_thesis: ( dom f = dom g & rng f = {y} & rng g = {y} implies f = g )
assume that
A1: dom f = dom g and
A2: rng f = {y} and
A3: rng g = {y} ; ::_thesis: f = g
 for x being set st x in dom f holds
f . x = g . x
proof
let x be set ; ::_thesis: ( x in dom f implies f . x = g . x )
assume A4: x in dom f ; ::_thesis: f . x = g . x
then  f . x in rng f by Def3;
then A5: f . x = y by A2, TARSKI:def_1;
 g . x in rng g by A1, A4, Def3;
hence  f . x = g . x by A3, A5, TARSKI:def_1; ::_thesis: verum
end;
hence  f = g by A1, Th2; ::_thesis: verum
end;

theorem :: FUNCT_1:8
for Y, X being set st ( Y <> {} or X = {} ) holds
ex f being Function st
( X = dom f & rng f c= Y )
proof
let Y, X be set ; ::_thesis: ( ( Y <> {} or X = {} ) implies ex f being Function st
( X = dom f & rng f c= Y ) )
assume A1: ( Y <> {} or X = {} ) ; ::_thesis: ex f being Function st
( X = dom f & rng f c= Y )
A2: now__::_thesis:_(_X_<>_{}_implies_ex_f_being_Function_st_
(_dom_f_=_X_&_rng_f_c=_Y_)_)
set y = the Element of Y;
deffunc H1( set ) ->  Element of Y = the Element of Y;
consider f being Function such that
A3: dom f = X and
A4: for x being set st x in X holds
f . x = H1(x) from FUNCT_1:sch_3();
assume  X <> {} ; ::_thesis: ex f being Function st
( dom f = X & rng f c= Y )
then A5: the Element of Y in Y by A1;
take f = f; ::_thesis: ( dom f = X & rng f c= Y )
thus  dom f = X by A3; ::_thesis: rng f c= Y
 for z being set st z in rng f holds
z in Y
proof
let z be set ; ::_thesis: ( z in rng f implies z in Y )
assume  z in rng f ; ::_thesis: z in Y
then  ex x being set st
( x in dom f & z = f . x ) by Def3;
hence  z in Y by A5, A3, A4; ::_thesis: verum
end;
hence  rng f c= Y by TARSKI:def_3; ::_thesis: verum
end;
now__::_thesis:_(_X_=_{}_implies_ex_f_being_set_st_
(_dom_f_=_X_&_rng_f_c=_Y_)_)
assume A6: X = {} ; ::_thesis: ex f being set st
( dom f = X & rng f c= Y )
take f = {} ; ::_thesis: ( dom f = X & rng f c= Y )
thus  dom f = X by A6; ::_thesis: rng f c= Y
thus  rng f c= Y by XBOOLE_1:2; ::_thesis: verum
end;
hence  ex f being Function st
( X = dom f & rng f c= Y ) by A2; ::_thesis: verum
end;

theorem :: FUNCT_1:9
for Y being set
for f being Function st ( for y being set st y in Y holds
ex x being set st
( x in dom f & y = f . x ) ) holds
Y c= rng f
proof
let Y be set ; ::_thesis: for f being Function st ( for y being set st y in Y holds
ex x being set st
( x in dom f & y = f . x ) ) holds
Y c= rng f
let f be Function; ::_thesis: ( ( for y being set st y in Y holds
ex x being set st
( x in dom f & y = f . x ) ) implies Y c= rng f )
assume A1: for y being set st y in Y holds
ex x being set st
( x in dom f & y = f . x ) ; ::_thesis: Y c= rng f
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Y or y in rng f )
assume  y in Y ; ::_thesis: y in rng f
then  ex x being set st
( x in dom f & y = f . x ) by A1;
hence  y in rng f by Def3; ::_thesis: verum
end;

notation
let f, g be Function;
synonym g * f for f * g;
end;

registration
let f, g be Function;
clusterg * f ->  Function-like ;
coherence
 g * f is Function-like
proof
let x be set ; :: according to FUNCT_1:def_1 ::_thesis: for y1, y2 being set st [x,y1] in g * f & [x,y2] in g * f holds
y1 = y2
let y1, y2 be set ; ::_thesis: ( [x,y1] in g * f & [x,y2] in g * f implies y1 = y2 )
assume  [x,y1] in g * f ; ::_thesis: ( not [x,y2] in g * f or y1 = y2 )
then consider z1 being set  such that
A1: [x,z1] in f and
A2: [z1,y1] in g by RELAT_1:def_8;
assume  [x,y2] in g * f ; ::_thesis: y1 = y2
then consider z2 being set  such that
A3: [x,z2] in f and
A4: [z2,y2] in g by RELAT_1:def_8;
 z1 = z2 by A1, A3, Def1;
hence  y1 = y2 by A2, A4, Def1; ::_thesis: verum
end;
end;

theorem :: FUNCT_1:10
for f, g, h being Function st ( for x being set holds
( x in dom h iff ( x in dom f & f . x in dom g ) ) ) & ( for x being set st x in dom h holds
h . x = g . (f . x) ) holds
h = g * f
proof
let f, g, h be Function; ::_thesis: ( ( for x being set holds
( x in dom h iff ( x in dom f & f . x in dom g ) ) ) & ( for x being set st x in dom h holds
h . x = g . (f . x) ) implies h = g * f )
assume that
A1: for x being set holds
( x in dom h iff ( x in dom f & f . x in dom g ) ) and
A2: for x being set st x in dom h holds
h . x = g . (f . x) ; ::_thesis: h = g * f
now__::_thesis:_for_x,_y_being_set_holds_
(_(_[x,y]_in_h_implies_ex_y1_being_set_st_
(_[x,y1]_in_f_&_[y1,y]_in_g_)_)_&_(_ex_z_being_set_st_
(_[x,z]_in_f_&_[z,y]_in_g_)_implies_[x,y]_in_h_)_)
let x, y be set ; ::_thesis: ( ( [x,y] in h implies ex y1 being set st
( [x,y1] in f & [y1,y] in g ) ) & ( ex z being set st
( [x,z] in f & [z,y] in g ) implies [x,y] in h ) )
hereby  ::_thesis: ( ex z being set st
( [x,z] in f & [z,y] in g ) implies [x,y] in h )
assume A3: [x,y] in h ; ::_thesis: ex y1 being set st
( [x,y1] in f & [y1,y] in g )
then A4: x in dom h by XTUPLE_0:def_12;
then A5: f . x in dom g by A1;
take y1 = f . x; ::_thesis: ( [x,y1] in f & [y1,y] in g )
 x in dom f by A1, A4;
hence  [x,y1] in f by Def2; ::_thesis: [y1,y] in g
y = h . x by A3, A4, Def2
.= g . (f . x) by A2, A4 ;
hence  [y1,y] in g by A5, Def2; ::_thesis: verum
end;
given z being set  such that A6: [x,z] in f and
A7: [z,y] in g ; ::_thesis: [x,y] in h
A8: x in dom f by A6, XTUPLE_0:def_12;
then A9: z = f . x by A6, Def2;
A10: z in dom g by A7, XTUPLE_0:def_12;
then A11: x in dom h by A1, A8, A9;
 y = g . z by A7, A10, Def2;
then  y = h . x by A2, A9, A11;
hence  [x,y] in h by A11, Def2; ::_thesis: verum
end;
hence  h = g * f by RELAT_1:def_8; ::_thesis: verum
end;

theorem Th11: :: FUNCT_1:11
for x being set
for g, f being Function holds
( x in dom (g * f) iff ( x in dom f & f . x in dom g ) )
proof
let x be set ; ::_thesis: for g, f being Function holds
( x in dom (g * f) iff ( x in dom f & f . x in dom g ) )
let g, f be Function; ::_thesis: ( x in dom (g * f) iff ( x in dom f & f . x in dom g ) )
set h = g * f;
hereby  ::_thesis: ( x in dom f & f . x in dom g implies x in dom (g * f) )
assume  x in dom (g * f) ; ::_thesis: ( x in dom f & f . x in dom g )
then consider y being set  such that
A1: [x,y] in g * f by XTUPLE_0:def_12;
consider z being set  such that
A2: [x,z] in f and
A3: [z,y] in g by A1, RELAT_1:def_8;
thus  x in dom f by A2, XTUPLE_0:def_12; ::_thesis: f . x in dom g
then  z = f . x by A2, Def2;
hence  f . x in dom g by A3, XTUPLE_0:def_12; ::_thesis: verum
end;
assume A4: x in dom f ; ::_thesis: ( not f . x in dom g or x in dom (g * f) )
then consider z being set  such that
A5: [x,z] in f by XTUPLE_0:def_12;
assume  f . x in dom g ; ::_thesis: x in dom (g * f)
then consider y being set  such that
A6: [(f . x),y] in g by XTUPLE_0:def_12;
 z = f . x by A4, A5, Def2;
then  [x,y] in g * f by A5, A6, RELAT_1:def_8;
hence  x in dom (g * f) by XTUPLE_0:def_12; ::_thesis: verum
end;

theorem Th12: :: FUNCT_1:12
for x being set
for g, f being Function st x in dom (g * f) holds
(g * f) . x = g . (f . x)
proof
let x be set ; ::_thesis: for g, f being Function st x in dom (g * f) holds
(g * f) . x = g . (f . x)
let g, f be Function; ::_thesis: ( x in dom (g * f) implies (g * f) . x = g . (f . x) )
set h = g * f;
assume A1: x in dom (g * f) ; ::_thesis: (g * f) . x = g . (f . x)
then consider y being set  such that
A2: [x,y] in g * f by XTUPLE_0:def_12;
consider z being set  such that
A3: [x,z] in f and
A4: [z,y] in g by A2, RELAT_1:def_8;
 x in dom f by A3, XTUPLE_0:def_12;
then A5: z = f . x by A3, Def2;
then  f . x in dom g by A4, XTUPLE_0:def_12;
then  y = g . (f . x) by A4, A5, Def2;
hence  (g * f) . x = g . (f . x) by A1, A2, Def2; ::_thesis: verum
end;

theorem Th13: :: FUNCT_1:13
for x being set
for f, g being Function st x in dom f holds
(g * f) . x = g . (f . x)
proof
let x be set ; ::_thesis: for f, g being Function st x in dom f holds
(g * f) . x = g . (f . x)
let f, g be Function; ::_thesis: ( x in dom f implies (g * f) . x = g . (f . x) )
assume A1: x in dom f ; ::_thesis: (g * f) . x = g . (f . x)
percases ( f . x in dom g or not f . x in dom g ) ;
suppose f . x in dom g ; ::_thesis: (g * f) . x = g . (f . x)
then  x in dom (g * f) by A1, Th11;
hence  (g * f) . x = g . (f . x) by Th12; ::_thesis: verum
end;
supposeA2: not f . x in dom g ; ::_thesis: (g * f) . x = g . (f . x)
then  not x in dom (g * f) by Th11;
hence (g * f) . x = {} by Def2
.= g . (f . x) by A2, Def2 ;
::_thesis: verum
end;
end;
end;

theorem :: FUNCT_1:14
for z being set
for g, f being Function st z in rng (g * f) holds
z in rng g
proof
let z be set ; ::_thesis: for g, f being Function st z in rng (g * f) holds
z in rng g
let g, f be Function; ::_thesis: ( z in rng (g * f) implies z in rng g )
assume  z in rng (g * f) ; ::_thesis: z in rng g
then consider x being set  such that
A1: x in dom (g * f) and
A2: z = (g * f) . x by Def3;
 ( f . x in dom g & (g * f) . x = g . (f . x) ) by A1, Th11, Th12;
hence  z in rng g by A2, Def3; ::_thesis: verum
end;

theorem Th15: :: FUNCT_1:15
for g, f being Function st dom (g * f) = dom f holds
rng f c= dom g
proof
let g, f be Function; ::_thesis: ( dom (g * f) = dom f implies rng f c= dom g )
assume A1: dom (g * f) = dom f ; ::_thesis: rng f c= dom g
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in dom g )
assume  y in rng f ; ::_thesis: y in dom g
then  ex x being set st
( x in dom f & y = f . x ) by Def3;
hence  y in dom g by A1, Th11; ::_thesis: verum
end;

theorem :: FUNCT_1:16
for Y being set
for f being Function st rng f c= Y & ( for g, h being Function st dom g = Y & dom h = Y & g * f = h * f holds
g = h ) holds
Y = rng f
proof
let Y be set ; ::_thesis: for f being Function st rng f c= Y & ( for g, h being Function st dom g = Y & dom h = Y & g * f = h * f holds
g = h ) holds
Y = rng f
let f be Function; ::_thesis: ( rng f c= Y & ( for g, h being Function st dom g = Y & dom h = Y & g * f = h * f holds
g = h ) implies Y = rng f )
assume that
A1: rng f c= Y and
A2: for g, h being Function st dom g = Y & dom h = Y & g * f = h * f holds
g = h ; ::_thesis: Y = rng f
 Y c= rng f
proof
deffunc H1( set ) ->  set = {} ;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Y or y in rng f )
assume that
A3: y in Y and
A4: not y in rng f ; ::_thesis: contradiction
defpred S1[ set , set ] means ( ( $1 = y implies $2 = 1 ) & ( $1 <> y implies $2 = {} ) );
A5: for x being set st x in Y holds
ex y1 being set st S1[x,y1]
proof
let x be set ; ::_thesis: ( x in Y implies ex y1 being set st S1[x,y1] )
assume  x in Y ; ::_thesis: ex y1 being set st S1[x,y1]
 ( x = y implies ex y1 being set st S1[x,y1] ) ;
hence  ex y1 being set st S1[x,y1] ; ::_thesis: verum
end;
A6: for x, y1, y2 being set st x in Y & S1[x,y1] & S1[x,y2] holds
y1 = y2 ;
consider h being Function such that
A7: dom h = Y and
A8: for x being set st x in Y holds
S1[x,h . x] from FUNCT_1:sch_2(A6, A5);
A9: dom (h * f) = dom f by A1, A7, RELAT_1:27;
consider g being Function such that
A10: dom g = Y and
A11: for x being set st x in Y holds
g . x = H1(x) from FUNCT_1:sch_3();
A12: dom (g * f) = dom f by A1, A10, RELAT_1:27;
 for x being set st x in dom f holds
(g * f) . x = (h * f) . x
proof
let x be set ; ::_thesis: ( x in dom f implies (g * f) . x = (h * f) . x )
assume A13: x in dom f ; ::_thesis: (g * f) . x = (h * f) . x
then  f . x in rng f by Def3;
then A14: ( g . (f . x) = {} & h . (f . x) = {} ) by A1, A4, A11, A8;
 (g * f) . x = g . (f . x) by A12, A13, Th12;
hence  (g * f) . x = (h * f) . x by A9, A13, A14, Th12; ::_thesis: verum
end;
then A15: g = h by A2, A10, A7, A12, A9, Th2;
 g . y = {} by A3, A11;
hence  contradiction by A3, A8, A15; ::_thesis: verum
end;
hence  Y = rng f by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

registration
let X be set ;
cluster id X ->  Function-like ;
coherence
 id X is Function-like
proof
let x be set ; :: according to FUNCT_1:def_1 ::_thesis: for y1, y2 being set st [x,y1] in id X & [x,y2] in id X holds
y1 = y2
let y1, y2 be set ; ::_thesis: ( [x,y1] in id X & [x,y2] in id X implies y1 = y2 )
assume that
A1: [x,y1] in id X and
A2: [x,y2] in id X ; ::_thesis: y1 = y2
 x = y1 by A1, RELAT_1:def_10;
hence  y1 = y2 by A2, RELAT_1:def_10; ::_thesis: verum
end;
end;

theorem Th17: :: FUNCT_1:17
for X being set
for f being Function holds
( f = id X iff ( dom f = X & ( for x being set st x in X holds
f . x = x ) ) )
proof
let X be set ; ::_thesis: for f being Function holds
( f = id X iff ( dom f = X & ( for x being set st x in X holds
f . x = x ) ) )
let f be Function; ::_thesis: ( f = id X iff ( dom f = X & ( for x being set st x in X holds
f . x = x ) ) )
hereby  ::_thesis: ( dom f = X & ( for x being set st x in X holds
f . x = x ) implies f = id X )
assume A1: f = id X ; ::_thesis: ( dom f = X & ( for x being set st x in X holds
f . x = x ) )
hence A2: dom f = X by RELAT_1:45; ::_thesis: for x being set st x in X holds
f . x = x
let x be set ; ::_thesis: ( x in X implies f . x = x )
assume A3: x in X ; ::_thesis: f . x = x
then  [x,x] in f by A1, RELAT_1:def_10;
hence  f . x = x by A2, A3, Def2; ::_thesis: verum
end;
assume that
A4: dom f = X and
A5: for x being set st x in X holds
f . x = x ; ::_thesis: f = id X
now__::_thesis:_for_x,_y_being_set_holds_
(_(_[x,y]_in_f_implies_(_x_in_X_&_x_=_y_)_)_&_(_x_in_X_&_x_=_y_implies_[x,y]_in_f_)_)
let x, y be set ; ::_thesis: ( ( [x,y] in f implies ( x in X & x = y ) ) & ( x in X & x = y implies [x,y] in f ) )
hereby  ::_thesis: ( x in X & x = y implies [x,y] in f )
assume A6: [x,y] in f ; ::_thesis: ( x in X & x = y )
hence A7: x in X by A4, Th1; ::_thesis: x = y
 y = f . x by A6, Th1;
hence  x = y by A5, A7; ::_thesis: verum
end;
assume A8: x in X ; ::_thesis: ( x = y implies [x,y] in f )
then  f . x = x by A5;
hence  ( x = y implies [x,y] in f ) by A4, A8, Th1; ::_thesis: verum
end;
hence  f = id X by RELAT_1:def_10; ::_thesis: verum
end;

theorem :: FUNCT_1:18
for x, X being set st x in X holds
(id X) . x = x by Th17;

theorem Th19: :: FUNCT_1:19
for X being set
for f being Function holds dom (f * (id X)) = (dom f) /\ X
proof
let X be set ; ::_thesis: for f being Function holds dom (f * (id X)) = (dom f) /\ X
let f be Function; ::_thesis: dom (f * (id X)) = (dom f) /\ X
 for x being set holds
( x in dom (f * (id X)) iff x in (dom f) /\ X )
proof
let x be set ; ::_thesis: ( x in dom (f * (id X)) iff x in (dom f) /\ X )
 ( x in dom (f * (id X)) iff ( x in dom f & x in X ) )
proof
thus  ( x in dom (f * (id X)) implies ( x in dom f & x in X ) ) ::_thesis: ( x in dom f & x in X implies x in dom (f * (id X)) )
proof
assume  x in dom (f * (id X)) ; ::_thesis: ( x in dom f & x in X )
then A1: ( x in dom (id X) & (id X) . x in dom f ) by Th11;
thus  ( x in dom f & x in X ) by A1, Th17; ::_thesis: verum
end;
assume A2: x in dom f ; ::_thesis: ( not x in X or x in dom (f * (id X)) )
A3: dom (id X) = X ;
assume A4: x in X ; ::_thesis: x in dom (f * (id X))
then  (id X) . x in dom f by A2, Th17;
hence  x in dom (f * (id X)) by A4, A3, Th11; ::_thesis: verum
end;
hence  ( x in dom (f * (id X)) iff x in (dom f) /\ X ) by XBOOLE_0:def_4; ::_thesis: verum
end;
hence  dom (f * (id X)) = (dom f) /\ X by TARSKI:1; ::_thesis: verum
end;

theorem :: FUNCT_1:20
for x, X being set
for f being Function st x in (dom f) /\ X holds
f . x = (f * (id X)) . x
proof
let x, X be set ; ::_thesis: for f being Function st x in (dom f) /\ X holds
f . x = (f * (id X)) . x
let f be Function; ::_thesis: ( x in (dom f) /\ X implies f . x = (f * (id X)) . x )
assume  x in (dom f) /\ X ; ::_thesis: f . x = (f * (id X)) . x
then  x in X by XBOOLE_0:def_4;
then  ( (id X) . x = x & x in dom (id X) ) by Th17;
hence  f . x = (f * (id X)) . x by Th13; ::_thesis: verum
end;

theorem :: FUNCT_1:21
for x, Y being set
for f being Function holds
( x in dom ((id Y) * f) iff ( x in dom f & f . x in Y ) )
proof
let x, Y be set ; ::_thesis: for f being Function holds
( x in dom ((id Y) * f) iff ( x in dom f & f . x in Y ) )
let f be Function; ::_thesis: ( x in dom ((id Y) * f) iff ( x in dom f & f . x in Y ) )
 dom (id Y) = Y ;
hence  ( x in dom ((id Y) * f) iff ( x in dom f & f . x in Y ) ) by Th11; ::_thesis: verum
end;

theorem :: FUNCT_1:22
for X, Y being set holds (id X) * (id Y) = id (X /\ Y)
proof
let X, Y be set ; ::_thesis: (id X) * (id Y) = id (X /\ Y)
A1: dom ((id X) * (id Y)) = (dom (id X)) /\ Y by Th19
.= X /\ Y ;
A2: for z being set st z in X /\ Y holds
((id X) * (id Y)) . z = (id (X /\ Y)) . z
proof
let z be set ; ::_thesis: ( z in X /\ Y implies ((id X) * (id Y)) . z = (id (X /\ Y)) . z )
assume A3: z in X /\ Y ; ::_thesis: ((id X) * (id Y)) . z = (id (X /\ Y)) . z
then A4: z in X by XBOOLE_0:def_4;
A5: z in Y by A3, XBOOLE_0:def_4;
thus ((id X) * (id Y)) . z = (id X) . ((id Y) . z) by A1, A3, Th12
.= (id X) . z by A5, Th17
.= z by A4, Th17
.= (id (X /\ Y)) . z by A3, Th17 ; ::_thesis: verum
end;
 X /\ Y = dom (id (X /\ Y)) ;
hence  (id X) * (id Y) = id (X /\ Y) by A1, A2, Th2; ::_thesis: verum
end;

theorem Th23: :: FUNCT_1:23
for f, g being Function st rng f = dom g & g * f = f holds
g = id (dom g)
proof
let f, g be Function; ::_thesis: ( rng f = dom g & g * f = f implies g = id (dom g) )
assume that
A1: rng f = dom g and
A2: g * f = f ; ::_thesis: g = id (dom g)
set X = dom g;
 for x being set st x in dom g holds
g . x = x
proof
let x be set ; ::_thesis: ( x in dom g implies g . x = x )
assume  x in dom g ; ::_thesis: g . x = x
then  ex y being set st
( y in dom f & f . y = x ) by A1, Def3;
hence  g . x = x by A2, Th13; ::_thesis: verum
end;
hence  g = id (dom g) by Th17; ::_thesis: verum
end;

definition
let f be Function;
attrf is one-to-one  means :Def4: :: FUNCT_1:def 4
 for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2;
end;

:: deftheorem Def4 defines one-to-one FUNCT_1:def_4_:_
 for f being Function holds
( f is one-to-one iff for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2 );

theorem Th24: :: FUNCT_1:24
for f, g being Function st f is one-to-one & g is one-to-one holds
g * f is one-to-one
proof
let f, g be Function; ::_thesis: ( f is one-to-one & g is one-to-one implies g * f is one-to-one )
assume that
A1: f is one-to-one and
A2: g is one-to-one ; ::_thesis: g * f is one-to-one
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_(g_*_f)_&_x2_in_dom_(g_*_f)_&_(g_*_f)_._x1_=_(g_*_f)_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom (g * f) & x2 in dom (g * f) & (g * f) . x1 = (g * f) . x2 implies x1 = x2 )
assume A3: ( x1 in dom (g * f) & x2 in dom (g * f) ) ; ::_thesis: ( (g * f) . x1 = (g * f) . x2 implies x1 = x2 )
then A4: ( (g * f) . x1 = g . (f . x1) & (g * f) . x2 = g . (f . x2) ) by Th12;
A5: ( x1 in dom f & x2 in dom f ) by A3, Th11;
assume A6: (g * f) . x1 = (g * f) . x2 ; ::_thesis: x1 = x2
 ( f . x1 in dom g & f . x2 in dom g ) by A3, Th11;
then  f . x1 = f . x2 by A2, A4, A6, Def4;
hence  x1 = x2 by A1, A5, Def4; ::_thesis: verum
end;
hence  g * f is one-to-one by Def4; ::_thesis: verum
end;

theorem Th25: :: FUNCT_1:25
for g, f being Function st g * f is one-to-one & rng f c= dom g holds
f is one-to-one
proof
let g, f be Function; ::_thesis: ( g * f is one-to-one & rng f c= dom g implies f is one-to-one )
assume that
A1: g * f is one-to-one and
A2: rng f c= dom g ; ::_thesis: f is one-to-one
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_f_&_x2_in_dom_f_&_f_._x1_=_f_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A3: ( x1 in dom f & x2 in dom f ) and
A4: f . x1 = f . x2 ; ::_thesis: x1 = x2
A5: ( x1 in dom (g * f) & x2 in dom (g * f) ) by A2, A3, RELAT_1:27;
 ( (g * f) . x1 = g . (f . x1) & (g * f) . x2 = g . (f . x2) ) by A3, Th13;
hence  x1 = x2 by A1, A4, A5, Def4; ::_thesis: verum
end;
hence  f is one-to-one by Def4; ::_thesis: verum
end;

theorem :: FUNCT_1:26
for g, f being Function st g * f is one-to-one & rng f = dom g holds
( f is one-to-one & g is one-to-one )
proof
let g, f be Function; ::_thesis: ( g * f is one-to-one & rng f = dom g implies ( f is one-to-one & g is one-to-one ) )
assume that
A1: g * f is one-to-one and
A2: rng f = dom g ; ::_thesis: ( f is one-to-one & g is one-to-one )
A3: dom (g * f) = dom f by A2, RELAT_1:27;
thus  f is one-to-one by A1, A2, Th25; ::_thesis: g is one-to-one
assume  not g is one-to-one ; ::_thesis: contradiction
then consider y1, y2 being set  such that
A4: y1 in dom g and
A5: y2 in dom g and
A6: ( g . y1 = g . y2 & y1 <> y2 ) by Def4;
consider x2 being set  such that
A7: x2 in dom f and
A8: f . x2 = y2 by A2, A5, Def3;
A9: (g * f) . x2 = g . (f . x2) by A7, Th13;
consider x1 being set  such that
A10: x1 in dom f and
A11: f . x1 = y1 by A2, A4, Def3;
 (g * f) . x1 = g . (f . x1) by A10, Th13;
hence  contradiction by A1, A6, A10, A11, A7, A8, A3, A9, Def4; ::_thesis: verum
end;

theorem :: FUNCT_1:27
for f being Function holds
( f is one-to-one iff for g, h being Function st rng g c= dom f & rng h c= dom f & dom g = dom h & f * g = f * h holds
g = h )
proof
let f be Function; ::_thesis: ( f is one-to-one iff for g, h being Function st rng g c= dom f & rng h c= dom f & dom g = dom h & f * g = f * h holds
g = h )
thus  ( f is one-to-one implies for g, h being Function st rng g c= dom f & rng h c= dom f & dom g = dom h & f * g = f * h holds
g = h ) ::_thesis: ( ( for g, h being Function st rng g c= dom f & rng h c= dom f & dom g = dom h & f * g = f * h holds
g = h ) implies f is one-to-one )
proof
assume A1: f is one-to-one ; ::_thesis: for g, h being Function st rng g c= dom f & rng h c= dom f & dom g = dom h & f * g = f * h holds
g = h
let g, h be Function; ::_thesis: ( rng g c= dom f & rng h c= dom f & dom g = dom h & f * g = f * h implies g = h )
assume that
A2: ( rng g c= dom f & rng h c= dom f ) and
A3: dom g = dom h and
A4: f * g = f * h ; ::_thesis: g = h
 for x being set st x in dom g holds
g . x = h . x
proof
let x be set ; ::_thesis: ( x in dom g implies g . x = h . x )
assume A5: x in dom g ; ::_thesis: g . x = h . x
then A6: ( g . x in rng g & h . x in rng h ) by A3, Def3;
 ( (f * g) . x = f . (g . x) & (f * h) . x = f . (h . x) ) by A3, A5, Th13;
hence  g . x = h . x by A1, A2, A4, A6, Def4; ::_thesis: verum
end;
hence  g = h by A3, Th2; ::_thesis: verum
end;
assume A7: for g, h being Function st rng g c= dom f & rng h c= dom f & dom g = dom h & f * g = f * h holds
g = h ; ::_thesis: f is one-to-one
 for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A8: x1 in dom f and
A9: x2 in dom f and
A10: f . x1 = f . x2 ; ::_thesis: x1 = x2
deffunc H1( set ) ->  set = x1;
consider g being Function such that
A11: dom g = {{}} and
A12: for x being set st x in {{}} holds
g . x = H1(x) from FUNCT_1:sch_3();
A13: {} in {{}} by TARSKI:def_1;
then A14: g . {} = x1 by A12;
then  rng g = {x1} by A11, Th4;
then A15: rng g c= dom f by A8, ZFMISC_1:31;
then A16: dom (f * g) = dom g by RELAT_1:27;
deffunc H2( set ) ->  set = x2;
consider h being Function such that
A17: dom h = {{}} and
A18: for x being set st x in {{}} holds
h . x = H2(x) from FUNCT_1:sch_3();
A19: h . {} = x2 by A18, A13;
then  rng h = {x2} by A17, Th4;
then A20: rng h c= dom f by A9, ZFMISC_1:31;
then A21: dom (f * h) = dom h by RELAT_1:27;
 for x being set st x in dom (f * g) holds
(f * g) . x = (f * h) . x
proof
let x be set ; ::_thesis: ( x in dom (f * g) implies (f * g) . x = (f * h) . x )
assume A22: x in dom (f * g) ; ::_thesis: (f * g) . x = (f * h) . x
then A23: g . x = x1 by A11, A12, A16;
 ( (f * g) . x = f . (g . x) & (f * h) . x = f . (h . x) ) by A11, A17, A16, A21, A22, Th12;
hence  (f * g) . x = (f * h) . x by A10, A11, A18, A16, A22, A23; ::_thesis: verum
end;
hence  x1 = x2 by A7, A11, A17, A14, A19, A15, A20, A16, A21, Th2; ::_thesis: verum
end;
hence  f is one-to-one by Def4; ::_thesis: verum
end;

theorem :: FUNCT_1:28
for X being set
for f, g being Function st dom f = X & dom g = X & rng g c= X & f is one-to-one & f * g = f holds
g = id X
proof
let X be set ; ::_thesis: for f, g being Function st dom f = X & dom g = X & rng g c= X & f is one-to-one & f * g = f holds
g = id X
let f, g be Function; ::_thesis: ( dom f = X & dom g = X & rng g c= X & f is one-to-one & f * g = f implies g = id X )
assume that
A1: dom f = X and
A2: dom g = X and
A3: ( rng g c= X & f is one-to-one ) and
A4: f * g = f ; ::_thesis: g = id X
 for x being set st x in X holds
g . x = x
proof
let x be set ; ::_thesis: ( x in X implies g . x = x )
assume A5: x in X ; ::_thesis: g . x = x
then  ( g . x in rng g & f . x = f . (g . x) ) by A2, A4, Def3, Th13;
hence  g . x = x by A1, A3, A5, Def4; ::_thesis: verum
end;
hence  g = id X by A2, Th17; ::_thesis: verum
end;

theorem :: FUNCT_1:29
for g, f being Function st rng (g * f) = rng g & g is one-to-one holds
dom g c= rng f
proof
let g, f be Function; ::_thesis: ( rng (g * f) = rng g & g is one-to-one implies dom g c= rng f )
assume that
A1: rng (g * f) = rng g and
A2: g is one-to-one ; ::_thesis: dom g c= rng f
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in dom g or y in rng f )
assume A3: y in dom g ; ::_thesis: y in rng f
then  g . y in rng (g * f) by A1, Def3;
then consider x being set  such that
A4: x in dom (g * f) and
A5: g . y = (g * f) . x by Def3;
 ( (g * f) . x = g . (f . x) & f . x in dom g ) by A4, Th11, Th12;
then A6: y = f . x by A2, A3, A5, Def4;
 x in dom f by A4, Th11;
hence  y in rng f by A6, Def3; ::_thesis: verum
end;

registration
let X be set ;
cluster id X ->  one-to-one ;
coherence
 id X is one-to-one
proof
let x1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for x2 being set st x1 in dom (id X) & x2 in dom (id X) & (id X) . x1 = (id X) . x2 holds
x1 = x2
let x2 be set ; ::_thesis: ( x1 in dom (id X) & x2 in dom (id X) & (id X) . x1 = (id X) . x2 implies x1 = x2 )
assume that
A1: x1 in dom (id X) and
A2: x2 in dom (id X) ; ::_thesis: ( not (id X) . x1 = (id X) . x2 or x1 = x2 )
 x1 in X by A1;
then A3: (id X) . x1 = x1 by Th17;
 x2 in X by A2;
hence  ( not (id X) . x1 = (id X) . x2 or x1 = x2 ) by A3, Th17; ::_thesis: verum
end;
end;

theorem :: FUNCT_1:30
canceled;

theorem :: FUNCT_1:31
for f being Function st ex g being Function st g * f = id (dom f) holds
f is one-to-one
proof
let f be Function; ::_thesis: ( ex g being Function st g * f = id (dom f) implies f is one-to-one )
given g being Function such that A1: g * f = id (dom f) ; ::_thesis: f is one-to-one
 dom (g * f) = dom f by A1, RELAT_1:45;
then  rng f c= dom g by Th15;
hence  f is one-to-one by A1, Th25; ::_thesis: verum
end;

registration
cluster empty Relation-like Function-like  ->  one-to-one for set ;
coherence
 for b1 being Function st b1 is empty holds
b1 is one-to-one
proof
let f be Function; ::_thesis: ( f is empty implies f is one-to-one )
assume A1: f is empty ; ::_thesis: f is one-to-one
let x1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
let x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
thus  ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 ) by A1; ::_thesis: verum
end;
end;

registration
cluster Relation-like Function-like one-to-one for set ;
existence
 ex b1 being Function st b1 is one-to-one
proof
take  {} ; ::_thesis: {} is one-to-one
thus  {} is one-to-one ; ::_thesis: verum
end;
end;

registration
let f be one-to-one Function;
clusterf ~  ->  Function-like ;
coherence
 f ~ is Function-like
proof
let x be set ; :: according to FUNCT_1:def_1 ::_thesis: for y1, y2 being set st [x,y1] in f ~ & [x,y2] in f ~ holds
y1 = y2
let y1, y2 be set ; ::_thesis: ( [x,y1] in f ~ & [x,y2] in f ~ implies y1 = y2 )
assume that
A1: [x,y1] in f ~ and
A2: [x,y2] in f ~ ; ::_thesis: y1 = y2
A3: [y2,x] in f by A2, RELAT_1:def_7;
then A4: y2 in dom f by XTUPLE_0:def_12;
then A5: x = f . y2 by A3, Def2;
A6: [y1,x] in f by A1, RELAT_1:def_7;
then A7: y1 in dom f by XTUPLE_0:def_12;
then  x = f . y1 by A6, Def2;
hence  y1 = y2 by A7, A4, A5, Def4; ::_thesis: verum
end;
end;

definition
let f be Function;
assume A1: f is one-to-one ;
funcf "  ->  Function equals :Def5: :: FUNCT_1:def 5
f ~ ;
coherence
 f ~ is Function by A1;
end;

:: deftheorem Def5 defines " FUNCT_1:def_5_:_
 for f being Function st f is one-to-one holds
f " = f ~ ;

theorem Th32: :: FUNCT_1:32
for f being Function st f is one-to-one holds
for g being Function holds
( g = f " iff ( dom g = rng f & ( for y, x being set holds
( y in rng f & x = g . y iff ( x in dom f & y = f . x ) ) ) ) )
proof
let f be Function; ::_thesis: ( f is one-to-one implies for g being Function holds
( g = f " iff ( dom g = rng f & ( for y, x being set holds
( y in rng f & x = g . y iff ( x in dom f & y = f . x ) ) ) ) ) )
assume A1: f is one-to-one ; ::_thesis: for g being Function holds
( g = f " iff ( dom g = rng f & ( for y, x being set holds
( y in rng f & x = g . y iff ( x in dom f & y = f . x ) ) ) ) )
let g be Function; ::_thesis: ( g = f " iff ( dom g = rng f & ( for y, x being set holds
( y in rng f & x = g . y iff ( x in dom f & y = f . x ) ) ) ) )
thus  ( g = f " implies ( dom g = rng f & ( for y, x being set holds
( y in rng f & x = g . y iff ( x in dom f & y = f . x ) ) ) ) ) ::_thesis: ( dom g = rng f & ( for y, x being set holds
( y in rng f & x = g . y iff ( x in dom f & y = f . x ) ) ) implies g = f " )
proof
assume  g = f " ; ::_thesis: ( dom g = rng f & ( for y, x being set holds
( y in rng f & x = g . y iff ( x in dom f & y = f . x ) ) ) )
then A2: g = f ~ by A1, Def5;
hence  dom g = rng f by RELAT_1:20; ::_thesis: for y, x being set holds
( y in rng f & x = g . y iff ( x in dom f & y = f . x ) )
let y, x be set ; ::_thesis: ( y in rng f & x = g . y iff ( x in dom f & y = f . x ) )
thus  ( y in rng f & x = g . y implies ( x in dom f & y = f . x ) ) ::_thesis: ( x in dom f & y = f . x implies ( y in rng f & x = g . y ) )
proof
assume that
A3: y in rng f and
A4: x = g . y ; ::_thesis: ( x in dom f & y = f . x )
 y in dom g by A2, A3, RELAT_1:20;
then  [y,x] in g by A4, Def2;
then A5: [x,y] in f by A2, RELAT_1:def_7;
hence  x in dom f by XTUPLE_0:def_12; ::_thesis: y = f . x
hence  y = f . x by A5, Def2; ::_thesis: verum
end;
assume  ( x in dom f & y = f . x ) ; ::_thesis: ( y in rng f & x = g . y )
then A6: [x,y] in f by Def2;
hence  y in rng f by XTUPLE_0:def_13; ::_thesis: x = g . y
then A7: y in dom g by A2, RELAT_1:20;
 [y,x] in g by A2, A6, RELAT_1:def_7;
hence  x = g . y by A7, Def2; ::_thesis: verum
end;
assume that
A8: dom g = rng f and
A9: for y, x being set holds
( y in rng f & x = g . y iff ( x in dom f & y = f . x ) ) ; ::_thesis: g = f "
let a, b be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [a,b] in g or [a,b] in f " ) & ( not [a,b] in f " or [a,b] in g ) )
thus  ( [a,b] in g implies [a,b] in f " ) ::_thesis: ( not [a,b] in f " or [a,b] in g )
proof
assume A10: [a,b] in g ; ::_thesis: [a,b] in f "
then A11: a in dom g by XTUPLE_0:def_12;
then  b = g . a by A10, Def2;
then  ( b in dom f & a = f . b ) by A8, A9, A11;
then  [b,a] in f by Def2;
then  [a,b] in f ~ by RELAT_1:def_7;
hence  [a,b] in f " by A1, Def5; ::_thesis: verum
end;
assume  [a,b] in f " ; ::_thesis: [a,b] in g
then  [a,b] in f ~ by A1, Def5;
then A12: [b,a] in f by RELAT_1:def_7;
then A13: b in dom f by XTUPLE_0:def_12;
then  a = f . b by A12, Def2;
then  ( a in rng f & b = g . a ) by A9, A13;
hence  [a,b] in g by A8, Def2; ::_thesis: verum
end;

theorem Th33: :: FUNCT_1:33
for f being Function st f is one-to-one holds
( rng f = dom (f ") & dom f = rng (f ") )
proof
let f be Function; ::_thesis: ( f is one-to-one implies ( rng f = dom (f ") & dom f = rng (f ") ) )
assume  f is one-to-one ; ::_thesis: ( rng f = dom (f ") & dom f = rng (f ") )
then  f " = f ~ by Def5;
hence  ( rng f = dom (f ") & dom f = rng (f ") ) by RELAT_1:20; ::_thesis: verum
end;

theorem Th34: :: FUNCT_1:34
for x being set
for f being Function st f is one-to-one & x in dom f holds
( x = (f ") . (f . x) & x = ((f ") * f) . x )
proof
let x be set ; ::_thesis: for f being Function st f is one-to-one & x in dom f holds
( x = (f ") . (f . x) & x = ((f ") * f) . x )
let f be Function; ::_thesis: ( f is one-to-one & x in dom f implies ( x = (f ") . (f . x) & x = ((f ") * f) . x ) )
assume A1: f is one-to-one ; ::_thesis: ( not x in dom f or ( x = (f ") . (f . x) & x = ((f ") * f) . x ) )
assume A2: x in dom f ; ::_thesis: ( x = (f ") . (f . x) & x = ((f ") * f) . x )
hence  x = (f ") . (f . x) by A1, Th32; ::_thesis: x = ((f ") * f) . x
hence  x = ((f ") * f) . x by A2, Th13; ::_thesis: verum
end;

theorem Th35: :: FUNCT_1:35
for y being set
for f being Function st f is one-to-one & y in rng f holds
( y = f . ((f ") . y) & y = (f * (f ")) . y )
proof
let y be set ; ::_thesis: for f being Function st f is one-to-one & y in rng f holds
( y = f . ((f ") . y) & y = (f * (f ")) . y )
let f be Function; ::_thesis: ( f is one-to-one & y in rng f implies ( y = f . ((f ") . y) & y = (f * (f ")) . y ) )
assume A1: f is one-to-one ; ::_thesis: ( not y in rng f or ( y = f . ((f ") . y) & y = (f * (f ")) . y ) )
assume A2: y in rng f ; ::_thesis: ( y = f . ((f ") . y) & y = (f * (f ")) . y )
hence A3: y = f . ((f ") . y) by A1, Th32; ::_thesis: y = (f * (f ")) . y
 rng f = dom (f ") by A1, Th33;
hence  y = (f * (f ")) . y by A2, A3, Th13; ::_thesis: verum
end;

theorem Th36: :: FUNCT_1:36
for f being Function st f is one-to-one holds
( dom ((f ") * f) = dom f & rng ((f ") * f) = dom f )
proof
let f be Function; ::_thesis: ( f is one-to-one implies ( dom ((f ") * f) = dom f & rng ((f ") * f) = dom f ) )
assume A1: f is one-to-one ; ::_thesis: ( dom ((f ") * f) = dom f & rng ((f ") * f) = dom f )
then A2: rng f = dom (f ") by Th33;
then  rng ((f ") * f) = rng (f ") by RELAT_1:28;
hence  ( dom ((f ") * f) = dom f & rng ((f ") * f) = dom f ) by A1, A2, Th33, RELAT_1:27; ::_thesis: verum
end;

theorem Th37: :: FUNCT_1:37
for f being Function st f is one-to-one holds
( dom (f * (f ")) = rng f & rng (f * (f ")) = rng f )
proof
let f be Function; ::_thesis: ( f is one-to-one implies ( dom (f * (f ")) = rng f & rng (f * (f ")) = rng f ) )
assume A1: f is one-to-one ; ::_thesis: ( dom (f * (f ")) = rng f & rng (f * (f ")) = rng f )
then A2: rng (f ") = dom f by Th33;
then  dom (f * (f ")) = dom (f ") by RELAT_1:27;
hence  ( dom (f * (f ")) = rng f & rng (f * (f ")) = rng f ) by A1, A2, Th33, RELAT_1:28; ::_thesis: verum
end;

theorem :: FUNCT_1:38
for f, g being Function st f is one-to-one & dom f = rng g & rng f = dom g & ( for x, y being set st x in dom f & y in dom g holds
( f . x = y iff g . y = x ) ) holds
g = f "
proof
let f, g be Function; ::_thesis: ( f is one-to-one & dom f = rng g & rng f = dom g & ( for x, y being set st x in dom f & y in dom g holds
( f . x = y iff g . y = x ) ) implies g = f " )
assume that
A1: f is one-to-one and
A2: dom f = rng g and
A3: rng f = dom g and
A4: for x, y being set st x in dom f & y in dom g holds
( f . x = y iff g . y = x ) ; ::_thesis: g = f "
A5: for y being set st y in dom g holds
g . y = (f ") . y
proof
let y be set ; ::_thesis: ( y in dom g implies g . y = (f ") . y )
assume A6: y in dom g ; ::_thesis: g . y = (f ") . y
then A7: g . y in dom f by A2, Def3;
then  f . (g . y) = y by A4, A6;
hence  g . y = (f ") . y by A1, A7, Th32; ::_thesis: verum
end;
 rng f = dom (f ") by A1, Th32;
hence  g = f " by A3, A5, Th2; ::_thesis: verum
end;

theorem Th39: :: FUNCT_1:39
for f being Function st f is one-to-one holds
( (f ") * f = id (dom f) & f * (f ") = id (rng f) )
proof
let f be Function; ::_thesis: ( f is one-to-one implies ( (f ") * f = id (dom f) & f * (f ") = id (rng f) ) )
assume A1: f is one-to-one ; ::_thesis: ( (f ") * f = id (dom f) & f * (f ") = id (rng f) )
A2: for x being set st x in dom ((f ") * f) holds
((f ") * f) . x = x
proof
let x be set ; ::_thesis: ( x in dom ((f ") * f) implies ((f ") * f) . x = x )
assume  x in dom ((f ") * f) ; ::_thesis: ((f ") * f) . x = x
then  x in dom f by A1, Th36;
hence  ((f ") * f) . x = x by A1, Th34; ::_thesis: verum
end;
A3: for x being set st x in dom (f * (f ")) holds
(f * (f ")) . x = x
proof
let x be set ; ::_thesis: ( x in dom (f * (f ")) implies (f * (f ")) . x = x )
assume  x in dom (f * (f ")) ; ::_thesis: (f * (f ")) . x = x
then  x in rng f by A1, Th37;
hence  (f * (f ")) . x = x by A1, Th35; ::_thesis: verum
end;
 dom ((f ") * f) = dom f by A1, Th36;
hence  (f ") * f = id (dom f) by A2, Th17; ::_thesis: f * (f ") = id (rng f)
 dom (f * (f ")) = rng f by A1, Th37;
hence  f * (f ") = id (rng f) by A3, Th17; ::_thesis: verum
end;

theorem Th40: :: FUNCT_1:40
for f being Function st f is one-to-one holds
f " is one-to-one
proof
let f be Function; ::_thesis: ( f is one-to-one implies f " is one-to-one )
assume A1: f is one-to-one ; ::_thesis: f " is one-to-one
let y1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for x2 being set st y1 in dom (f ") & x2 in dom (f ") & (f ") . y1 = (f ") . x2 holds
y1 = x2
let y2 be set ; ::_thesis: ( y1 in dom (f ") & y2 in dom (f ") & (f ") . y1 = (f ") . y2 implies y1 = y2 )
assume that
A2: y1 in dom (f ") and
A3: y2 in dom (f ") ; ::_thesis: ( not (f ") . y1 = (f ") . y2 or y1 = y2 )
 y1 in rng f by A1, A2, Th32;
then A4: y1 = f . ((f ") . y1) by A1, Th35;
 y2 in rng f by A1, A3, Th32;
hence  ( not (f ") . y1 = (f ") . y2 or y1 = y2 ) by A1, A4, Th35; ::_thesis: verum
end;

registration
let f be one-to-one Function;
clusterf "  ->  one-to-one ;
coherence
 f " is one-to-one by Th40;
let g be one-to-one Function;
clusterg * f ->  one-to-one ;
coherence
 g * f is one-to-one by Th24;
end;

Lm1:  for X being set
for g2, f, g1 being Function st rng g2 = X & f * g2 = id (dom g1) & g1 * f = id X holds
g1 = g2
proof
let X be set ; ::_thesis: for g2, f, g1 being Function st rng g2 = X & f * g2 = id (dom g1) & g1 * f = id X holds
g1 = g2
let g2, f, g1 be Function; ::_thesis: ( rng g2 = X & f * g2 = id (dom g1) & g1 * f = id X implies g1 = g2 )
A1: ( g1 * (f * g2) = (g1 * f) * g2 & g1 * (id (dom g1)) = g1 ) by RELAT_1:36, RELAT_1:51;
assume  ( rng g2 = X & f * g2 = id (dom g1) & g1 * f = id X ) ; ::_thesis: g1 = g2
hence  g1 = g2 by A1, RELAT_1:53; ::_thesis: verum
end;

theorem Th41: :: FUNCT_1:41
for f, g being Function st f is one-to-one & rng f = dom g & g * f = id (dom f) holds
g = f "
proof
let f, g be Function; ::_thesis: ( f is one-to-one & rng f = dom g & g * f = id (dom f) implies g = f " )
assume that
A1: f is one-to-one and
A2: ( rng f = dom g & g * f = id (dom f) ) ; ::_thesis: g = f "
 ( f * (f ") = id (rng f) & rng (f ") = dom f ) by A1, Th33, Th39;
hence  g = f " by A2, Lm1; ::_thesis: verum
end;

theorem :: FUNCT_1:42
for f, g being Function st f is one-to-one & rng g = dom f & f * g = id (rng f) holds
g = f "
proof
let f, g be Function; ::_thesis: ( f is one-to-one & rng g = dom f & f * g = id (rng f) implies g = f " )
assume that
A1: f is one-to-one and
A2: ( rng g = dom f & f * g = id (rng f) ) ; ::_thesis: g = f "
 ( (f ") * f = id (dom f) & dom (f ") = rng f ) by A1, Th33, Th39;
hence  g = f " by A2, Lm1; ::_thesis: verum
end;

theorem :: FUNCT_1:43
for f being Function st f is one-to-one holds
(f ") " = f
proof
let f be Function; ::_thesis: ( f is one-to-one implies (f ") " = f )
assume A1: f is one-to-one ; ::_thesis: (f ") " = f
then  rng f = dom (f ") by Th33;
then A2: f * (f ") = id (dom (f ")) by A1, Th39;
 dom f = rng (f ") by A1, Th33;
hence  (f ") " = f by A1, A2, Th41; ::_thesis: verum
end;

theorem :: FUNCT_1:44
for f, g being Function st f is one-to-one & g is one-to-one holds
(g * f) " = (f ") * (g ")
proof
let f, g be Function; ::_thesis: ( f is one-to-one & g is one-to-one implies (g * f) " = (f ") * (g ") )
assume that
A1: f is one-to-one and
A2: g is one-to-one ; ::_thesis: (g * f) " = (f ") * (g ")
 for y being set holds
( y in rng (g * f) iff y in dom ((f ") * (g ")) )
proof
let y be set ; ::_thesis: ( y in rng (g * f) iff y in dom ((f ") * (g ")) )
thus  ( y in rng (g * f) implies y in dom ((f ") * (g ")) ) ::_thesis: ( y in dom ((f ") * (g ")) implies y in rng (g * f) )
proof
assume  y in rng (g * f) ; ::_thesis: y in dom ((f ") * (g "))
then consider x being set  such that
A3: x in dom (g * f) and
A4: y = (g * f) . x by Def3;
A5: f . x in dom g by A3, Th11;
A6: y = g . (f . x) by A3, A4, Th12;
then  y in rng g by A5, Def3;
then A7: y in dom (g ") by A2, Th32;
A8: x in dom f by A3, Th11;
(g ") . (g . (f . x)) = ((g ") * g) . (f . x) by A5, Th13
.= (id (dom g)) . (f . x) by A2, Th39
.= f . x by A5, Th17 ;
then  (g ") . y in rng f by A8, A6, Def3;
then  (g ") . y in dom (f ") by A1, Th32;
hence  y in dom ((f ") * (g ")) by A7, Th11; ::_thesis: verum
end;
assume A9: y in dom ((f ") * (g ")) ; ::_thesis: y in rng (g * f)
then  y in dom (g ") by Th11;
then  y in rng g by A2, Th32;
then consider z being set  such that
A10: z in dom g and
A11: y = g . z by Def3;
 (g ") . y in dom (f ") by A9, Th11;
then  (g ") . (g . z) in rng f by A1, A11, Th32;
then  ((g ") * g) . z in rng f by A10, Th13;
then  (id (dom g)) . z in rng f by A2, Th39;
then  z in rng f by A10, Th17;
then consider x being set  such that
A12: ( x in dom f & z = f . x ) by Def3;
 ( x in dom (g * f) & y = (g * f) . x ) by A10, A11, A12, Th11, Th13;
hence  y in rng (g * f) by Def3; ::_thesis: verum
end;
then A13: rng (g * f) = dom ((f ") * (g ")) by TARSKI:1;
 for x being set holds
( x in dom (((f ") * (g ")) * (g * f)) iff x in dom (g * f) )
proof
let x be set ; ::_thesis: ( x in dom (((f ") * (g ")) * (g * f)) iff x in dom (g * f) )
thus  ( x in dom (((f ") * (g ")) * (g * f)) implies x in dom (g * f) ) by Th11; ::_thesis: ( x in dom (g * f) implies x in dom (((f ") * (g ")) * (g * f)) )
assume A14: x in dom (g * f) ; ::_thesis: x in dom (((f ") * (g ")) * (g * f))
then  (g * f) . x in rng (g * f) by Def3;
hence  x in dom (((f ") * (g ")) * (g * f)) by A13, A14, Th11; ::_thesis: verum
end;
then A15: dom (((f ") * (g ")) * (g * f)) = dom (g * f) by TARSKI:1;
 for x being set st x in dom (g * f) holds
(((f ") * (g ")) * (g * f)) . x = x
proof
let x be set ; ::_thesis: ( x in dom (g * f) implies (((f ") * (g ")) * (g * f)) . x = x )
assume A16: x in dom (g * f) ; ::_thesis: (((f ") * (g ")) * (g * f)) . x = x
then A17: f . x in dom g by Th11;
 (g * f) . x in rng (g * f) by A16, Def3;
then A18: g . (f . x) in dom ((f ") * (g ")) by A13, A16, Th12;
A19: x in dom f by A16, Th11;
thus (((f ") * (g ")) * (g * f)) . x = ((f ") * (g ")) . ((g * f) . x) by A15, A16, Th12
.= ((f ") * (g ")) . (g . (f . x)) by A16, Th12
.= (f ") . ((g ") . (g . (f . x))) by A18, Th12
.= (f ") . (((g ") * g) . (f . x)) by A17, Th13
.= (f ") . ((id (dom g)) . (f . x)) by A2, Th39
.= (f ") . (f . x) by A17, Th17
.= x by A1, A19, Th34 ; ::_thesis: verum
end;
then  ((f ") * (g ")) * (g * f) = id (dom (g * f)) by A15, Th17;
hence  (g * f) " = (f ") * (g ") by A1, A2, A13, Th41; ::_thesis: verum
end;

theorem :: FUNCT_1:45
for X being set holds (id X) " = id X
proof
let X be set ; ::_thesis: (id X) " = id X
 dom (id X) = X ;
then A1: ((id X) ") * (id X) = id X by Th39;
 ( dom ((id X) ") = rng (id X) & rng (id X) = X ) by Th33;
hence  (id X) " = id X by A1, Th23; ::_thesis: verum
end;

registration
let f be Function;
let X be set ;
clusterf | X ->  Function-like ;
coherence
 f | X is Function-like
proof
let x be set ; :: according to FUNCT_1:def_1 ::_thesis: for y1, y2 being set st [x,y1] in f | X & [x,y2] in f | X holds
y1 = y2
let y1, y2 be set ; ::_thesis: ( [x,y1] in f | X & [x,y2] in f | X implies y1 = y2 )
assume  ( [x,y1] in f | X & [x,y2] in f | X ) ; ::_thesis: y1 = y2
then  ( [x,y1] in f & [x,y2] in f ) by RELAT_1:def_11;
hence  y1 = y2 by Def1; ::_thesis: verum
end;
end;

theorem :: FUNCT_1:46
for X being set
for g, f being Function st dom g = (dom f) /\ X & ( for x being set st x in dom g holds
g . x = f . x ) holds
g = f | X
proof
let X be set ; ::_thesis: for g, f being Function st dom g = (dom f) /\ X & ( for x being set st x in dom g holds
g . x = f . x ) holds
g = f | X
let g, f be Function; ::_thesis: ( dom g = (dom f) /\ X & ( for x being set st x in dom g holds
g . x = f . x ) implies g = f | X )
assume that
A1: dom g = (dom f) /\ X and
A2: for x being set st x in dom g holds
g . x = f . x ; ::_thesis: g = f | X
now__::_thesis:_for_x,_y_being_set_holds_
(_(_[x,y]_in_g_implies_(_x_in_X_&_[x,y]_in_f_)_)_&_(_x_in_X_&_[x,y]_in_f_implies_[x,y]_in_g_)_)
let x, y be set ; ::_thesis: ( ( [x,y] in g implies ( x in X & [x,y] in f ) ) & ( x in X & [x,y] in f implies [x,y] in g ) )
hereby  ::_thesis: ( x in X & [x,y] in f implies [x,y] in g )
assume A3: [x,y] in g ; ::_thesis: ( x in X & [x,y] in f )
then A4: x in dom g by XTUPLE_0:def_12;
hence  x in X by A1, XBOOLE_0:def_4; ::_thesis: [x,y] in f
A5: x in dom f by A1, A4, XBOOLE_0:def_4;
y = g . x by A3, A4, Def2
.= f . x by A2, A4 ;
hence  [x,y] in f by A5, Def2; ::_thesis: verum
end;
assume A6: x in X ; ::_thesis: ( [x,y] in f implies [x,y] in g )
assume A7: [x,y] in f ; ::_thesis: [x,y] in g
then A8: x in dom f by XTUPLE_0:def_12;
then A9: x in dom g by A1, A6, XBOOLE_0:def_4;
y = f . x by A7, A8, Def2
.= g . x by A2, A9 ;
hence  [x,y] in g by A9, Def2; ::_thesis: verum
end;
hence  g = f | X by RELAT_1:def_11; ::_thesis: verum
end;

theorem Th47: :: FUNCT_1:47
for x, X being set
for f being Function st x in dom (f | X) holds
(f | X) . x = f . x
proof
let x, X be set ; ::_thesis: for f being Function st x in dom (f | X) holds
(f | X) . x = f . x
let f be Function; ::_thesis: ( x in dom (f | X) implies (f | X) . x = f . x )
set g = f | X;
assume A1: x in dom (f | X) ; ::_thesis: (f | X) . x = f . x
 dom (f | X) = (dom f) /\ X by RELAT_1:61;
then A2: x in dom f by A1, XBOOLE_0:def_4;
 ( f | X c= f & [x,((f | X) . x)] in f | X ) by A1, Def2, RELAT_1:59;
hence  (f | X) . x = f . x by A2, Def2; ::_thesis: verum
end;

theorem Th48: :: FUNCT_1:48
for x, X being set
for f being Function st x in (dom f) /\ X holds
(f | X) . x = f . x
proof
let x, X be set ; ::_thesis: for f being Function st x in (dom f) /\ X holds
(f | X) . x = f . x
let f be Function; ::_thesis: ( x in (dom f) /\ X implies (f | X) . x = f . x )
assume  x in (dom f) /\ X ; ::_thesis: (f | X) . x = f . x
then  x in dom (f | X) by RELAT_1:61;
hence  (f | X) . x = f . x by Th47; ::_thesis: verum
end;

theorem Th49: :: FUNCT_1:49
for x, X being set
for f being Function st x in X holds
(f | X) . x = f . x
proof
let x, X be set ; ::_thesis: for f being Function st x in X holds
(f | X) . x = f . x
let f be Function; ::_thesis: ( x in X implies (f | X) . x = f . x )
assume A1: x in X ; ::_thesis: (f | X) . x = f . x
percases ( x in dom f or not x in dom f ) ;
suppose x in dom f ; ::_thesis: (f | X) . x = f . x
then  x in dom (f | X) by A1, RELAT_1:57;
hence  (f | X) . x = f . x by Th47; ::_thesis: verum
end;
supposeA2: not x in dom f ; ::_thesis: (f | X) . x = f . x
then  not x in dom (f | X) by RELAT_1:57;
hence (f | X) . x = {} by Def2
.= f . x by A2, Def2 ;
::_thesis: verum
end;
end;
end;

theorem :: FUNCT_1:50
for x, X being set
for f being Function st x in dom f & x in X holds
f . x in rng (f | X)
proof
let x, X be set ; ::_thesis: for f being Function st x in dom f & x in X holds
f . x in rng (f | X)
let f be Function; ::_thesis: ( x in dom f & x in X implies f . x in rng (f | X) )
assume that
A1: x in dom f and
A2: x in X ; ::_thesis: f . x in rng (f | X)
 x in (dom f) /\ X by A1, A2, XBOOLE_0:def_4;
then A3: x in dom (f | X) by RELAT_1:61;
 (f | X) . x = f . x by A2, Th49;
hence  f . x in rng (f | X) by A3, Def3; ::_thesis: verum
end;

theorem :: FUNCT_1:51
for X, Y being set
for f being Function st X c= Y holds
( (f | X) | Y = f | X & (f | Y) | X = f | X ) by RELAT_1:73, RELAT_1:74;

theorem :: FUNCT_1:52
for X being set
for f being Function st f is one-to-one holds
f | X is one-to-one
proof
let X be set ; ::_thesis: for f being Function st f is one-to-one holds
f | X is one-to-one
let f be Function; ::_thesis: ( f is one-to-one implies f | X is one-to-one )
assume A1: f is one-to-one ; ::_thesis: f | X is one-to-one
let x1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for x2 being set st x1 in dom (f | X) & x2 in dom (f | X) & (f | X) . x1 = (f | X) . x2 holds
x1 = x2
let x2 be set ; ::_thesis: ( x1 in dom (f | X) & x2 in dom (f | X) & (f | X) . x1 = (f | X) . x2 implies x1 = x2 )
assume that
A2: x1 in dom (f | X) and
A3: x2 in dom (f | X) ; ::_thesis: ( not (f | X) . x1 = (f | X) . x2 or x1 = x2 )
 x1 in (dom f) /\ X by A2, RELAT_1:61;
then A4: x1 in dom f by XBOOLE_0:def_4;
 x2 in (dom f) /\ X by A3, RELAT_1:61;
then A5: x2 in dom f by XBOOLE_0:def_4;
 ( (f | X) . x1 = f . x1 & (f | X) . x2 = f . x2 ) by A2, A3, Th47;
hence  ( not (f | X) . x1 = (f | X) . x2 or x1 = x2 ) by A1, A4, A5, Def4; ::_thesis: verum
end;

registration
let Y be set ;
let f be Function;
clusterY |` f ->  Function-like ;
coherence
 Y |` f is Function-like
proof
let x be set ; :: according to FUNCT_1:def_1 ::_thesis: for y1, y2 being set st [x,y1] in Y |` f & [x,y2] in Y |` f holds
y1 = y2
let y1, y2 be set ; ::_thesis: ( [x,y1] in Y |` f & [x,y2] in Y |` f implies y1 = y2 )
assume  ( [x,y1] in Y |` f & [x,y2] in Y |` f ) ; ::_thesis: y1 = y2
then  ( [x,y1] in f & [x,y2] in f ) by RELAT_1:def_12;
hence  y1 = y2 by Def1; ::_thesis: verum
end;
end;

theorem Th53: :: FUNCT_1:53
for Y being set
for g, f being Function holds
( g = Y |` f iff ( ( for x being set holds
( x in dom g iff ( x in dom f & f . x in Y ) ) ) & ( for x being set st x in dom g holds
g . x = f . x ) ) )
proof
let Y be set ; ::_thesis: for g, f being Function holds
( g = Y |` f iff ( ( for x being set holds
( x in dom g iff ( x in dom f & f . x in Y ) ) ) & ( for x being set st x in dom g holds
g . x = f . x ) ) )
let g, f be Function; ::_thesis: ( g = Y |` f iff ( ( for x being set holds
( x in dom g iff ( x in dom f & f . x in Y ) ) ) & ( for x being set st x in dom g holds
g . x = f . x ) ) )
hereby  ::_thesis: ( ( for x being set holds
( x in dom g iff ( x in dom f & f . x in Y ) ) ) & ( for x being set st x in dom g holds
g . x = f . x ) implies g = Y |` f )
assume A1: g = Y |` f ; ::_thesis: ( ( for x being set holds
( ( x in dom g implies ( x in dom f & f . x in Y ) ) & ( x in dom f & f . x in Y implies x in dom g ) ) ) & ( for x being set st x in dom g holds
f . x = g . x ) )
hereby  ::_thesis: for x being set st x in dom g holds
f . x = g . x
let x be set ; ::_thesis: ( ( x in dom g implies ( x in dom f & f . x in Y ) ) & ( x in dom f & f . x in Y implies x in dom g ) )
hereby  ::_thesis: ( x in dom f & f . x in Y implies x in dom g )
assume  x in dom g ; ::_thesis: ( x in dom f & f . x in Y )
then A2: [x,(g . x)] in g by Def2;
then A3: [x,(g . x)] in f by A1, RELAT_1:def_12;
hence  x in dom f by XTUPLE_0:def_12; ::_thesis: f . x in Y
then  f . x = g . x by A3, Def2;
hence  f . x in Y by A1, A2, RELAT_1:def_12; ::_thesis: verum
end;
assume  x in dom f ; ::_thesis: ( f . x in Y implies x in dom g )
then A4: [x,(f . x)] in f by Def2;
assume  f . x in Y ; ::_thesis: x in dom g
then  [x,(f . x)] in g by A1, A4, RELAT_1:def_12;
hence  x in dom g by XTUPLE_0:def_12; ::_thesis: verum
end;
let x be set ; ::_thesis: ( x in dom g implies f . x = g . x )
assume  x in dom g ; ::_thesis: f . x = g . x
then  [x,(g . x)] in g by Def2;
then A5: [x,(g . x)] in f by A1, RELAT_1:def_12;
then  x in dom f by XTUPLE_0:def_12;
hence  f . x = g . x by A5, Def2; ::_thesis: verum
end;
assume that
A6: for x being set holds
( x in dom g iff ( x in dom f & f . x in Y ) ) and
A7: for x being set st x in dom g holds
g . x = f . x ; ::_thesis: g = Y |` f
now__::_thesis:_for_x,_y_being_set_holds_
(_(_[x,y]_in_g_implies_(_y_in_Y_&_[x,y]_in_f_)_)_&_(_y_in_Y_&_[x,y]_in_f_implies_[x,y]_in_g_)_)
let x, y be set ; ::_thesis: ( ( [x,y] in g implies ( y in Y & [x,y] in f ) ) & ( y in Y & [x,y] in f implies [x,y] in g ) )
hereby  ::_thesis: ( y in Y & [x,y] in f implies [x,y] in g )
assume A8: [x,y] in g ; ::_thesis: ( y in Y & [x,y] in f )
then A9: x in dom g by XTUPLE_0:def_12;
then A10: y = g . x by A8, Def2
.= f . x by A7, A9 ;
hence  y in Y by A6, A9; ::_thesis: [x,y] in f
 x in dom f by A6, A9;
hence  [x,y] in f by A10, Def2; ::_thesis: verum
end;
assume A11: y in Y ; ::_thesis: ( [x,y] in f implies [x,y] in g )
assume A12: [x,y] in f ; ::_thesis: [x,y] in g
then A13: y = f . x by Th1;
 x in dom f by A12, XTUPLE_0:def_12;
then A14: x in dom g by A6, A11, A13;
then  y = g . x by A7, A13;
hence  [x,y] in g by A14, Def2; ::_thesis: verum
end;
hence  g = Y |` f by RELAT_1:def_12; ::_thesis: verum
end;

theorem :: FUNCT_1:54
for x, Y being set
for f being Function holds
( x in dom (Y |` f) iff ( x in dom f & f . x in Y ) ) by Th53;

theorem :: FUNCT_1:55
for x, Y being set
for f being Function st x in dom (Y |` f) holds
(Y |` f) . x = f . x by Th53;

theorem :: FUNCT_1:56
for Y being set
for f being Function holds dom (Y |` f) c= dom f
proof
let Y be set ; ::_thesis: for f being Function holds dom (Y |` f) c= dom f
let f be Function; ::_thesis: dom (Y |` f) c= dom f
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (Y |` f) or x in dom f )
thus  ( not x in dom (Y |` f) or x in dom f ) by Th53; ::_thesis: verum
end;

theorem :: FUNCT_1:57
for X, Y being set
for f being Function st X c= Y holds
( Y |` (X |` f) = X |` f & X |` (Y |` f) = X |` f ) by RELAT_1:98, RELAT_1:99;

theorem :: FUNCT_1:58
for Y being set
for f being Function st f is one-to-one holds
Y |` f is one-to-one
proof
let Y be set ; ::_thesis: for f being Function st f is one-to-one holds
Y |` f is one-to-one
let f be Function; ::_thesis: ( f is one-to-one implies Y |` f is one-to-one )
assume A1: f is one-to-one ; ::_thesis: Y |` f is one-to-one
let x1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for x2 being set st x1 in dom (Y |` f) & x2 in dom (Y |` f) & (Y |` f) . x1 = (Y |` f) . x2 holds
x1 = x2
let x2 be set ; ::_thesis: ( x1 in dom (Y |` f) & x2 in dom (Y |` f) & (Y |` f) . x1 = (Y |` f) . x2 implies x1 = x2 )
assume that
A2: ( x1 in dom (Y |` f) & x2 in dom (Y |` f) ) and
A3: (Y |` f) . x1 = (Y |` f) . x2 ; ::_thesis: x1 = x2
A4: ( x1 in dom f & x2 in dom f ) by A2, Th53;
 ( (Y |` f) . x1 = f . x1 & (Y |` f) . x2 = f . x2 ) by A2, Th53;
hence  x1 = x2 by A1, A3, A4, Def4; ::_thesis: verum
end;

definition
let f be Function;
let X be set ;
redefine func f .: X means :Def6: :: FUNCT_1:def 6
 for y being set holds
( y in it iff ex x being set st
( x in dom f & x in X & y = f . x ) );
compatibility
 for b1 being set holds
( b1 = f .: X iff for y being set holds
( y in b1 iff ex x being set st
( x in dom f & x in X & y = f . x ) ) )
proof
let Y be set ; ::_thesis: ( Y = f .: X iff for y being set holds
( y in Y iff ex x being set st
( x in dom f & x in X & y = f . x ) ) )
hereby  ::_thesis: ( ( for y being set holds
( y in Y iff ex x being set st
( x in dom f & x in X & y = f . x ) ) ) implies Y = f .: X )
assume A1: Y = f .: X ; ::_thesis: for y being set holds
( ( y in Y implies ex x being set st
( x in dom f & x in X & y = f . x ) ) & ( ex x being set st
( x in dom f & x in X & y = f . x ) implies y in Y ) )
let y be set ; ::_thesis: ( ( y in Y implies ex x being set st
( x in dom f & x in X & y = f . x ) ) & ( ex x being set st
( x in dom f & x in X & y = f . x ) implies y in Y ) )
hereby  ::_thesis: ( ex x being set st
( x in dom f & x in X & y = f . x ) implies y in Y )
assume  y in Y ; ::_thesis: ex x being set st
( x in dom f & x in X & y = f . x )
then consider x being set  such that
A2: [x,y] in f and
A3: x in X by A1, RELAT_1:def_13;
take x = x; ::_thesis: ( x in dom f & x in X & y = f . x )
thus A4: x in dom f by A2, XTUPLE_0:def_12; ::_thesis: ( x in X & y = f . x )
thus  x in X by A3; ::_thesis: y = f . x
thus  y = f . x by A2, A4, Def2; ::_thesis: verum
end;
given x being set  such that A5: x in dom f and
A6: x in X and
A7: y = f . x ; ::_thesis: y in Y
 [x,y] in f by A5, A7, Def2;
hence  y in Y by A1, A6, RELAT_1:def_13; ::_thesis: verum
end;
assume A8: for y being set holds
( y in Y iff ex x being set st
( x in dom f & x in X & y = f . x ) ) ; ::_thesis: Y = f .: X
now__::_thesis:_for_y_being_set_holds_
(_(_y_in_Y_implies_ex_x_being_set_st_
(_[x,y]_in_f_&_x_in_X_)_)_&_(_ex_x_being_set_st_
(_[x,y]_in_f_&_x_in_X_)_implies_y_in_Y_)_)
let y be set ; ::_thesis: ( ( y in Y implies ex x being set st
( [x,y] in f & x in X ) ) & ( ex x being set st
( [x,y] in f & x in X ) implies y in Y ) )
hereby  ::_thesis: ( ex x being set st
( [x,y] in f & x in X ) implies y in Y )
assume  y in Y ; ::_thesis: ex x being set st
( [x,y] in f & x in X )
then consider x being set  such that
A9: x in dom f and
A10: x in X and
A11: y = f . x by A8;
take x = x; ::_thesis: ( [x,y] in f & x in X )
thus  [x,y] in f by A9, A11, Def2; ::_thesis: x in X
thus  x in X by A10; ::_thesis: verum
end;
given x being set  such that A12: [x,y] in f and
A13: x in X ; ::_thesis: y in Y
 ( x in dom f & y = f . x ) by A12, Th1;
hence  y in Y by A8, A13; ::_thesis: verum
end;
hence  Y = f .: X by RELAT_1:def_13; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines .: FUNCT_1:def_6_:_
 for f being Function
for X being set
for b3 being set holds
( b3 = f .: X iff for y being set holds
( y in b3 iff ex x being set st
( x in dom f & x in X & y = f . x ) ) );

theorem Th59: :: FUNCT_1:59
for x being set
for f being Function st x in dom f holds
Im (f,x) = {(f . x)}
proof
let x be set ; ::_thesis: for f being Function st x in dom f holds
Im (f,x) = {(f . x)}
let f be Function; ::_thesis: ( x in dom f implies Im (f,x) = {(f . x)} )
assume A1: x in dom f ; ::_thesis: Im (f,x) = {(f . x)}
 for y being set holds
( y in f .: {x} iff y in {(f . x)} )
proof
let y be set ; ::_thesis: ( y in f .: {x} iff y in {(f . x)} )
thus  ( y in f .: {x} implies y in {(f . x)} ) ::_thesis: ( y in {(f . x)} implies y in f .: {x} )
proof
assume  y in f .: {x} ; ::_thesis: y in {(f . x)}
then consider z being set  such that
 z in dom f and
A2: z in {x} and
A3: y = f . z by Def6;
 z = x by A2, TARSKI:def_1;
hence  y in {(f . x)} by A3, TARSKI:def_1; ::_thesis: verum
end;
assume  y in {(f . x)} ; ::_thesis: y in f .: {x}
then A4: y = f . x by TARSKI:def_1;
 x in {x} by TARSKI:def_1;
hence  y in f .: {x} by A1, A4, Def6; ::_thesis: verum
end;
hence  Im (f,x) = {(f . x)} by TARSKI:1; ::_thesis: verum
end;

theorem :: FUNCT_1:60
for x1, x2 being set
for f being Function st x1 in dom f & x2 in dom f holds
f .: {x1,x2} = {(f . x1),(f . x2)}
proof
let x1, x2 be set ; ::_thesis: for f being Function st x1 in dom f & x2 in dom f holds
f .: {x1,x2} = {(f . x1),(f . x2)}
let f be Function; ::_thesis: ( x1 in dom f & x2 in dom f implies f .: {x1,x2} = {(f . x1),(f . x2)} )
assume A1: ( x1 in dom f & x2 in dom f ) ; ::_thesis: f .: {x1,x2} = {(f . x1),(f . x2)}
 for y being set holds
( y in f .: {x1,x2} iff ( y = f . x1 or y = f . x2 ) )
proof
let y be set ; ::_thesis: ( y in f .: {x1,x2} iff ( y = f . x1 or y = f . x2 ) )
A2: ( x1 in {x1,x2} & x2 in {x1,x2} ) by TARSKI:def_2;
thus  ( not y in f .: {x1,x2} or y = f . x1 or y = f . x2 ) ::_thesis: ( ( y = f . x1 or y = f . x2 ) implies y in f .: {x1,x2} )
proof
assume  y in f .: {x1,x2} ; ::_thesis: ( y = f . x1 or y = f . x2 )
then  ex x being set st
( x in dom f & x in {x1,x2} & y = f . x ) by Def6;
hence  ( y = f . x1 or y = f . x2 ) by TARSKI:def_2; ::_thesis: verum
end;
assume  ( y = f . x1 or y = f . x2 ) ; ::_thesis: y in f .: {x1,x2}
hence  y in f .: {x1,x2} by A1, A2, Def6; ::_thesis: verum
end;
hence  f .: {x1,x2} = {(f . x1),(f . x2)} by TARSKI:def_2; ::_thesis: verum
end;

theorem :: FUNCT_1:61
for Y, X being set
for f being Function holds (Y |` f) .: X c= f .: X
proof
let Y, X be set ; ::_thesis: for f being Function holds (Y |` f) .: X c= f .: X
let f be Function; ::_thesis: (Y |` f) .: X c= f .: X
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (Y |` f) .: X or y in f .: X )
assume  y in (Y |` f) .: X ; ::_thesis: y in f .: X
then consider x being set  such that
A1: x in dom (Y |` f) and
A2: x in X and
A3: y = (Y |` f) . x by Def6;
 ( y = f . x & x in dom f ) by A1, A3, Th53;
hence  y in f .: X by A2, Def6; ::_thesis: verum
end;

theorem Th62: :: FUNCT_1:62
for X1, X2 being set
for f being Function st f is one-to-one holds
f .: (X1 /\ X2) = (f .: X1) /\ (f .: X2)
proof
let X1, X2 be set ; ::_thesis: for f being Function st f is one-to-one holds
f .: (X1 /\ X2) = (f .: X1) /\ (f .: X2)
let f be Function; ::_thesis: ( f is one-to-one implies f .: (X1 /\ X2) = (f .: X1) /\ (f .: X2) )
assume A1: f is one-to-one ; ::_thesis: f .: (X1 /\ X2) = (f .: X1) /\ (f .: X2)
A2: (f .: X1) /\ (f .: X2) c= f .: (X1 /\ X2)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (f .: X1) /\ (f .: X2) or y in f .: (X1 /\ X2) )
assume A3: y in (f .: X1) /\ (f .: X2) ; ::_thesis: y in f .: (X1 /\ X2)
then  y in f .: X1 by XBOOLE_0:def_4;
then consider x1 being set  such that
A4: x1 in dom f and
A5: x1 in X1 and
A6: y = f . x1 by Def6;
 y in f .: X2 by A3, XBOOLE_0:def_4;
then consider x2 being set  such that
A7: x2 in dom f and
A8: x2 in X2 and
A9: y = f . x2 by Def6;
 x1 = x2 by A1, A4, A6, A7, A9, Def4;
then  x1 in X1 /\ X2 by A5, A8, XBOOLE_0:def_4;
hence  y in f .: (X1 /\ X2) by A4, A6, Def6; ::_thesis: verum
end;
 f .: (X1 /\ X2) c= (f .: X1) /\ (f .: X2) by RELAT_1:121;
hence  f .: (X1 /\ X2) = (f .: X1) /\ (f .: X2) by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: FUNCT_1:63
for f being Function st ( for X1, X2 being set holds f .: (X1 /\ X2) = (f .: X1) /\ (f .: X2) ) holds
f is one-to-one
proof
let f be Function; ::_thesis: ( ( for X1, X2 being set holds f .: (X1 /\ X2) = (f .: X1) /\ (f .: X2) ) implies f is one-to-one )
assume A1: for X1, X2 being set holds f .: (X1 /\ X2) = (f .: X1) /\ (f .: X2) ; ::_thesis: f is one-to-one
given x1, x2 being set  such that A2: ( x1 in dom f & x2 in dom f ) and
A3: f . x1 = f . x2 and
A4: x1 <> x2 ; :: according to FUNCT_1:def_4 ::_thesis: contradiction
A5: f .: ({x1} /\ {x2}) = (f .: {x1}) /\ (f .: {x2}) by A1;
 {x1} misses {x2} by A4, ZFMISC_1:11;
then A6: {x1} /\ {x2} = {} by XBOOLE_0:def_7;
 ( Im (f,x1) = {(f . x1)} & Im (f,x2) = {(f . x2)} ) by A2, Th59;
hence  contradiction by A3, A6, A5; ::_thesis: verum
end;

theorem :: FUNCT_1:64
for X1, X2 being set
for f being Function st f is one-to-one holds
f .: (X1 \ X2) = (f .: X1) \ (f .: X2)
proof
let X1, X2 be set ; ::_thesis: for f being Function st f is one-to-one holds
f .: (X1 \ X2) = (f .: X1) \ (f .: X2)
let f be Function; ::_thesis: ( f is one-to-one implies f .: (X1 \ X2) = (f .: X1) \ (f .: X2) )
assume A1: f is one-to-one ; ::_thesis: f .: (X1 \ X2) = (f .: X1) \ (f .: X2)
A2: f .: (X1 \ X2) c= (f .: X1) \ (f .: X2)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: (X1 \ X2) or y in (f .: X1) \ (f .: X2) )
assume  y in f .: (X1 \ X2) ; ::_thesis: y in (f .: X1) \ (f .: X2)
then consider x being set  such that
A3: x in dom f and
A4: x in X1 \ X2 and
A5: y = f . x by Def6;
A6: not x in X2 by A4, XBOOLE_0:def_5;
A7: now__::_thesis:_not_y_in_f_.:_X2
assume  y in f .: X2 ; ::_thesis: contradiction
then  ex z being set st
( z in dom f & z in X2 & y = f . z ) by Def6;
hence  contradiction by A1, A3, A5, A6, Def4; ::_thesis: verum
end;
 y in f .: X1 by A3, A4, A5, Def6;
hence  y in (f .: X1) \ (f .: X2) by A7, XBOOLE_0:def_5; ::_thesis: verum
end;
 (f .: X1) \ (f .: X2) c= f .: (X1 \ X2) by RELAT_1:122;
hence  f .: (X1 \ X2) = (f .: X1) \ (f .: X2) by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: FUNCT_1:65
for f being Function st ( for X1, X2 being set holds f .: (X1 \ X2) = (f .: X1) \ (f .: X2) ) holds
f is one-to-one
proof
let f be Function; ::_thesis: ( ( for X1, X2 being set holds f .: (X1 \ X2) = (f .: X1) \ (f .: X2) ) implies f is one-to-one )
assume A1: for X1, X2 being set holds f .: (X1 \ X2) = (f .: X1) \ (f .: X2) ; ::_thesis: f is one-to-one
given x1, x2 being set  such that A2: ( x1 in dom f & x2 in dom f ) and
A3: f . x1 = f . x2 and
A4: x1 <> x2 ; :: according to FUNCT_1:def_4 ::_thesis: contradiction
A5: f .: ({x1} \ {x2}) = f .: {x1} by A4, ZFMISC_1:14;
A6: f .: ({x1} \ {x2}) = (f .: {x1}) \ (f .: {x2}) by A1;
 ( Im (f,x1) = {(f . x1)} & Im (f,x2) = {(f . x2)} ) by A2, Th59;
hence  contradiction by A3, A5, A6, XBOOLE_1:37; ::_thesis: verum
end;

theorem :: FUNCT_1:66
for X, Y being set
for f being Function st X misses Y & f is one-to-one holds
f .: X misses f .: Y
proof
let X, Y be set ; ::_thesis: for f being Function st X misses Y & f is one-to-one holds
f .: X misses f .: Y
let f be Function; ::_thesis: ( X misses Y & f is one-to-one implies f .: X misses f .: Y )
assume  ( X /\ Y = {} & f is one-to-one ) ; :: according to XBOOLE_0:def_7 ::_thesis: f .: X misses f .: Y
then  ( f .: (X /\ Y) = {} & f .: (X /\ Y) = (f .: X) /\ (f .: Y) ) by Th62;
hence  f .: X misses f .: Y by XBOOLE_0:def_7; ::_thesis: verum
end;

theorem :: FUNCT_1:67
for Y, X being set
for f being Function holds (Y |` f) .: X = Y /\ (f .: X)
proof
let Y, X be set ; ::_thesis: for f being Function holds (Y |` f) .: X = Y /\ (f .: X)
let f be Function; ::_thesis: (Y |` f) .: X = Y /\ (f .: X)
 for y being set holds
( y in (Y |` f) .: X iff y in Y /\ (f .: X) )
proof
let y be set ; ::_thesis: ( y in (Y |` f) .: X iff y in Y /\ (f .: X) )
thus  ( y in (Y |` f) .: X implies y in Y /\ (f .: X) ) ::_thesis: ( y in Y /\ (f .: X) implies y in (Y |` f) .: X )
proof
assume  y in (Y |` f) .: X ; ::_thesis: y in Y /\ (f .: X)
then consider x being set  such that
A1: x in dom (Y |` f) and
A2: x in X and
A3: y = (Y |` f) . x by Def6;
A4: y = f . x by A1, A3, Th53;
then A5: y in Y by A1, Th53;
 x in dom f by A1, Th53;
then  y in f .: X by A2, A4, Def6;
hence  y in Y /\ (f .: X) by A5, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A6: y in Y /\ (f .: X) ; ::_thesis: y in (Y |` f) .: X
then  y in f .: X by XBOOLE_0:def_4;
then consider x being set  such that
A7: x in dom f and
A8: x in X and
A9: y = f . x by Def6;
 y in Y by A6, XBOOLE_0:def_4;
then A10: x in dom (Y |` f) by A7, A9, Th53;
then  (Y |` f) . x = f . x by Th53;
hence  y in (Y |` f) .: X by A8, A9, A10, Def6; ::_thesis: verum
end;
hence  (Y |` f) .: X = Y /\ (f .: X) by TARSKI:1; ::_thesis: verum
end;

definition
let f be Function;
let Y be set ;
redefine func f " Y means :Def7: :: FUNCT_1:def 7
 for x being set holds
( x in it iff ( x in dom f & f . x in Y ) );
compatibility
 for b1 being set holds
( b1 = f " Y iff for x being set holds
( x in b1 iff ( x in dom f & f . x in Y ) ) )
proof
let X be set ; ::_thesis: ( X = f " Y iff for x being set holds
( x in X iff ( x in dom f & f . x in Y ) ) )
hereby  ::_thesis: ( ( for x being set holds
( x in X iff ( x in dom f & f . x in Y ) ) ) implies X = f " Y )
assume A1: X = f " Y ; ::_thesis: for x being set holds
( ( x in X implies ( x in dom f & f . x in Y ) ) & ( x in dom f & f . x in Y implies x in X ) )
let x be set ; ::_thesis: ( ( x in X implies ( x in dom f & f . x in Y ) ) & ( x in dom f & f . x in Y implies x in X ) )
hereby  ::_thesis: ( x in dom f & f . x in Y implies x in X )
assume  x in X ; ::_thesis: ( x in dom f & f . x in Y )
then A2: ex y being set st
( [x,y] in f & y in Y ) by A1, RELAT_1:def_14;
hence  x in dom f by XTUPLE_0:def_12; ::_thesis: f . x in Y
thus  f . x in Y by A2, Th1; ::_thesis: verum
end;
assume that
A3: x in dom f and
A4: f . x in Y ; ::_thesis: x in X
 [x,(f . x)] in f by A3, Th1;
hence  x in X by A1, A4, RELAT_1:def_14; ::_thesis: verum
end;
assume A5: for x being set holds
( x in X iff ( x in dom f & f . x in Y ) ) ; ::_thesis: X = f " Y
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_X_implies_ex_y_being_set_st_
(_[x,y]_in_f_&_y_in_Y_)_)_&_(_ex_y_being_set_st_
(_[x,y]_in_f_&_y_in_Y_)_implies_x_in_X_)_)
let x be set ; ::_thesis: ( ( x in X implies ex y being set st
( [x,y] in f & y in Y ) ) & ( ex y being set st
( [x,y] in f & y in Y ) implies x in X ) )
hereby  ::_thesis: ( ex y being set st
( [x,y] in f & y in Y ) implies x in X )
assume A6: x in X ; ::_thesis: ex y being set st
( [x,y] in f & y in Y )
take y = f . x; ::_thesis: ( [x,y] in f & y in Y )
 x in dom f by A5, A6;
hence  [x,y] in f by Def2; ::_thesis: y in Y
thus  y in Y by A5, A6; ::_thesis: verum
end;
given y being set  such that A7: [x,y] in f and
A8: y in Y ; ::_thesis: x in X
 ( x in dom f & y = f . x ) by A7, Th1;
hence  x in X by A5, A8; ::_thesis: verum
end;
hence  X = f " Y by RELAT_1:def_14; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines " FUNCT_1:def_7_:_
 for f being Function
for Y being set
for b3 being set holds
( b3 = f " Y iff for x being set holds
( x in b3 iff ( x in dom f & f . x in Y ) ) );

theorem Th68: :: FUNCT_1:68
for Y1, Y2 being set
for f being Function holds f " (Y1 /\ Y2) = (f " Y1) /\ (f " Y2)
proof
let Y1, Y2 be set ; ::_thesis: for f being Function holds f " (Y1 /\ Y2) = (f " Y1) /\ (f " Y2)
let f be Function; ::_thesis: f " (Y1 /\ Y2) = (f " Y1) /\ (f " Y2)
 for x being set holds
( x in f " (Y1 /\ Y2) iff x in (f " Y1) /\ (f " Y2) )
proof
let x be set ; ::_thesis: ( x in f " (Y1 /\ Y2) iff x in (f " Y1) /\ (f " Y2) )
A1: ( x in f " Y2 iff ( f . x in Y2 & x in dom f ) ) by Def7;
A2: ( x in f " (Y1 /\ Y2) iff ( f . x in Y1 /\ Y2 & x in dom f ) ) by Def7;
 ( x in f " Y1 iff ( f . x in Y1 & x in dom f ) ) by Def7;
hence  ( x in f " (Y1 /\ Y2) iff x in (f " Y1) /\ (f " Y2) ) by A1, A2, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  f " (Y1 /\ Y2) = (f " Y1) /\ (f " Y2) by TARSKI:1; ::_thesis: verum
end;

theorem :: FUNCT_1:69
for Y1, Y2 being set
for f being Function holds f " (Y1 \ Y2) = (f " Y1) \ (f " Y2)
proof
let Y1, Y2 be set ; ::_thesis: for f being Function holds f " (Y1 \ Y2) = (f " Y1) \ (f " Y2)
let f be Function; ::_thesis: f " (Y1 \ Y2) = (f " Y1) \ (f " Y2)
 for x being set holds
( x in f " (Y1 \ Y2) iff x in (f " Y1) \ (f " Y2) )
proof
let x be set ; ::_thesis: ( x in f " (Y1 \ Y2) iff x in (f " Y1) \ (f " Y2) )
A1: ( x in f " Y2 iff ( f . x in Y2 & x in dom f ) ) by Def7;
A2: ( x in f " (Y1 \ Y2) iff ( f . x in Y1 \ Y2 & x in dom f ) ) by Def7;
 ( x in f " Y1 iff ( f . x in Y1 & x in dom f ) ) by Def7;
hence  ( x in f " (Y1 \ Y2) iff x in (f " Y1) \ (f " Y2) ) by A1, A2, XBOOLE_0:def_5; ::_thesis: verum
end;
hence  f " (Y1 \ Y2) = (f " Y1) \ (f " Y2) by TARSKI:1; ::_thesis: verum
end;

theorem :: FUNCT_1:70
for X, Y being set
for R being Relation holds (R | X) " Y = X /\ (R " Y)
proof
let X, Y be set ; ::_thesis: for R being Relation holds (R | X) " Y = X /\ (R " Y)
let R be Relation; ::_thesis: (R | X) " Y = X /\ (R " Y)
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: X /\ (R " Y) c= (R | X) " Y
let x be set ; ::_thesis: ( x in (R | X) " Y implies x in X /\ (R " Y) )
assume  x in (R | X) " Y ; ::_thesis: x in X /\ (R " Y)
then A1: ex y being set st
( [x,y] in R | X & y in Y ) by RELAT_1:def_14;
then A2: x in X by RELAT_1:def_11;
 R | X c= R by RELAT_1:59;
then  x in R " Y by A1, RELAT_1:def_14;
hence  x in X /\ (R " Y) by A2, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X /\ (R " Y) or x in (R | X) " Y )
assume A3: x in X /\ (R " Y) ; ::_thesis: x in (R | X) " Y
then  x in R " Y by XBOOLE_0:def_4;
then consider y being set  such that
A4: [x,y] in R and
A5: y in Y by RELAT_1:def_14;
 x in X by A3, XBOOLE_0:def_4;
then  [x,y] in R | X by A4, RELAT_1:def_11;
hence  x in (R | X) " Y by A5, RELAT_1:def_14; ::_thesis: verum
end;

theorem :: FUNCT_1:71
for f being Function
for A, B being set st A misses B holds
f " A misses f " B
proof
let f be Function; ::_thesis: for A, B being set st A misses B holds
f " A misses f " B
let A, B be set ; ::_thesis: ( A misses B implies f " A misses f " B )
assume  A misses B ; ::_thesis: f " A misses f " B
then  A /\ B = {} by XBOOLE_0:def_7;
then  {} = f " (A /\ B)
.= (f " A) /\ (f " B) by Th68 ;
hence  f " A misses f " B by XBOOLE_0:def_7; ::_thesis: verum
end;

theorem Th72: :: FUNCT_1:72
for y being set
for R being Relation holds
( y in rng R iff R " {y} <> {} )
proof
let y be set ; ::_thesis: for R being Relation holds
( y in rng R iff R " {y} <> {} )
let R be Relation; ::_thesis: ( y in rng R iff R " {y} <> {} )
thus  ( y in rng R implies R " {y} <> {} ) ::_thesis: ( R " {y} <> {} implies y in rng R )
proof
assume  y in rng R ; ::_thesis: R " {y} <> {}
then A1: ex x being set st [x,y] in R by XTUPLE_0:def_13;
 y in {y} by TARSKI:def_1;
hence  R " {y} <> {} by A1, RELAT_1:def_14; ::_thesis: verum
end;
assume  R " {y} <> {} ; ::_thesis: y in rng R
then consider x being set  such that
A2: x in R " {y} by XBOOLE_0:def_1;
consider z being set  such that
A3: [x,z] in R and
A4: z in {y} by A2, RELAT_1:def_14;
 z = y by A4, TARSKI:def_1;
hence  y in rng R by A3, XTUPLE_0:def_13; ::_thesis: verum
end;

theorem :: FUNCT_1:73
for Y being set
for R being Relation st ( for y being set st y in Y holds
R " {y} <> {} ) holds
Y c= rng R
proof
let Y be set ; ::_thesis: for R being Relation st ( for y being set st y in Y holds
R " {y} <> {} ) holds
Y c= rng R
let R be Relation; ::_thesis: ( ( for y being set st y in Y holds
R " {y} <> {} ) implies Y c= rng R )
assume A1: for y being set st y in Y holds
R " {y} <> {} ; ::_thesis: Y c= rng R
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Y or y in rng R )
assume  y in Y ; ::_thesis: y in rng R
then  R " {y} <> {} by A1;
hence  y in rng R by Th72; ::_thesis: verum
end;

theorem Th74: :: FUNCT_1:74
for f being Function holds
( ( for y being set st y in rng f holds
ex x being set st f " {y} = {x} ) iff f is one-to-one )
proof
let f be Function; ::_thesis: ( ( for y being set st y in rng f holds
ex x being set st f " {y} = {x} ) iff f is one-to-one )
thus  ( ( for y being set st y in rng f holds
ex x being set st f " {y} = {x} ) implies f is one-to-one ) ::_thesis: ( f is one-to-one implies for y being set st y in rng f holds
ex x being set st f " {y} = {x} )
proof
assume A1: for y being set st y in rng f holds
ex x being set st f " {y} = {x} ; ::_thesis: f is one-to-one
let x1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
let x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A2: x1 in dom f and
A3: x2 in dom f ; ::_thesis: ( not f . x1 = f . x2 or x1 = x2 )
 f . x1 in rng f by A2, Def3;
then consider y1 being set  such that
A4: f " {(f . x1)} = {y1} by A1;
 f . x2 in rng f by A3, Def3;
then consider y2 being set  such that
A5: f " {(f . x2)} = {y2} by A1;
 f . x1 in {(f . x1)} by TARSKI:def_1;
then  x1 in {y1} by A2, A4, Def7;
then A6: y1 = x1 by TARSKI:def_1;
 f . x2 in {(f . x2)} by TARSKI:def_1;
then  x2 in {y2} by A3, A5, Def7;
hence  ( not f . x1 = f . x2 or x1 = x2 ) by A4, A5, A6, TARSKI:def_1; ::_thesis: verum
end;
assume A7: f is one-to-one ; ::_thesis: for y being set st y in rng f holds
ex x being set st f " {y} = {x}
let y be set ; ::_thesis: ( y in rng f implies ex x being set st f " {y} = {x} )
assume  y in rng f ; ::_thesis: ex x being set st f " {y} = {x}
then consider x being set  such that
A8: ( x in dom f & y = f . x ) by Def3;
take  x ; ::_thesis: f " {y} = {x}
 for z being set holds
( z in f " {y} iff z = x )
proof
let z be set ; ::_thesis: ( z in f " {y} iff z = x )
thus  ( z in f " {y} implies z = x ) ::_thesis: ( z = x implies z in f " {y} )
proof
assume A9: z in f " {y} ; ::_thesis: z = x
then  f . z in {y} by Def7;
then A10: f . z = y by TARSKI:def_1;
 z in dom f by A9, Def7;
hence  z = x by A7, A8, A10, Def4; ::_thesis: verum
end;
 y in {y} by TARSKI:def_1;
hence  ( z = x implies z in f " {y} ) by A8, Def7; ::_thesis: verum
end;
hence  f " {y} = {x} by TARSKI:def_1; ::_thesis: verum
end;

theorem Th75: :: FUNCT_1:75
for Y being set
for f being Function holds f .: (f " Y) c= Y
proof
let Y be set ; ::_thesis: for f being Function holds f .: (f " Y) c= Y
let f be Function; ::_thesis: f .: (f " Y) c= Y
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: (f " Y) or y in Y )
assume  y in f .: (f " Y) ; ::_thesis: y in Y
then  ex x being set st
( x in dom f & x in f " Y & y = f . x ) by Def6;
hence  y in Y by Def7; ::_thesis: verum
end;

theorem Th76: :: FUNCT_1:76
for X being set
for R being Relation st X c= dom R holds
X c= R " (R .: X)
proof
let X be set ; ::_thesis: for R being Relation st X c= dom R holds
X c= R " (R .: X)
let R be Relation; ::_thesis: ( X c= dom R implies X c= R " (R .: X) )
assume A1: X c= dom R ; ::_thesis: X c= R " (R .: X)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in R " (R .: X) )
assume A2: x in X ; ::_thesis: x in R " (R .: X)
then consider Rx being set  such that
A3: [x,Rx] in R by A1, XTUPLE_0:def_12;
 Rx in R .: X by A2, A3, RELAT_1:def_13;
hence  x in R " (R .: X) by A3, RELAT_1:def_14; ::_thesis: verum
end;

theorem :: FUNCT_1:77
for Y being set
for f being Function st Y c= rng f holds
f .: (f " Y) = Y
proof
let Y be set ; ::_thesis: for f being Function st Y c= rng f holds
f .: (f " Y) = Y
let f be Function; ::_thesis: ( Y c= rng f implies f .: (f " Y) = Y )
assume A1: Y c= rng f ; ::_thesis: f .: (f " Y) = Y
thus  f .: (f " Y) c= Y by Th75; :: according to XBOOLE_0:def_10 ::_thesis: Y c= f .: (f " Y)
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Y or y in f .: (f " Y) )
assume A2: y in Y ; ::_thesis: y in f .: (f " Y)
then consider x being set  such that
A3: ( x in dom f & y = f . x ) by A1, Def3;
 x in f " Y by A2, A3, Def7;
hence  y in f .: (f " Y) by A3, Def6; ::_thesis: verum
end;

theorem :: FUNCT_1:78
for Y being set
for f being Function holds f .: (f " Y) = Y /\ (f .: (dom f))
proof
let Y be set ; ::_thesis: for f being Function holds f .: (f " Y) = Y /\ (f .: (dom f))
let f be Function; ::_thesis: f .: (f " Y) = Y /\ (f .: (dom f))
 ( f .: (f " Y) c= Y & f .: (f " Y) c= f .: (dom f) ) by Th75, RELAT_1:114;
hence  f .: (f " Y) c= Y /\ (f .: (dom f)) by XBOOLE_1:19; :: according to XBOOLE_0:def_10 ::_thesis: Y /\ (f .: (dom f)) c= f .: (f " Y)
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Y /\ (f .: (dom f)) or y in f .: (f " Y) )
assume A1: y in Y /\ (f .: (dom f)) ; ::_thesis: y in f .: (f " Y)
then  y in f .: (dom f) by XBOOLE_0:def_4;
then consider x being set  such that
A2: x in dom f and
 x in dom f and
A3: y = f . x by Def6;
 y in Y by A1, XBOOLE_0:def_4;
then  x in f " Y by A2, A3, Def7;
hence  y in f .: (f " Y) by A2, A3, Def6; ::_thesis: verum
end;

theorem Th79: :: FUNCT_1:79
for X, Y being set
for f being Function holds f .: (X /\ (f " Y)) c= (f .: X) /\ Y
proof
let X, Y be set ; ::_thesis: for f being Function holds f .: (X /\ (f " Y)) c= (f .: X) /\ Y
let f be Function; ::_thesis: f .: (X /\ (f " Y)) c= (f .: X) /\ Y
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: (X /\ (f " Y)) or y in (f .: X) /\ Y )
assume  y in f .: (X /\ (f " Y)) ; ::_thesis: y in (f .: X) /\ Y
then consider x being set  such that
A1: x in dom f and
A2: x in X /\ (f " Y) and
A3: y = f . x by Def6;
 x in f " Y by A2, XBOOLE_0:def_4;
then A4: y in Y by A3, Def7;
 x in X by A2, XBOOLE_0:def_4;
then  y in f .: X by A1, A3, Def6;
hence  y in (f .: X) /\ Y by A4, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem :: FUNCT_1:80
for X, Y being set
for f being Function holds f .: (X /\ (f " Y)) = (f .: X) /\ Y
proof
let X, Y be set ; ::_thesis: for f being Function holds f .: (X /\ (f " Y)) = (f .: X) /\ Y
let f be Function; ::_thesis: f .: (X /\ (f " Y)) = (f .: X) /\ Y
thus  f .: (X /\ (f " Y)) c= (f .: X) /\ Y by Th79; :: according to XBOOLE_0:def_10 ::_thesis: (f .: X) /\ Y c= f .: (X /\ (f " Y))
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (f .: X) /\ Y or y in f .: (X /\ (f " Y)) )
assume A1: y in (f .: X) /\ Y ; ::_thesis: y in f .: (X /\ (f " Y))
then  y in f .: X by XBOOLE_0:def_4;
then consider x being set  such that
A2: x in dom f and
A3: x in X and
A4: y = f . x by Def6;
 y in Y by A1, XBOOLE_0:def_4;
then  x in f " Y by A2, A4, Def7;
then  x in X /\ (f " Y) by A3, XBOOLE_0:def_4;
hence  y in f .: (X /\ (f " Y)) by A2, A4, Def6; ::_thesis: verum
end;

theorem :: FUNCT_1:81
for X, Y being set
for R being Relation holds X /\ (R " Y) c= R " ((R .: X) /\ Y)
proof
let X, Y be set ; ::_thesis: for R being Relation holds X /\ (R " Y) c= R " ((R .: X) /\ Y)
let R be Relation; ::_thesis: X /\ (R " Y) c= R " ((R .: X) /\ Y)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X /\ (R " Y) or x in R " ((R .: X) /\ Y) )
assume A1: x in X /\ (R " Y) ; ::_thesis: x in R " ((R .: X) /\ Y)
then  x in R " Y by XBOOLE_0:def_4;
then consider Rx being set  such that
A2: [x,Rx] in R and
A3: Rx in Y by RELAT_1:def_14;
 x in X by A1, XBOOLE_0:def_4;
then  Rx in R .: X by A2, RELAT_1:def_13;
then  Rx in (R .: X) /\ Y by A3, XBOOLE_0:def_4;
hence  x in R " ((R .: X) /\ Y) by A2, RELAT_1:def_14; ::_thesis: verum
end;

theorem Th82: :: FUNCT_1:82
for X being set
for f being Function st f is one-to-one holds
f " (f .: X) c= X
proof
let X be set ; ::_thesis: for f being Function st f is one-to-one holds
f " (f .: X) c= X
let f be Function; ::_thesis: ( f is one-to-one implies f " (f .: X) c= X )
assume A1: f is one-to-one ; ::_thesis: f " (f .: X) c= X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f " (f .: X) or x in X )
assume A2: x in f " (f .: X) ; ::_thesis: x in X
then  f . x in f .: X by Def7;
then A3: ex z being set st
( z in dom f & z in X & f . x = f . z ) by Def6;
 x in dom f by A2, Def7;
hence  x in X by A1, A3, Def4; ::_thesis: verum
end;

theorem :: FUNCT_1:83
for f being Function st ( for X being set holds f " (f .: X) c= X ) holds
f is one-to-one
proof
let f be Function; ::_thesis: ( ( for X being set holds f " (f .: X) c= X ) implies f is one-to-one )
assume A1: for X being set holds f " (f .: X) c= X ; ::_thesis: f is one-to-one
given x1, x2 being set  such that A2: x1 in dom f and
A3: x2 in dom f and
A4: ( f . x1 = f . x2 & x1 <> x2 ) ; :: according to FUNCT_1:def_4 ::_thesis: contradiction
A5: f " (f .: {x1}) c= {x1} by A1;
A6: Im (f,x2) = {(f . x2)} by A3, Th59;
A7: Im (f,x1) = {(f . x1)} by A2, Th59;
 f . x1 in rng f by A2, Def3;
then  f " (f .: {x1}) <> {} by A7, Th72;
then  f " (f .: {x1}) = {x1} by A5, ZFMISC_1:33;
hence  contradiction by A1, A4, A7, A6, ZFMISC_1:3; ::_thesis: verum
end;

theorem :: FUNCT_1:84
for X being set
for f being Function st f is one-to-one holds
f .: X = (f ") " X
proof
let X be set ; ::_thesis: for f being Function st f is one-to-one holds
f .: X = (f ") " X
let f be Function; ::_thesis: ( f is one-to-one implies f .: X = (f ") " X )
assume A1: f is one-to-one ; ::_thesis: f .: X = (f ") " X
 for y being set holds
( y in f .: X iff y in (f ") " X )
proof
let y be set ; ::_thesis: ( y in f .: X iff y in (f ") " X )
thus  ( y in f .: X implies y in (f ") " X ) ::_thesis: ( y in (f ") " X implies y in f .: X )
proof
assume  y in f .: X ; ::_thesis: y in (f ") " X
then consider x being set  such that
A2: x in dom f and
A3: x in X and
A4: y = f . x by Def6;
 y in rng f by A2, A4, Def3;
then A5: y in dom (f ") by A1, Th32;
 (f ") . (f . x) = x by A1, A2, Th32;
hence  y in (f ") " X by A3, A4, A5, Def7; ::_thesis: verum
end;
assume A6: y in (f ") " X ; ::_thesis: y in f .: X
then A7: (f ") . y in X by Def7;
 y in dom (f ") by A6, Def7;
then  y in rng f by A1, Th32;
then consider x being set  such that
A8: ( x in dom f & y = f . x ) by Def3;
 (f ") . y = x by A1, A8, Th34;
hence  y in f .: X by A7, A8, Def6; ::_thesis: verum
end;
hence  f .: X = (f ") " X by TARSKI:1; ::_thesis: verum
end;

theorem :: FUNCT_1:85
for Y being set
for f being Function st f is one-to-one holds
f " Y = (f ") .: Y
proof
let Y be set ; ::_thesis: for f being Function st f is one-to-one holds
f " Y = (f ") .: Y
let f be Function; ::_thesis: ( f is one-to-one implies f " Y = (f ") .: Y )
assume A1: f is one-to-one ; ::_thesis: f " Y = (f ") .: Y
 for x being set holds
( x in f " Y iff x in (f ") .: Y )
proof
let x be set ; ::_thesis: ( x in f " Y iff x in (f ") .: Y )
thus  ( x in f " Y implies x in (f ") .: Y ) ::_thesis: ( x in (f ") .: Y implies x in f " Y )
proof
assume A2: x in f " Y ; ::_thesis: x in (f ") .: Y
then A3: f . x in Y by Def7;
A4: x in dom f by A2, Def7;
then  f . x in rng f by Def3;
then A5: f . x in dom (f ") by A1, Th32;
 (f ") . (f . x) = x by A1, A4, Th32;
hence  x in (f ") .: Y by A3, A5, Def6; ::_thesis: verum
end;
assume  x in (f ") .: Y ; ::_thesis: x in f " Y
then consider y being set  such that
A6: y in dom (f ") and
A7: y in Y and
A8: x = (f ") . y by Def6;
 dom (f ") = rng f by A1, Th32;
then  ( y = f . x & x in dom f ) by A1, A6, A8, Th32;
hence  x in f " Y by A7, Def7; ::_thesis: verum
end;
hence  f " Y = (f ") .: Y by TARSKI:1; ::_thesis: verum
end;

theorem :: FUNCT_1:86
for Y being set
for f, g, h being Function st Y = rng f & dom g = Y & dom h = Y & g * f = h * f holds
g = h
proof
let Y be set ; ::_thesis: for f, g, h being Function st Y = rng f & dom g = Y & dom h = Y & g * f = h * f holds
g = h
let f, g, h be Function; ::_thesis: ( Y = rng f & dom g = Y & dom h = Y & g * f = h * f implies g = h )
assume that
A1: Y = rng f and
A2: ( dom g = Y & dom h = Y ) and
A3: g * f = h * f ; ::_thesis: g = h
 for y being set st y in Y holds
g . y = h . y
proof
let y be set ; ::_thesis: ( y in Y implies g . y = h . y )
assume  y in Y ; ::_thesis: g . y = h . y
then consider x being set  such that
A4: ( x in dom f & y = f . x ) by A1, Def3;
 (g * f) . x = g . y by A4, Th13;
hence  g . y = h . y by A3, A4, Th13; ::_thesis: verum
end;
hence  g = h by A2, Th2; ::_thesis: verum
end;

theorem :: FUNCT_1:87
for X1, X2 being set
for f being Function st f .: X1 c= f .: X2 & X1 c= dom f & f is one-to-one holds
X1 c= X2
proof
let X1, X2 be set ; ::_thesis: for f being Function st f .: X1 c= f .: X2 & X1 c= dom f & f is one-to-one holds
X1 c= X2
let f be Function; ::_thesis: ( f .: X1 c= f .: X2 & X1 c= dom f & f is one-to-one implies X1 c= X2 )
assume that
A1: f .: X1 c= f .: X2 and
A2: X1 c= dom f and
A3: f is one-to-one ; ::_thesis: X1 c= X2
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X1 or x in X2 )
assume A4: x in X1 ; ::_thesis: x in X2
then  f . x in f .: X1 by A2, Def6;
then  ex x2 being set st
( x2 in dom f & x2 in X2 & f . x = f . x2 ) by A1, Def6;
hence  x in X2 by A2, A3, A4, Def4; ::_thesis: verum
end;

theorem Th88: :: FUNCT_1:88
for Y1, Y2 being set
for f being Function st f " Y1 c= f " Y2 & Y1 c= rng f holds
Y1 c= Y2
proof
let Y1, Y2 be set ; ::_thesis: for f being Function st f " Y1 c= f " Y2 & Y1 c= rng f holds
Y1 c= Y2
let f be Function; ::_thesis: ( f " Y1 c= f " Y2 & Y1 c= rng f implies Y1 c= Y2 )
assume that
A1: f " Y1 c= f " Y2 and
A2: Y1 c= rng f ; ::_thesis: Y1 c= Y2
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Y1 or y in Y2 )
assume A3: y in Y1 ; ::_thesis: y in Y2
then consider x being set  such that
A4: x in dom f and
A5: y = f . x by A2, Def3;
 x in f " Y1 by A3, A4, A5, Def7;
hence  y in Y2 by A1, A5, Def7; ::_thesis: verum
end;

theorem :: FUNCT_1:89
for f being Function holds
( f is one-to-one iff for y being set ex x being set st f " {y} c= {x} )
proof
let f be Function; ::_thesis: ( f is one-to-one iff for y being set ex x being set st f " {y} c= {x} )
 ( ( for y being set ex x being set st f " {y} c= {x} ) iff for y being set st y in rng f holds
ex x being set st f " {y} = {x} )
proof
thus  ( ( for y being set ex x being set st f " {y} c= {x} ) implies for y being set st y in rng f holds
ex x being set st f " {y} = {x} ) ::_thesis: ( ( for y being set st y in rng f holds
ex x being set st f " {y} = {x} ) implies for y being set ex x being set st f " {y} c= {x} )
proof
assume A1: for y being set ex x being set st f " {y} c= {x} ; ::_thesis: for y being set st y in rng f holds
ex x being set st f " {y} = {x}
let y be set ; ::_thesis: ( y in rng f implies ex x being set st f " {y} = {x} )
consider x being set  such that
A2: f " {y} c= {x} by A1;
assume  y in rng f ; ::_thesis: ex x being set st f " {y} = {x}
then consider x1 being set  such that
A3: x1 in dom f and
A4: y = f . x1 by Def3;
take  x ; ::_thesis: f " {y} = {x}
 f . x1 in {y} by A4, TARSKI:def_1;
then  f " {y} <> {} by A3, Def7;
hence  f " {y} = {x} by A2, ZFMISC_1:33; ::_thesis: verum
end;
assume A5: for y being set st y in rng f holds
ex x being set st f " {y} = {x} ; ::_thesis: for y being set ex x being set st f " {y} c= {x}
let y be set ; ::_thesis: ex x being set st f " {y} c= {x}
A6: now__::_thesis:_(_not_y_in_rng_f_implies_ex_x_being_set_st_f_"_{y}_c=_{x}_)
set x = the set ;
assume A7: not y in rng f ; ::_thesis: ex x being set st f " {y} c= {x}
take x = the set ; ::_thesis: f " {y} c= {x}
 rng f misses {y} by A7, ZFMISC_1:50;
then  f " {y} = {} by RELAT_1:138;
hence  f " {y} c= {x} by XBOOLE_1:2; ::_thesis: verum
end;
now__::_thesis:_(_y_in_rng_f_implies_ex_x_being_set_st_f_"_{y}_c=_{x}_)
assume  y in rng f ; ::_thesis: ex x being set st f " {y} c= {x}
then consider x being set  such that
A8: f " {y} = {x} by A5;
take x = x; ::_thesis: f " {y} c= {x}
thus  f " {y} c= {x} by A8; ::_thesis: verum
end;
hence  ex x being set st f " {y} c= {x} by A6; ::_thesis: verum
end;
hence  ( f is one-to-one iff for y being set ex x being set st f " {y} c= {x} ) by Th74; ::_thesis: verum
end;

theorem :: FUNCT_1:90
for X being set
for R, S being Relation st rng R c= dom S holds
R " X c= (R * S) " (S .: X)
proof
let X be set ; ::_thesis: for R, S being Relation st rng R c= dom S holds
R " X c= (R * S) " (S .: X)
let R, S be Relation; ::_thesis: ( rng R c= dom S implies R " X c= (R * S) " (S .: X) )
assume A1: rng R c= dom S ; ::_thesis: R " X c= (R * S) " (S .: X)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R " X or x in (R * S) " (S .: X) )
assume  x in R " X ; ::_thesis: x in (R * S) " (S .: X)
then consider Rx being set  such that
A2: [x,Rx] in R and
A3: Rx in X by RELAT_1:def_14;
 Rx in rng R by A2, XTUPLE_0:def_13;
then consider SRx being set  such that
A4: [Rx,SRx] in S by A1, XTUPLE_0:def_12;
 ( SRx in S .: X & [x,SRx] in R * S ) by A2, A3, A4, RELAT_1:def_8, RELAT_1:def_13;
hence  x in (R * S) " (S .: X) by RELAT_1:def_14; ::_thesis: verum
end;

theorem :: FUNCT_1:91
for X, Y being set
for f being Function st f " X = f " Y & X c= rng f & Y c= rng f holds
X = Y
proof
let X, Y be set ; ::_thesis: for f being Function st f " X = f " Y & X c= rng f & Y c= rng f holds
X = Y
let f be Function; ::_thesis: ( f " X = f " Y & X c= rng f & Y c= rng f implies X = Y )
assume  ( f " X = f " Y & X c= rng f & Y c= rng f ) ; ::_thesis: X = Y
then  ( X c= Y & Y c= X ) by Th88;
hence  X = Y by XBOOLE_0:def_10; ::_thesis: verum
end;

begin


theorem :: FUNCT_1:92
for X being set
for A being Subset of X holds (id X) .: A = A
proof
let X be set ; ::_thesis: for A being Subset of X holds (id X) .: A = A
let A be Subset of X; ::_thesis: (id X) .: A = A
now__::_thesis:_for_e_being_set_holds_
(_(_e_in_A_implies_ex_u_being_set_st_
(_u_in_dom_(id_X)_&_u_in_A_&_e_=_(id_X)_._u_)_)_&_(_ex_u_being_set_st_
(_u_in_dom_(id_X)_&_u_in_A_&_e_=_(id_X)_._u_)_implies_e_in_A_)_)
let e be set ; ::_thesis: ( ( e in A implies ex u being set st
( u in dom (id X) & u in A & e = (id X) . u ) ) & ( ex u being set st
( u in dom (id X) & u in A & e = (id X) . u ) implies e in A ) )
thus  ( e in A implies ex u being set st
( u in dom (id X) & u in A & e = (id X) . u ) ) ::_thesis: ( ex u being set st
( u in dom (id X) & u in A & e = (id X) . u ) implies e in A )
proof
assume A1: e in A ; ::_thesis: ex u being set st
( u in dom (id X) & u in A & e = (id X) . u )
take  e ; ::_thesis: ( e in dom (id X) & e in A & e = (id X) . e )
thus  e in dom (id X) by A1; ::_thesis: ( e in A & e = (id X) . e )
thus  e in A by A1; ::_thesis: e = (id X) . e
thus  e = (id X) . e by A1, Th17; ::_thesis: verum
end;
assume  ex u being set st
( u in dom (id X) & u in A & e = (id X) . u ) ; ::_thesis: e in A
hence  e in A by Th17; ::_thesis: verum
end;
hence  (id X) .: A = A by Def6; ::_thesis: verum
end;

definition
let f be Function;
redefine attr f is empty-yielding  means :Def8: :: FUNCT_1:def 8
 for x being set st x in dom f holds
f . x is empty ;
compatibility
 ( f is empty-yielding iff for x being set st x in dom f holds
f . x is empty )
proof
hereby  ::_thesis: ( ( for x being set st x in dom f holds
f . x is empty ) implies f is empty-yielding )
assume A1: f is empty-yielding ; ::_thesis: for x being set st x in dom f holds
f . x is empty
let x be set ; ::_thesis: ( x in dom f implies f . x is empty )
assume  x in dom f ; ::_thesis: f . x is empty
then  f . x in rng f by Def3;
hence  f . x is empty by A1, RELAT_1:149; ::_thesis: verum
end;
assume A2: for x being set st x in dom f holds
f . x is empty ; ::_thesis: f is empty-yielding
let s be set ; :: according to TARSKI:def_3,RELAT_1:def_15 ::_thesis: ( not s in rng f or s in {{}} )
assume  s in rng f ; ::_thesis: s in {{}}
then  ex e being set st
( e in dom f & s = f . e ) by Def3;
then  s = {} by A2;
hence  s in {{}} by TARSKI:def_1; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines empty-yielding FUNCT_1:def_8_:_
 for f being Function holds
( f is empty-yielding iff for x being set st x in dom f holds
f . x is empty );

definition
let F be Function;
redefine attr F is non-empty  means :Def9: :: FUNCT_1:def 9
 for n being set st n in dom F holds
not F . n is empty ;
compatibility
 ( F is non-empty iff for n being set st n in dom F holds
not F . n is empty )
proof
hereby  ::_thesis: ( ( for n being set st n in dom F holds
not F . n is empty ) implies F is non-empty )
assume  F is non-empty ; ::_thesis: for i being set st i in dom F holds
not F . i is empty
then A1: not {} in rng F by RELAT_1:def_9;
let i be set ; ::_thesis: ( i in dom F implies not F . i is empty )
assume  i in dom F ; ::_thesis: not F . i is empty
hence  not F . i is empty by A1, Def3; ::_thesis: verum
end;
assume A2: for n being set st n in dom F holds
not F . n is empty ; ::_thesis: F is non-empty
assume  {} in rng F ; :: according to RELAT_1:def_9 ::_thesis: contradiction
then  ex i being set st
( i in dom F & F . i = {} ) by Def3;
hence  contradiction by A2; ::_thesis: verum
end;
end;

:: deftheorem Def9 defines non-empty FUNCT_1:def_9_:_
 for F being Function holds
( F is non-empty iff for n being set st n in dom F holds
not F . n is empty );

registration
cluster Relation-like non-empty Function-like for set ;
existence
 ex b1 being Function st b1 is non-empty
proof
take  {} ; ::_thesis: {} is non-empty
let x be set ; :: according to FUNCT_1:def_9 ::_thesis: ( x in dom {} implies not {} . x is empty )
thus  ( x in dom {} implies not {} . x is empty ) ; ::_thesis: verum
end;
end;

scheme :: FUNCT_1:sch 4
LambdaB{ F1() ->  non empty set , F2( set ) ->  set } :
 ex f being Function st
( dom f = F1() & ( for d being Element of F1() holds f . d = F2(d) ) )
proof
consider f being Function such that
A1: ( dom f = F1() & ( for d being set st d in F1() holds
f . d = F2(d) ) ) from FUNCT_1:sch_3();
take  f ; ::_thesis: ( dom f = F1() & ( for d being Element of F1() holds f . d = F2(d) ) )
thus  ( dom f = F1() & ( for d being Element of F1() holds f . d = F2(d) ) ) by A1; ::_thesis: verum
end;

registration
let f be non-empty Function;
cluster rng f ->  with_non-empty_elements ;
coherence
 rng f is with_non-empty_elements
proof
assume  {} in rng f ; :: according to SETFAM_1:def_8 ::_thesis: contradiction
then  ex x being set st
( x in dom f & {} = f . x ) by Def3;
hence  contradiction by Def9; ::_thesis: verum
end;
end;

definition
let f be Function;
attrf is constant  means :Def10: :: FUNCT_1:def 10
 for x, y being set st x in dom f & y in dom f holds
f . x = f . y;
end;

:: deftheorem Def10 defines constant FUNCT_1:def_10_:_
 for f being Function holds
( f is constant iff for x, y being set st x in dom f & y in dom f holds
f . x = f . y );

theorem :: FUNCT_1:93
for A, B being set
for f being Function st A c= dom f & f .: A c= B holds
A c= f " B
proof
let A, B be set ; ::_thesis: for f being Function st A c= dom f & f .: A c= B holds
A c= f " B
let f be Function; ::_thesis: ( A c= dom f & f .: A c= B implies A c= f " B )
assume  A c= dom f ; ::_thesis: ( not f .: A c= B or A c= f " B )
then A1: A c= f " (f .: A) by Th76;
assume  f .: A c= B ; ::_thesis: A c= f " B
then  f " (f .: A) c= f " B by RELAT_1:143;
hence  A c= f " B by A1, XBOOLE_1:1; ::_thesis: verum
end;

theorem :: FUNCT_1:94
for X being set
for f being Function st X c= dom f & f is one-to-one holds
f " (f .: X) = X
proof
let X be set ; ::_thesis: for f being Function st X c= dom f & f is one-to-one holds
f " (f .: X) = X
let f be Function; ::_thesis: ( X c= dom f & f is one-to-one implies f " (f .: X) = X )
assume that
A1: X c= dom f and
A2: f is one-to-one ; ::_thesis: f " (f .: X) = X
thus  f " (f .: X) c= X by A2, Th82; :: according to XBOOLE_0:def_10 ::_thesis: X c= f " (f .: X)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in f " (f .: X) )
assume A3: x in X ; ::_thesis: x in f " (f .: X)
then  f . x in f .: X by A1, Def6;
hence  x in f " (f .: X) by A1, A3, Def7; ::_thesis: verum
end;

definition
let f, g be Function;
redefine pred f = g means :: FUNCT_1:def 11
( dom f = dom g & ( for x being set st x in dom f holds
f . x = g . x ) );
compatibility
 ( f = g iff ( dom f = dom g & ( for x being set st x in dom f holds
f . x = g . x ) ) ) by Th2;
end;

:: deftheorem  defines = FUNCT_1:def_11_:_
 for f, g being Function holds
( f = g iff ( dom f = dom g & ( for x being set st x in dom f holds
f . x = g . x ) ) );

registration
cluster non empty Relation-like non-empty Function-like for set ;
existence
 ex b1 being Function st
( b1 is non-empty & not b1 is empty )
proof
consider f being Function such that
A1: dom f = {{}} and
A2: rng f = {{{}}} by Th5;
take  f ; ::_thesis: ( f is non-empty & not f is empty )
 not {} in rng f by A2, TARSKI:def_1;
hence  f is non-empty by RELAT_1:def_9; ::_thesis: not f is empty
thus  not f is empty by A1; ::_thesis: verum
end;
end;

registration
let a be non empty non-empty Function;
let i be Element of dom a;
clustera . i ->  non empty ;
coherence
 not a . i is empty
proof
 a . i in rng a by Def3;
hence  not a . i is empty by RELAT_1:def_9; ::_thesis: verum
end;
end;

registration
let f be Function;
cluster  ->  Function-like for Element of bool f;
coherence
 for b1 being Subset of f holds b1 is Function-like
proof
let g be Subset of f; ::_thesis: g is Function-like
let x be set ; :: according to FUNCT_1:def_1 ::_thesis: for y1, y2 being set st [x,y1] in g & [x,y2] in g holds
y1 = y2
let y1, y2 be set ; ::_thesis: ( [x,y1] in g & [x,y2] in g implies y1 = y2 )
assume  ( [x,y1] in g & [x,y2] in g ) ; ::_thesis: y1 = y2
hence  y1 = y2 by Def1; ::_thesis: verum
end;
end;

theorem :: FUNCT_1:95
for f, g being Function
for D being set st D c= dom f & D c= dom g holds
( f | D = g | D iff for x being set st x in D holds
f . x = g . x )
proof
let f, g be Function; ::_thesis: for D being set st D c= dom f & D c= dom g holds
( f | D = g | D iff for x being set st x in D holds
f . x = g . x )
let D be set ; ::_thesis: ( D c= dom f & D c= dom g implies ( f | D = g | D iff for x being set st x in D holds
f . x = g . x ) )
assume that
A1: D c= dom f and
A2: D c= dom g ; ::_thesis: ( f | D = g | D iff for x being set st x in D holds
f . x = g . x )
A3: dom (g | D) = (dom g) /\ D by RELAT_1:61
.= D by A2, XBOOLE_1:28 ;
hereby  ::_thesis: ( ( for x being set st x in D holds
f . x = g . x ) implies f | D = g | D )
assume A4: f | D = g | D ; ::_thesis: for x being set st x in D holds
f . x = g . x
hereby  ::_thesis: verum
let x be set ; ::_thesis: ( x in D implies f . x = g . x )
assume A5: x in D ; ::_thesis: f . x = g . x
hence f . x = (g | D) . x by A4, Th49
.= g . x by A5, Th49 ;
::_thesis: verum
end;
end;
assume A6: for x being set st x in D holds
f . x = g . x ; ::_thesis: f | D = g | D
A7: now__::_thesis:_for_x_being_set_st_x_in_D_holds_
(f_|_D)_._x_=_(g_|_D)_._x
let x be set ; ::_thesis: ( x in D implies (f | D) . x = (g | D) . x )
assume A8: x in D ; ::_thesis: (f | D) . x = (g | D) . x
hence (f | D) . x = f . x by Th49
.= g . x by A6, A8
.= (g | D) . x by A8, Th49 ;
::_thesis: verum
end;
dom (f | D) = (dom f) /\ D by RELAT_1:61
.= D by A1, XBOOLE_1:28 ;
hence  f | D = g | D by A3, A7, Th2; ::_thesis: verum
end;

theorem :: FUNCT_1:96
for f, g being Function
for X being set st dom f = dom g & ( for x being set st x in X holds
f . x = g . x ) holds
f | X = g | X
proof
let f, g be Function; ::_thesis: for X being set st dom f = dom g & ( for x being set st x in X holds
f . x = g . x ) holds
f | X = g | X
let X be set ; ::_thesis: ( dom f = dom g & ( for x being set st x in X holds
f . x = g . x ) implies f | X = g | X )
assume that
A1: dom f = dom g and
A2: for x being set st x in X holds
f . x = g . x ; ::_thesis: f | X = g | X
A3: dom (f | X) = (dom f) /\ X by RELAT_1:61;
then A4: dom (f | X) = dom (g | X) by A1, RELAT_1:61;
now__::_thesis:_for_x_being_set_st_x_in_dom_(f_|_X)_holds_
(f_|_X)_._x_=_(g_|_X)_._x
let x be set ; ::_thesis: ( x in dom (f | X) implies (f | X) . x = (g | X) . x )
assume A5: x in dom (f | X) ; ::_thesis: (f | X) . x = (g | X) . x
then A6: x in X by A3, XBOOLE_0:def_4;
 ( (f | X) . x = f . x & (g | X) . x = g . x ) by A4, A5, Th47;
hence  (f | X) . x = (g | X) . x by A2, A6; ::_thesis: verum
end;
hence  f | X = g | X by A4, Th2; ::_thesis: verum
end;

theorem Th97: :: FUNCT_1:97
for X being set
for f being Function holds rng (f | {X}) c= {(f . X)}
proof
let X be set ; ::_thesis: for f being Function holds rng (f | {X}) c= {(f . X)}
let f be Function; ::_thesis: rng (f | {X}) c= {(f . X)}
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (f | {X}) or x in {(f . X)} )
assume  x in rng (f | {X}) ; ::_thesis: x in {(f . X)}
then consider y being set  such that
A1: y in dom (f | {X}) and
A2: x = (f | {X}) . y by Def3;
 dom (f | {X}) c= {X} by RELAT_1:58;
then  y = X by A1, TARSKI:def_1;
then  x = f . X by A1, A2, Th47;
hence  x in {(f . X)} by TARSKI:def_1; ::_thesis: verum
end;

theorem :: FUNCT_1:98
for X being set
for f being Function st X in dom f holds
rng (f | {X}) = {(f . X)}
proof
let X be set ; ::_thesis: for f being Function st X in dom f holds
rng (f | {X}) = {(f . X)}
let f be Function; ::_thesis: ( X in dom f implies rng (f | {X}) = {(f . X)} )
A1: X in {X} by TARSKI:def_1;
assume  X in dom f ; ::_thesis: rng (f | {X}) = {(f . X)}
then A2: X in dom (f | {X}) by A1, RELAT_1:57;
thus  rng (f | {X}) c= {(f . X)} by Th97; :: according to XBOOLE_0:def_10 ::_thesis: {(f . X)} c= rng (f | {X})
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(f . X)} or x in rng (f | {X}) )
assume  x in {(f . X)} ; ::_thesis: x in rng (f | {X})
then  x = f . X by TARSKI:def_1;
then  x = (f | {X}) . X by A2, Th47;
hence  x in rng (f | {X}) by A2, Def3; ::_thesis: verum
end;

registration
cluster empty Relation-like Function-like  ->  constant for set ;
coherence
 for b1 being Function st b1 is empty holds
b1 is constant
proof
let f be Function; ::_thesis: ( f is empty implies f is constant )
assume A1: f is empty ; ::_thesis: f is constant
let x be set ; :: according to FUNCT_1:def_10 ::_thesis: for y being set st x in dom f & y in dom f holds
f . x = f . y
thus  for y being set st x in dom f & y in dom f holds
f . x = f . y by A1; ::_thesis: verum
end;
end;

registration
let f be constant Function;
cluster rng f ->  trivial ;
coherence
 rng f is trivial
proof
percases ( f is empty or f <> {} ) ;
suppose f is empty ; ::_thesis: rng f is trivial
then reconsider g = f as empty Function ;
 rng g is empty ;
hence  rng f is trivial ; ::_thesis: verum
end;
suppose f <> {} ; ::_thesis: rng f is trivial
then consider x being set  such that
A1: x in dom f by XBOOLE_0:def_1;
 for y being set holds
( y in {(f . x)} iff ex z being set st
( z in dom f & y = f . z ) )
proof
let y be set ; ::_thesis: ( y in {(f . x)} iff ex z being set st
( z in dom f & y = f . z ) )
hereby  ::_thesis: ( ex z being set st
( z in dom f & y = f . z ) implies y in {(f . x)} )
assume A2: y in {(f . x)} ; ::_thesis: ex x being set st
( x in dom f & y = f . x )
take x = x; ::_thesis: ( x in dom f & y = f . x )
thus  ( x in dom f & y = f . x ) by A1, A2, TARSKI:def_1; ::_thesis: verum
end;
given z being set  such that A3: ( z in dom f & y = f . z ) ; ::_thesis: y in {(f . x)}
 y = f . x by A1, A3, Def10;
hence  y in {(f . x)} by TARSKI:def_1; ::_thesis: verum
end;
hence  rng f is trivial by Def3; ::_thesis: verum
end;
end;
end;
end;

registration
cluster Relation-like Function-like non constant for set ;
existence
 not for b1 being Function holds b1 is constant
proof
set f = {[1,1],[2,2]};
 {[1,1],[2,2]} is Function-like
proof
let x, y, z be set ; :: according to FUNCT_1:def_1 ::_thesis: ( [x,y] in {[1,1],[2,2]} & [x,z] in {[1,1],[2,2]} implies y = z )
assume that
A1: [x,y] in {[1,1],[2,2]} and
A2: [x,z] in {[1,1],[2,2]} ; ::_thesis: y = z
 ( [x,y] = [1,1] or [x,y] = [2,2] ) by A1, TARSKI:def_2;
then A3: ( ( x = 1 & y = 1 ) or ( x = 2 & y = 2 ) ) by XTUPLE_0:1;
 ( [x,z] = [1,1] or [x,z] = [2,2] ) by A2, TARSKI:def_2;
hence  y = z by A3, XTUPLE_0:1; ::_thesis: verum
end;
then reconsider f = {[1,1],[2,2]} as Function ;
take  f ; ::_thesis: not f is constant
take  1 ; :: according to FUNCT_1:def_10 ::_thesis: ex y being set st
( 1 in dom f & y in dom f & not f . 1 = f . y )
take  2 ; ::_thesis: ( 1 in dom f & 2 in dom f & not f . 1 = f . 2 )
A4: [2,2] in f by TARSKI:def_2;
A5: [1,1] in f by TARSKI:def_2;
hence A6: ( 1 in dom f & 2 in dom f ) by A4, XTUPLE_0:def_12; ::_thesis: not f . 1 = f . 2
then  f . 1 = 1 by A5, Def2;
hence  not f . 1 = f . 2 by A4, A6, Def2; ::_thesis: verum
end;
end;

registration
let f be non constant Function;
cluster rng f ->  non trivial ;
coherence
 not rng f is trivial
proof
assume A1: rng f is trivial ; ::_thesis: contradiction
percases ( rng f is empty or not rng f is empty ) ;
suppose rng f is empty ; ::_thesis: contradiction
then reconsider f = f as empty Function ;
 f is trivial ;
hence  contradiction ; ::_thesis: verum
end;
suppose not rng f is empty ; ::_thesis: contradiction
then consider x being set  such that
A2: x in rng f by XBOOLE_0:def_1;
 f is constant
proof
let y, z be set ; :: according to FUNCT_1:def_10 ::_thesis: ( y in dom f & z in dom f implies f . y = f . z )
assume that
A3: y in dom f and
A4: z in dom f ; ::_thesis: f . y = f . z
A5: f . z in rng f by A4, Def3;
 f . y in rng f by A3, Def3;
hence f . y = x by A1, A2, ZFMISC_1:def_10
.= f . z by A1, A2, A5, ZFMISC_1:def_10 ;
::_thesis: verum
end;
hence  contradiction ; ::_thesis: verum
end;
end;
end;
end;

registration
cluster Relation-like Function-like non constant  ->  non trivial for set ;
coherence
 for b1 being Function st not b1 is constant holds
not b1 is trivial
proof
let f be Function; ::_thesis: ( not f is constant implies not f is trivial )
assume  not f is constant ; ::_thesis: not f is trivial
then consider n1, n2 being set  such that
A1: n1 in dom f and
A2: n2 in dom f and
A3: f . n1 <> f . n2 by Def10;
reconsider f = f as non empty Function by A1;
 not f is trivial
proof
reconsider x = [n1,(f . n1)], y = [n2,(f . n2)] as Element of f by A1, A2, Th1;
take  x ; :: according to ZFMISC_1:def_10 ::_thesis: ex b1 being set st
( x in f & b1 in f & not x = b1 )
take  y ; ::_thesis: ( x in f & y in f & not x = y )
thus  ( x in f & y in f ) ; ::_thesis: not x = y
thus  not x = y by A3, XTUPLE_0:1; ::_thesis: verum
end;
hence  not f is trivial ; ::_thesis: verum
end;
end;

registration
cluster trivial Relation-like Function-like  ->  constant for set ;
coherence
 for b1 being Function st b1 is trivial holds
b1 is constant ;
end;

theorem :: FUNCT_1:99
for F, G being Function
for X being set holds (G | (F .: X)) * (F | X) = (G * F) | X
proof
let F, G be Function; ::_thesis: for X being set holds (G | (F .: X)) * (F | X) = (G * F) | X
let X be set ; ::_thesis: (G | (F .: X)) * (F | X) = (G * F) | X
set Y = dom ((G * F) | X);
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_dom_((G_|_(F_.:_X))_*_(F_|_X))_implies_x_in_dom_((G_*_F)_|_X)_)_&_(_x_in_dom_((G_*_F)_|_X)_implies_x_in_dom_((G_|_(F_.:_X))_*_(F_|_X))_)_)
let x be set ; ::_thesis: ( ( x in dom ((G | (F .: X)) * (F | X)) implies x in dom ((G * F) | X) ) & ( x in dom ((G * F) | X) implies x in dom ((G | (F .: X)) * (F | X)) ) )
thus  ( x in dom ((G | (F .: X)) * (F | X)) implies x in dom ((G * F) | X) ) ::_thesis: ( x in dom ((G * F) | X) implies x in dom ((G | (F .: X)) * (F | X)) )
proof
assume A1: x in dom ((G | (F .: X)) * (F | X)) ; ::_thesis: x in dom ((G * F) | X)
then A2: x in dom (F | X) by Th11;
then A3: x in (dom F) /\ X by RELAT_1:61;
then A4: x in X by XBOOLE_0:def_4;
 (F | X) . x in dom (G | (F .: X)) by A1, Th11;
then  F . x in dom (G | (F .: X)) by A2, Th47;
then  F . x in (dom G) /\ (F .: X) by RELAT_1:61;
then A5: F . x in dom G by XBOOLE_0:def_4;
 x in dom F by A3, XBOOLE_0:def_4;
then  x in dom (G * F) by A5, Th11;
then  x in (dom (G * F)) /\ X by A4, XBOOLE_0:def_4;
hence  x in dom ((G * F) | X) by RELAT_1:61; ::_thesis: verum
end;
assume  x in dom ((G * F) | X) ; ::_thesis: x in dom ((G | (F .: X)) * (F | X))
then A6: x in (dom (G * F)) /\ X by RELAT_1:61;
then A7: x in dom (G * F) by XBOOLE_0:def_4;
then A8: F . x in dom G by Th11;
A9: x in X by A6, XBOOLE_0:def_4;
 x in dom F by A7, Th11;
then  x in (dom F) /\ X by A9, XBOOLE_0:def_4;
then A10: x in dom (F | X) by RELAT_1:61;
 x in dom F by A7, Th11;
then  F . x in F .: X by A9, Def6;
then  F . x in (dom G) /\ (F .: X) by A8, XBOOLE_0:def_4;
then  F . x in dom (G | (F .: X)) by RELAT_1:61;
then  (F | X) . x in dom (G | (F .: X)) by A10, Th47;
hence  x in dom ((G | (F .: X)) * (F | X)) by A10, Th11; ::_thesis: verum
end;
then A11: dom ((G * F) | X) = dom ((G | (F .: X)) * (F | X)) by TARSKI:1;
now__::_thesis:_for_x_being_set_st_x_in_dom_((G_*_F)_|_X)_holds_
((G_|_(F_.:_X))_*_(F_|_X))_._x_=_((G_*_F)_|_X)_._x
let x be set ; ::_thesis: ( x in dom ((G * F) | X) implies ((G | (F .: X)) * (F | X)) . x = ((G * F) | X) . x )
assume A12: x in dom ((G * F) | X) ; ::_thesis: ((G | (F .: X)) * (F | X)) . x = ((G * F) | X) . x
then A13: x in (dom (G * F)) /\ X by RELAT_1:61;
then  x in dom (G * F) by XBOOLE_0:def_4;
then A14: x in dom F by Th11;
A15: x in X by A13, XBOOLE_0:def_4;
then A16: F . x in F .: X by A14, Def6;
thus ((G | (F .: X)) * (F | X)) . x = (G | (F .: X)) . ((F | X) . x) by A11, A12, Th12
.= (G | (F .: X)) . (F . x) by A15, Th49
.= G . (F . x) by A16, Th49
.= (G * F) . x by A14, Th13
.= ((G * F) | X) . x by A13, Th48 ; ::_thesis: verum
end;
hence  (G | (F .: X)) * (F | X) = (G * F) | X by A11, Th2; ::_thesis: verum
end;

theorem :: FUNCT_1:100
for F, G being Function
for X, X1 being set holds (G | X1) * (F | X) = (G * F) | (X /\ (F " X1))
proof
let F, G be Function; ::_thesis: for X, X1 being set holds (G | X1) * (F | X) = (G * F) | (X /\ (F " X1))
let X, X1 be set ; ::_thesis: (G | X1) * (F | X) = (G * F) | (X /\ (F " X1))
set Y = dom ((G | X1) * (F | X));
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_dom_((G_*_F)_|_(X_/\_(F_"_X1)))_implies_x_in_dom_((G_|_X1)_*_(F_|_X))_)_&_(_x_in_dom_((G_|_X1)_*_(F_|_X))_implies_x_in_dom_((G_*_F)_|_(X_/\_(F_"_X1)))_)_)
let x be set ; ::_thesis: ( ( x in dom ((G * F) | (X /\ (F " X1))) implies x in dom ((G | X1) * (F | X)) ) & ( x in dom ((G | X1) * (F | X)) implies x in dom ((G * F) | (X /\ (F " X1))) ) )
thus  ( x in dom ((G * F) | (X /\ (F " X1))) implies x in dom ((G | X1) * (F | X)) ) ::_thesis: ( x in dom ((G | X1) * (F | X)) implies x in dom ((G * F) | (X /\ (F " X1))) )
proof
assume  x in dom ((G * F) | (X /\ (F " X1))) ; ::_thesis: x in dom ((G | X1) * (F | X))
then A1: x in (dom (G * F)) /\ (X /\ (F " X1)) by RELAT_1:61;
then A2: x in dom (G * F) by XBOOLE_0:def_4;
A3: x in X /\ (F " X1) by A1, XBOOLE_0:def_4;
then A4: x in X by XBOOLE_0:def_4;
 x in dom F by A2, Th11;
then  x in (dom F) /\ X by A4, XBOOLE_0:def_4;
then A5: x in dom (F | X) by RELAT_1:61;
 x in F " X1 by A3, XBOOLE_0:def_4;
then A6: F . x in X1 by Def7;
 F . x in dom G by A2, Th11;
then  F . x in (dom G) /\ X1 by A6, XBOOLE_0:def_4;
then  F . x in dom (G | X1) by RELAT_1:61;
then  (F | X) . x in dom (G | X1) by A5, Th47;
hence  x in dom ((G | X1) * (F | X)) by A5, Th11; ::_thesis: verum
end;
assume A7: x in dom ((G | X1) * (F | X)) ; ::_thesis: x in dom ((G * F) | (X /\ (F " X1)))
then A8: x in dom (F | X) by Th11;
then A9: x in (dom F) /\ X by RELAT_1:61;
then A10: x in dom F by XBOOLE_0:def_4;
A11: x in X by A9, XBOOLE_0:def_4;
 (F | X) . x in dom (G | X1) by A7, Th11;
then  F . x in dom (G | X1) by A8, Th47;
then A12: F . x in (dom G) /\ X1 by RELAT_1:61;
then  F . x in X1 by XBOOLE_0:def_4;
then  x in F " X1 by A10, Def7;
then A13: x in X /\ (F " X1) by A11, XBOOLE_0:def_4;
 F . x in dom G by A12, XBOOLE_0:def_4;
then  x in dom (G * F) by A10, Th11;
then  x in (dom (G * F)) /\ (X /\ (F " X1)) by A13, XBOOLE_0:def_4;
hence  x in dom ((G * F) | (X /\ (F " X1))) by RELAT_1:61; ::_thesis: verum
end;
then A14: dom ((G | X1) * (F | X)) = dom ((G * F) | (X /\ (F " X1))) by TARSKI:1;
now__::_thesis:_for_x_being_set_st_x_in_dom_((G_|_X1)_*_(F_|_X))_holds_
((G_|_X1)_*_(F_|_X))_._x_=_((G_*_F)_|_(X_/\_(F_"_X1)))_._x
let x be set ; ::_thesis: ( x in dom ((G | X1) * (F | X)) implies ((G | X1) * (F | X)) . x = ((G * F) | (X /\ (F " X1))) . x )
assume A15: x in dom ((G | X1) * (F | X)) ; ::_thesis: ((G | X1) * (F | X)) . x = ((G * F) | (X /\ (F " X1))) . x
then A16: x in dom (F | X) by Th11;
then A17: x in (dom F) /\ X by RELAT_1:61;
then A18: x in dom F by XBOOLE_0:def_4;
A19: (F | X) . x in dom (G | X1) by A15, Th11;
then A20: F . x in dom (G | X1) by A16, Th47;
A21: x in X by A17, XBOOLE_0:def_4;
 F . x in dom (G | X1) by A16, A19, Th47;
then  F . x in (dom G) /\ X1 by RELAT_1:61;
then  F . x in X1 by XBOOLE_0:def_4;
then  x in F " X1 by A18, Def7;
then A22: x in X /\ (F " X1) by A21, XBOOLE_0:def_4;
thus ((G | X1) * (F | X)) . x = (G | X1) . ((F | X) . x) by A15, Th12
.= (G | X1) . (F . x) by A16, Th47
.= G . (F . x) by A20, Th47
.= (G * F) . x by A18, Th13
.= ((G * F) | (X /\ (F " X1))) . x by A22, Th49 ; ::_thesis: verum
end;
hence  (G | X1) * (F | X) = (G * F) | (X /\ (F " X1)) by A14, Th2; ::_thesis: verum
end;

theorem :: FUNCT_1:101
for F, G being Function
for X being set holds
( X c= dom (G * F) iff ( X c= dom F & F .: X c= dom G ) )
proof
let F, G be Function; ::_thesis: for X being set holds
( X c= dom (G * F) iff ( X c= dom F & F .: X c= dom G ) )
let X be set ; ::_thesis: ( X c= dom (G * F) iff ( X c= dom F & F .: X c= dom G ) )
thus  ( X c= dom (G * F) implies ( X c= dom F & F .: X c= dom G ) ) ::_thesis: ( X c= dom F & F .: X c= dom G implies X c= dom (G * F) )
proof
assume A1: X c= dom (G * F) ; ::_thesis: ( X c= dom F & F .: X c= dom G )
then  for x being set st x in X holds
x in dom F by Th11;
hence  X c= dom F by TARSKI:def_3; ::_thesis: F .: X c= dom G
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F .: X or x in dom G )
assume  x in F .: X ; ::_thesis: x in dom G
then  ex y being set st
( y in dom F & y in X & x = F . y ) by Def6;
hence  x in dom G by A1, Th11; ::_thesis: verum
end;
assume that
A2: X c= dom F and
A3: F .: X c= dom G ; ::_thesis: X c= dom (G * F)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in dom (G * F) )
assume A4: x in X ; ::_thesis: x in dom (G * F)
then  F . x in F .: X by A2, Def6;
hence  x in dom (G * F) by A2, A3, A4, Th11; ::_thesis: verum
end;

definition
let f be Function;
assume A1: ( not f is empty & f is constant ) ;
func the_value_of f ->  set  means :: FUNCT_1:def 12
 ex x being set st
( x in dom f & it = f . x );
existence
 ex b1 being set ex x being set st
( x in dom f & b1 = f . x )
proof
consider x being set  such that
A2: x in dom f by A1, XBOOLE_0:def_1;
take  f . x ; ::_thesis: ex x being set st
( x in dom f & f . x = f . x )
thus  ex x being set st
( x in dom f & f . x = f . x ) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ex x being set st
( x in dom f & b1 = f . x ) & ex x being set st
( x in dom f & b2 = f . x ) holds
b1 = b2 by A1, Def10;
end;

:: deftheorem  defines the_value_of FUNCT_1:def_12_:_
 for f being Function st not f is empty & f is constant holds
for b2 being set holds
( b2 = the_value_of f iff ex x being set st
( x in dom f & b2 = f . x ) );

registration
let X, Y be set ;
cluster Relation-like X -defined Y -valued Function-like for set ;
existence
 ex b1 being Function st
( b1 is X -defined & b1 is Y -valued )
proof
take  {} ; ::_thesis: ( {} is X -defined & {} is Y -valued )
thus  ( dom {} c= X & rng {} c= Y ) by XBOOLE_1:2; :: according to RELAT_1:def_18,RELAT_1:def_19 ::_thesis: verum
end;
end;

theorem :: FUNCT_1:102
for X being set
for f being b1 -valued Function
for x being set st x in dom f holds
f . x in X
proof
let X be set ; ::_thesis: for f being X -valued Function
for x being set st x in dom f holds
f . x in X
let f be X -valued Function; ::_thesis: for x being set st x in dom f holds
f . x in X
let x be set ; ::_thesis: ( x in dom f implies f . x in X )
assume  x in dom f ; ::_thesis: f . x in X
then A1: f . x in rng f by Def3;
 rng f c= X by RELAT_1:def_19;
hence  f . x in X by A1; ::_thesis: verum
end;

definition
let IT be set ;
attrIT is functional  means :Def13: :: FUNCT_1:def 13
 for x being set st x in IT holds
x is Function;
end;

:: deftheorem Def13 defines functional FUNCT_1:def_13_:_
 for IT being set holds
( IT is functional iff for x being set st x in IT holds
x is Function );

registration
cluster empty  ->  functional for set ;
coherence
 for b1 being set st b1 is empty holds
b1 is functional
proof
let A be set ; ::_thesis: ( A is empty implies A is functional )
assume A1: A is empty ; ::_thesis: A is functional
let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( x in A implies x is Function )
thus  ( x in A implies x is Function ) by A1; ::_thesis: verum
end;
let f be Function;
cluster{f} ->  functional ;
coherence
 {f} is functional
proof
let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( x in {f} implies x is Function )
thus  ( x in {f} implies x is Function ) by TARSKI:def_1; ::_thesis: verum
end;
let g be Function;
cluster{f,g} ->  functional ;
coherence
 {f,g} is functional
proof
let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( x in {f,g} implies x is Function )
thus  ( x in {f,g} implies x is Function ) by TARSKI:def_2; ::_thesis: verum
end;
end;

registration
cluster non empty functional for set ;
existence
 ex b1 being set st
( not b1 is empty & b1 is functional )
proof
take  {{}} ; ::_thesis: ( not {{}} is empty & {{}} is functional )
thus  ( not {{}} is empty & {{}} is functional ) ; ::_thesis: verum
end;
end;

registration
let P be functional set ;
cluster  ->  Relation-like Function-like for Element of P;
coherence
 for b1 being Element of P holds
( b1 is Function-like & b1 is Relation-like )
proof
let x be Element of P; ::_thesis: ( x is Function-like & x is Relation-like )
percases ( P is empty or not P is empty ) ;
suppose P is empty ; ::_thesis: ( x is Function-like & x is Relation-like )
hence  ( x is Function-like & x is Relation-like ) by SUBSET_1:def_1; ::_thesis: verum
end;
suppose not P is empty ; ::_thesis: ( x is Function-like & x is Relation-like )
hence  ( x is Function-like & x is Relation-like ) by Def13; ::_thesis: verum
end;
end;
end;
end;

registration
let A be functional set ;
cluster  ->  functional for Element of bool A;
coherence
 for b1 being Subset of A holds b1 is functional
proof
let B be Subset of A; ::_thesis: B is functional
let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( x in B implies x is Function )
thus  ( x in B implies x is Function ) ; ::_thesis: verum
end;
end;

definition
let g, f be Function;
attrf is g -compatible  means :Def14: :: FUNCT_1:def 14
 for x being set st x in dom f holds
f . x in g . x;
end;

:: deftheorem Def14 defines -compatible FUNCT_1:def_14_:_
 for g, f being Function holds
( f is g -compatible iff for x being set st x in dom f holds
f . x in g . x );

theorem :: FUNCT_1:103
for f, g being Function st f is g -compatible & dom f = dom g holds
g is non-empty
proof
let f, g be Function; ::_thesis: ( f is g -compatible & dom f = dom g implies g is non-empty )
assume A1: ( f is g -compatible & dom f = dom g ) ; ::_thesis: g is non-empty
let x be set ; :: according to FUNCT_1:def_9 ::_thesis: ( x in dom g implies not g . x is empty )
assume  x in dom g ; ::_thesis: not g . x is empty
hence  not g . x is empty by A1, Def14; ::_thesis: verum
end;

theorem Th104: :: FUNCT_1:104
for f being Function holds {} is f -compatible
proof
let f be Function; ::_thesis: {} is f -compatible
let x be set ; :: according to FUNCT_1:def_14 ::_thesis: ( x in dom {} implies {} . x in f . x )
thus  ( x in dom {} implies {} . x in f . x ) ; ::_thesis: verum
end;

registration
let I be set ;
let f be Function;
cluster empty Relation-like I -defined Function-like f -compatible for set ;
existence
 ex b1 being Function st
( b1 is empty & b1 is I -defined & b1 is f -compatible )
proof
take  {} ; ::_thesis: ( {} is empty & {} is I -defined & {} is f -compatible )
thus  ( {} is empty & {} is I -defined & {} is f -compatible ) by Th104, RELAT_1:171; ::_thesis: verum
end;
end;

registration
let X be set ;
let f be Function;
let g be f -compatible Function;
clusterg | X -> f -compatible ;
coherence
 g | X is f -compatible
proof
let x be set ; :: according to FUNCT_1:def_14 ::_thesis: ( x in dom (g | X) implies (g | X) . x in f . x )
A1: dom (g | X) c= dom g by RELAT_1:60;
assume A2: x in dom (g | X) ; ::_thesis: (g | X) . x in f . x
then  g . x in f . x by A1, Def14;
hence  (g | X) . x in f . x by A2, Th47; ::_thesis: verum
end;
end;

registration
let I be set ;
cluster Relation-like non-empty I -defined Function-like for set ;
existence
 ex b1 being Function st
( b1 is non-empty & b1 is I -defined )
proof
take  {} ; ::_thesis: ( {} is non-empty & {} is I -defined )
thus  {} is non-empty ; ::_thesis: {} is I -defined
thus  dom {} c= I by XBOOLE_1:2; :: according to RELAT_1:def_18 ::_thesis: verum
end;
end;

theorem Th105: :: FUNCT_1:105
for f being Function
for g being b1 -compatible Function holds dom g c= dom f
proof
let f be Function; ::_thesis: for g being f -compatible Function holds dom g c= dom f
let g be f -compatible Function; ::_thesis: dom g c= dom f
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom g or x in dom f )
assume  x in dom g ; ::_thesis: x in dom f
then  g . x in f . x by Def14;
hence  x in dom f by Def2; ::_thesis: verum
end;

registration
let X be set ;
let f be X -defined Function;
cluster Relation-like Function-like f -compatible  -> X -defined for set ;
coherence
 for b1 being Function st b1 is f -compatible holds
b1 is X -defined
proof
let g be Function; ::_thesis: ( g is f -compatible implies g is X -defined )
assume  g is f -compatible ; ::_thesis: g is X -defined
then A1: dom g c= dom f by Th105;
 dom f c= X by RELAT_1:def_18;
hence  dom g c= X by A1, XBOOLE_1:1; :: according to RELAT_1:def_18 ::_thesis: verum
end;
end;

theorem :: FUNCT_1:106
for X, x being set
for f being b1 -valued Function st x in dom f holds
f . x is Element of X
proof
let X, x be set ; ::_thesis: for f being X -valued Function st x in dom f holds
f . x is Element of X
let f be X -valued Function; ::_thesis: ( x in dom f implies f . x is Element of X )
assume  x in dom f ; ::_thesis: f . x is Element of X
then A1: f . x in rng f by Def3;
 rng f c= X by RELAT_1:def_19;
hence  f . x is Element of X by A1; ::_thesis: verum
end;

theorem :: FUNCT_1:107
for f being Function
for A being set st f is one-to-one & A c= dom f holds
(f ") .: (f .: A) = A
proof
let f be Function; ::_thesis: for A being set st f is one-to-one & A c= dom f holds
(f ") .: (f .: A) = A
let A be set ; ::_thesis: ( f is one-to-one & A c= dom f implies (f ") .: (f .: A) = A )
set B = f .: A;
assume that
A1: f is one-to-one and
A2: A c= dom f ; ::_thesis: (f ") .: (f .: A) = A
A3: (f ") .: (f .: A) c= A
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (f ") .: (f .: A) or y in A )
assume  y in (f ") .: (f .: A) ; ::_thesis: y in A
then consider x being set  such that
 x in dom (f ") and
A4: x in f .: A and
A5: y = (f ") . x by Def6;
 ex y2 being set st
( y2 in dom f & y2 in A & x = f . y2 ) by A4, Def6;
hence  y in A by A1, A5, Th32; ::_thesis: verum
end;
 A c= (f ") .: (f .: A)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in (f ") .: (f .: A) )
assume A6: x in A ; ::_thesis: x in (f ") .: (f .: A)
set y0 = f . x;
A7: (f ") . (f . x) = x by A1, A2, A6, Th34;
 f . x in rng f by A2, A6, Def3;
then A8: f . x in dom (f ") by A1, Th33;
 f . x in f .: A by A2, A6, Def6;
hence  x in (f ") .: (f .: A) by A7, A8, Def6; ::_thesis: verum
end;
hence  (f ") .: (f .: A) = A by A3, XBOOLE_0:def_10; ::_thesis: verum
end;

registration
let A be functional set ;
let x be set ;
let F be A -valued Function;
clusterF . x ->  Relation-like Function-like ;
coherence
 ( F . x is Function-like & F . x is Relation-like )
proof
percases ( x in dom F or not x in dom F ) ;
suppose x in dom F ; ::_thesis: ( F . x is Function-like & F . x is Relation-like )
then A1: F . x in rng F by Def3;
 rng F c= A by RELAT_1:def_19;
hence  ( F . x is Function-like & F . x is Relation-like ) by A1; ::_thesis: verum
end;
suppose not x in dom F ; ::_thesis: ( F . x is Function-like & F . x is Relation-like )
hence  ( F . x is Function-like & F . x is Relation-like ) by Def2; ::_thesis: verum
end;
end;
end;
end;

theorem Th108: :: FUNCT_1:108
for x, X being set
for f being Function st x in X & x in dom f holds
f . x in f .: X
proof
let x, X be set ; ::_thesis: for f being Function st x in X & x in dom f holds
f . x in f .: X
let f be Function; ::_thesis: ( x in X & x in dom f implies f . x in f .: X )
assume that
A1: x in X and
A2: x in dom f ; ::_thesis: f . x in f .: X
 x in X /\ (dom f) by A1, A2, XBOOLE_0:def_4;
then  x in dom (f | X) by RELAT_1:61;
then A3: (f | X) . x in rng (f | X) by Def3;
 (f | X) . x = f . x by A1, Th49;
hence  f . x in f .: X by A3, RELAT_1:115; ::_thesis: verum
end;

theorem :: FUNCT_1:109
for X being set
for f being Function st X <> {} & X c= dom f holds
f .: X <> {}
proof
let X be set ; ::_thesis: for f being Function st X <> {} & X c= dom f holds
f .: X <> {}
let f be Function; ::_thesis: ( X <> {} & X c= dom f implies f .: X <> {} )
assume  X <> {} ; ::_thesis: ( not X c= dom f or f .: X <> {} )
then  ex x being set st x in X by XBOOLE_0:def_1;
hence  ( not X c= dom f or f .: X <> {} ) by Th108; ::_thesis: verum
end;

registration
let f be non trivial Function;
cluster dom f ->  non trivial ;
coherence
 not dom f is trivial
proof
consider u, w being set  such that
A1: u in f and
A2: w in f and
A3: u <> w by ZFMISC_1:def_10;
consider u1, u2 being set  such that
A4: u = [u1,u2] by A1, RELAT_1:def_1;
consider w1, w2 being set  such that
A5: w = [w1,w2] by A2, RELAT_1:def_1;
take  u1 ; :: according to ZFMISC_1:def_10 ::_thesis: ex b1 being set st
( u1 in dom f & b1 in dom f & not u1 = b1 )
take  w1 ; ::_thesis: ( u1 in dom f & w1 in dom f & not u1 = w1 )
thus  ( u1 in dom f & w1 in dom f ) by A4, A5, A1, A2, XTUPLE_0:def_12; ::_thesis: not u1 = w1
thus  u1 <> w1 by A1, A2, A3, A4, A5, Def1; ::_thesis: verum
end;
end;

theorem :: FUNCT_1:110
for B being non empty functional set
for f being Function st f = union B holds
( dom f = union  {  (dom g) where g is Element of B : verum  }  & rng f = union  {  (rng g) where g is Element of B : verum  }  )
proof
let B be non empty functional set ; ::_thesis: for f being Function st f = union B holds
( dom f = union  {  (dom g) where g is Element of B : verum  }  & rng f = union  {  (rng g) where g is Element of B : verum  }  )
let f be Function; ::_thesis: ( f = union B implies ( dom f = union  {  (dom g) where g is Element of B : verum  }  & rng f = union  {  (rng g) where g is Element of B : verum  }  ) )
assume A1: f = union B ; ::_thesis: ( dom f = union  {  (dom g) where g is Element of B : verum  }  & rng f = union  {  (rng g) where g is Element of B : verum  }  )
set X =  {  (dom g) where g is Element of B : verum  }  ;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_dom_f_implies_ex_Z_being_set_st_
(_x_in_Z_&_Z_in__{__(dom_g)_where_g_is_Element_of_B_:_verum__}__)_)_&_(_ex_Z_being_set_st_
(_x_in_Z_&_Z_in__{__(dom_g)_where_g_is_Element_of_B_:_verum__}__)_implies_x_in_dom_f_)_)
let x be set ; ::_thesis: ( ( x in dom f implies ex Z being set st
( x in Z & Z in  {  (dom g) where g is Element of B : verum  }  ) ) & ( ex Z being set st
( x in Z & Z in  {  (dom g) where g is Element of B : verum  }  ) implies x in dom f ) )
hereby  ::_thesis: ( ex Z being set st
( x in Z & Z in  {  (dom g) where g is Element of B : verum  }  ) implies x in dom f )
assume  x in dom f ; ::_thesis: ex Z being set st
( x in Z & Z in  {  (dom g) where g is Element of B : verum  }  )
then  [x,(f . x)] in f by Th1;
then consider g being set  such that
A2: [x,(f . x)] in g and
A3: g in B by A1, TARSKI:def_4;
reconsider g = g as Function by A3;
take Z = dom g; ::_thesis: ( x in Z & Z in  {  (dom g) where g is Element of B : verum  }  )
thus  ( x in Z & Z in  {  (dom g) where g is Element of B : verum  }  ) by A2, A3, Th1; ::_thesis: verum
end;
given Z being set  such that A4: x in Z and
A5: Z in  {  (dom g) where g is Element of B : verum  }  ; ::_thesis: x in dom f
consider g being Element of B such that
A6: Z = dom g by A5;
 [x,(g . x)] in g by A4, A6, Th1;
then  [x,(g . x)] in f by A1, TARSKI:def_4;
hence  x in dom f by Th1; ::_thesis: verum
end;
hence  dom f = union  {  (dom g) where g is Element of B : verum  }  by TARSKI:def_4; ::_thesis: rng f = union  {  (rng g) where g is Element of B : verum  }
set X =  {  (rng g) where g is Element of B : verum  }  ;
now__::_thesis:_for_y_being_set_holds_
(_(_y_in_rng_f_implies_ex_Z_being_set_st_
(_y_in_Z_&_Z_in__{__(rng_g)_where_g_is_Element_of_B_:_verum__}__)_)_&_(_ex_Z_being_set_st_
(_y_in_Z_&_Z_in__{__(rng_g)_where_g_is_Element_of_B_:_verum__}__)_implies_y_in_rng_f_)_)
let y be set ; ::_thesis: ( ( y in rng f implies ex Z being set st
( y in Z & Z in  {  (rng g) where g is Element of B : verum  }  ) ) & ( ex Z being set st
( y in Z & Z in  {  (rng g) where g is Element of B : verum  }  ) implies y in rng f ) )
hereby  ::_thesis: ( ex Z being set st
( y in Z & Z in  {  (rng g) where g is Element of B : verum  }  ) implies y in rng f )
assume  y in rng f ; ::_thesis: ex Z being set st
( y in Z & Z in  {  (rng g) where g is Element of B : verum  }  )
then consider x being set  such that
A7: ( x in dom f & y = f . x ) by Def3;
 [x,y] in f by A7, Th1;
then consider g being set  such that
A8: [x,y] in g and
A9: g in B by A1, TARSKI:def_4;
reconsider g = g as Function by A9;
take Z = rng g; ::_thesis: ( y in Z & Z in  {  (rng g) where g is Element of B : verum  }  )
 ( x in dom g & y = g . x ) by A8, Th1;
hence  ( y in Z & Z in  {  (rng g) where g is Element of B : verum  }  ) by A9, Def3; ::_thesis: verum
end;
given Z being set  such that A10: y in Z and
A11: Z in  {  (rng g) where g is Element of B : verum  }  ; ::_thesis: y in rng f
consider g being Element of B such that
A12: Z = rng g by A11;
consider x being set  such that
A13: ( x in dom g & y = g . x ) by A10, A12, Def3;
 [x,y] in g by A13, Th1;
then  [x,y] in f by A1, TARSKI:def_4;
hence  y in rng f by XTUPLE_0:def_13; ::_thesis: verum
end;
hence  rng f = union  {  (rng g) where g is Element of B : verum  }  by TARSKI:def_4; ::_thesis: verum
end;

theorem Th111: :: FUNCT_1:111
for M being set st ( for X being set st X in M holds
X <> {} ) holds
ex f being Function st
( dom f = M & ( for X being set st X in M holds
f . X in X ) )
proof
let M be set ; ::_thesis: ( ( for X being set st X in M holds
X <> {} ) implies ex f being Function st
( dom f = M & ( for X being set st X in M holds
f . X in X ) ) )
assume A1: for X being set st X in M holds
X <> {} ; ::_thesis: ex f being Function st
( dom f = M & ( for X being set st X in M holds
f . X in X ) )
deffunc H1( set ) ->  Element of $1 = the Element of $1;
consider f being Function such that
A2: dom f = M and
A3: for x being set st x in M holds
f . x = H1(x) from FUNCT_1:sch_3();
take  f ; ::_thesis: ( dom f = M & ( for X being set st X in M holds
f . X in X ) )
thus  dom f = M by A2; ::_thesis: for X being set st X in M holds
f . X in X
let X be set ; ::_thesis: ( X in M implies f . X in X )
assume A4: X in M ; ::_thesis: f . X in X
then A5: f . X = the Element of X by A3;
 X <> {} by A1, A4;
hence  f . X in X by A5; ::_thesis: verum
end;

scheme :: FUNCT_1:sch 5
NonUniqBoundFuncEx{ F1() ->  set , F2() ->  set , P1[ set , set ] } :
 ex f being Function st
( dom f = F1() & rng f c= F2() & ( for x being set st x in F1() holds
P1[x,f . x] ) )
provided
A1: for x being set st x in F1() holds
ex y being set st
( y in F2() & P1[x,y] )
proof
percases ( F1() = {} or F1() <> {} ) ;
supposeA2: F1() = {} ; ::_thesis: ex f being Function st
( dom f = F1() & rng f c= F2() & ( for x being set st x in F1() holds
P1[x,f . x] ) )
take  {} ; ::_thesis: ( dom {} = F1() & rng {} c= F2() & ( for x being set st x in F1() holds
P1[x,{} . x] ) )
thus  ( dom {} = F1() & rng {} c= F2() & ( for x being set st x in F1() holds
P1[x,{} . x] ) ) by A2, XBOOLE_1:2; ::_thesis: verum
end;
supposeA3: F1() <> {} ; ::_thesis: ex f being Function st
( dom f = F1() & rng f c= F2() & ( for x being set st x in F1() holds
P1[x,f . x] ) )
defpred S1[ set , set ] means  for y being set holds
( y in $2 iff ( y in F2() & P1[$1,y] ) );
A4: for e, u1, u2 being set st e in F1() & S1[e,u1] & S1[e,u2] holds
u1 = u2
proof
let e, u1, u2 be set ; ::_thesis: ( e in F1() & S1[e,u1] & S1[e,u2] implies u1 = u2 )
assume  e in F1() ; ::_thesis: ( not S1[e,u1] or not S1[e,u2] or u1 = u2 )
assume A5: for y being set holds
( y in u1 iff ( y in F2() & P1[e,y] ) ) ; ::_thesis: ( not S1[e,u2] or u1 = u2 )
defpred S2[ set ] means ( $1 in F2() & P1[e,$1] );
A6: for x being set holds
( x in u1 iff S2[x] ) by A5;
assume A7: for y being set holds
( y in u2 iff ( y in F2() & P1[e,y] ) ) ; ::_thesis: u1 = u2
A8: for x being set holds
( x in u2 iff S2[x] ) by A7;
 u1 = u2 from XBOOLE_0:sch_2(A6, A8);
hence  u1 = u2 ; ::_thesis: verum
end;
A9: for x being set st x in F1() holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in F1() implies ex y being set st S1[x,y] )
assume  x in F1() ; ::_thesis: ex y being set st S1[x,y]
defpred S2[ set ] means P1[x,$1];
consider X being set  such that
A10: for y being set holds
( y in X iff ( y in F2() & S2[y] ) ) from XBOOLE_0:sch_1();
take  X ; ::_thesis: S1[x,X]
thus  S1[x,X] by A10; ::_thesis: verum
end;
consider G being Function such that
A11: ( dom G = F1() & ( for x being set st x in F1() holds
S1[x,G . x] ) ) from FUNCT_1:sch_2(A4, A9);
reconsider D = rng G as non empty set by A11, A3, RELAT_1:42;
now__::_thesis:_for_X_being_set_st_X_in_D_holds_
X_<>_{}
let X be set ; ::_thesis: ( X in D implies X <> {} )
assume  X in D ; ::_thesis: X <> {}
then consider x being set  such that
A12: ( x in dom G & X = G . x ) by Def3;
 ( ( for y being set holds
( y in X iff ( y in F2() & P1[x,y] ) ) ) & ex y being set st
( y in F2() & P1[x,y] ) ) by A1, A11, A12;
hence  X <> {} ; ::_thesis: verum
end;
then consider F being Function such that
A13: dom F = D and
A14: for X being set st X in D holds
F . X in X by Th111;
A15: dom (F * G) = F1() by A11, A13, RELAT_1:27;
take f = F * G; ::_thesis: ( dom f = F1() & rng f c= F2() & ( for x being set st x in F1() holds
P1[x,f . x] ) )
thus  dom f = F1() by A11, A13, RELAT_1:27; ::_thesis: ( rng f c= F2() & ( for x being set st x in F1() holds
P1[x,f . x] ) )
 rng F c= F2()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng F or x in F2() )
assume  x in rng F ; ::_thesis: x in F2()
then consider y being set  such that
A16: y in dom F and
A17: x = F . y by Def3;
A18: ex z being set st
( z in dom G & y = G . z ) by A13, A16, Def3;
 x in y by A13, A14, A16, A17;
hence  x in F2() by A11, A18; ::_thesis: verum
end;
hence  rng f c= F2() by A13, RELAT_1:28; ::_thesis: for x being set st x in F1() holds
P1[x,f . x]
let x be set ; ::_thesis: ( x in F1() implies P1[x,f . x] )
assume A19: x in F1() ; ::_thesis: P1[x,f . x]
then  ( f . x = F . (G . x) & G . x in D ) by A11, A15, Th12, Def3;
then  f . x in G . x by A14;
hence  P1[x,f . x] by A11, A19; ::_thesis: verum
end;
end;
end;

registration
let f be empty-yielding Function;
let x be set ;
clusterf . x ->  empty ;
coherence
 f . x is empty
proof
 ( x in dom f or not x in dom f ) ;
hence  f . x is empty by Def2, Def8; ::_thesis: verum
end;
end;