:: FUNCT_2 semantic presentation

begin


definition
let X, Y be set ;
let R be Relation of X,Y;
attrR is quasi_total  means :Def1: :: FUNCT_2:def 1
X = dom R if Y <> {}
otherwise R = {} ;
consistency
 verum ;
end;

:: deftheorem Def1 defines quasi_total FUNCT_2:def_1_:_
 for X, Y being set
for R being Relation of X,Y holds
( ( Y <> {} implies ( R is quasi_total iff X = dom R ) ) & ( not Y <> {} implies ( R is quasi_total iff R = {} ) ) );

registration
let X, Y be set ;
cluster Relation-like X -defined Y -valued Function-like quasi_total for Element of bool [:X,Y:];
existence
 ex b1 being PartFunc of X,Y st b1 is quasi_total
proof
percases ( Y = {} or Y <> {} ) ;
supposeA1: Y = {} ; ::_thesis: ex b1 being PartFunc of X,Y st b1 is quasi_total
reconsider R = {} as PartFunc of X,Y by RELSET_1:12;
take  R ; ::_thesis: R is quasi_total
thus  R is quasi_total by A1, Def1; ::_thesis: verum
end;
supposeA2: Y <> {} ; ::_thesis: ex b1 being PartFunc of X,Y st b1 is quasi_total
then consider f being Function such that
A3: X = dom f and
A4: rng f c= Y by FUNCT_1:8;
reconsider R = f as PartFunc of X,Y by A3, A4, RELSET_1:4;
take  R ; ::_thesis: R is quasi_total
thus  R is quasi_total by A2, A3, Def1; ::_thesis: verum
end;
end;
end;
end;

registration
let X, Y be set ;
cluster total  ->  quasi_total for Element of bool [:X,Y:];
coherence
 for b1 being Relation of X,Y st b1 is total holds
b1 is quasi_total
proof
let f be Relation of X,Y; ::_thesis: ( f is total implies f is quasi_total )
assume A1: dom f = X ; :: according to PARTFUN1:def_2 ::_thesis: f is quasi_total
percases ( Y <> {} or Y = {} ) ;
:: according to FUNCT_2:def_1
case Y <> {} ; ::_thesis: X = dom f
thus  X = dom f by A1; ::_thesis: verum
end;
case Y = {} ; ::_thesis: f = {}
hence  f = {} ; ::_thesis: verum
end;
end;
end;
end;

definition
let X, Y be set ;
mode Function of X,Y is quasi_total PartFunc of X,Y;
end;

registration
let X be empty set ;
let Y be set ;
cluster quasi_total  ->  total for Element of bool [:X,Y:];
coherence
 for b1 being Relation of X,Y st b1 is quasi_total holds
b1 is total ;
end;

registration
let X be set ;
let Y be non empty set ;
cluster quasi_total  ->  total for Element of bool [:X,Y:];
coherence
 for b1 being Relation of X,Y st b1 is quasi_total holds
b1 is total
proof
let F be Relation of X,Y; ::_thesis: ( F is quasi_total implies F is total )
assume  F is quasi_total ; ::_thesis: F is total
hence  X = dom F by Def1; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
end;

registration
let X be set ;
cluster quasi_total  ->  total for Element of bool [:X,X:];
coherence
 for b1 being Relation of X,X st b1 is quasi_total holds
b1 is total
proof
percases ( X = {} or X <> {} ) ;
suppose X = {} ; ::_thesis: for b1 being Relation of X,X st b1 is quasi_total holds
b1 is total
hence  for b1 being Relation of X,X st b1 is quasi_total holds
b1 is total ; ::_thesis: verum
end;
suppose X <> {} ; ::_thesis: for b1 being Relation of X,X st b1 is quasi_total holds
b1 is total
hence  for b1 being Relation of X,X st b1 is quasi_total holds
b1 is total ; ::_thesis: verum
end;
end;
end;
end;

theorem :: FUNCT_2:1
for f being Function holds f is Function of (dom f),(rng f)
proof
let f be Function; ::_thesis: f is Function of (dom f),(rng f)
reconsider R = f as Relation of (dom f),(rng f) by RELSET_1:4;
 ( rng R <> {} or rng R = {} ) ;
hence  f is Function of (dom f),(rng f) by Def1; ::_thesis: verum
end;

theorem Th2: :: FUNCT_2:2
for Y being set
for f being Function st rng f c= Y holds
f is Function of (dom f),Y
proof
let Y be set ; ::_thesis: for f being Function st rng f c= Y holds
f is Function of (dom f),Y
let f be Function; ::_thesis: ( rng f c= Y implies f is Function of (dom f),Y )
assume  rng f c= Y ; ::_thesis: f is Function of (dom f),Y
then reconsider R = f as Relation of (dom f),Y by RELSET_1:4;
 ( Y = {} or Y <> {} ) ;
then  R is quasi_total by Def1;
hence  f is Function of (dom f),Y ; ::_thesis: verum
end;

theorem :: FUNCT_2:3
for X, Y being set
for f being Function st dom f = X & ( for x being set st x in X holds
f . x in Y ) holds
f is Function of X,Y
proof
let X, Y be set ; ::_thesis: for f being Function st dom f = X & ( for x being set st x in X holds
f . x in Y ) holds
f is Function of X,Y
let f be Function; ::_thesis: ( dom f = X & ( for x being set st x in X holds
f . x in Y ) implies f is Function of X,Y )
assume that
A1: dom f = X and
A2: for x being set st x in X holds
f . x in Y ; ::_thesis: f is Function of X,Y
 rng f c= Y
proof
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  ex x being set st
( x in X & y = f . x ) by A1, FUNCT_1:def_3;
hence  y in Y by A2; ::_thesis: verum
end;
then reconsider R = f as Relation of (dom f),Y by RELSET_1:4;
 ( Y = {} or Y <> {} ) ;
then  R is quasi_total by Def1;
hence  f is Function of X,Y by A1; ::_thesis: verum
end;

theorem Th4: :: FUNCT_2:4
for X, Y, x being set
for f being Function of X,Y st Y <> {} & x in X holds
f . x in rng f
proof
let X, Y, x be set ; ::_thesis: for f being Function of X,Y st Y <> {} & x in X holds
f . x in rng f
let f be Function of X,Y; ::_thesis: ( Y <> {} & x in X implies f . x in rng f )
assume  Y <> {} ; ::_thesis: ( not x in X or f . x in rng f )
then  dom f = X by Def1;
hence  ( not x in X or f . x in rng f ) by FUNCT_1:def_3; ::_thesis: verum
end;

theorem Th5: :: FUNCT_2:5
for X, Y, x being set
for f being Function of X,Y st Y <> {} & x in X holds
f . x in Y
proof
let X, Y, x be set ; ::_thesis: for f being Function of X,Y st Y <> {} & x in X holds
f . x in Y
let f be Function of X,Y; ::_thesis: ( Y <> {} & x in X implies f . x in Y )
assume  ( Y <> {} & x in X ) ; ::_thesis: f . x in Y
then  f . x in rng f by Th4;
hence  f . x in Y ; ::_thesis: verum
end;

theorem :: FUNCT_2:6
for X, Y, Z being set
for f being Function of X,Y st ( Y = {} implies X = {} ) & rng f c= Z holds
f is Function of X,Z
proof
let X, Y, Z be set ; ::_thesis: for f being Function of X,Y st ( Y = {} implies X = {} ) & rng f c= Z holds
f is Function of X,Z
let f be Function of X,Y; ::_thesis: ( ( Y = {} implies X = {} ) & rng f c= Z implies f is Function of X,Z )
assume  ( Y <> {} or X = {} ) ; ::_thesis: ( not rng f c= Z or f is Function of X,Z )
then A1: dom f = X by Def1;
assume A2: rng f c= Z ; ::_thesis: f is Function of X,Z
now__::_thesis:_(_Z_=_{}_implies_X_=_{}_)
assume  Z = {} ; ::_thesis: X = {}
then  rng f = {} by A2;
hence  X = {} by A1, RELAT_1:42; ::_thesis: verum
end;
hence  f is Function of X,Z by A1, A2, Def1, RELSET_1:4; ::_thesis: verum
end;

theorem :: FUNCT_2:7
for X, Y, Z being set
for f being Function of X,Y st ( Y = {} implies X = {} ) & Y c= Z holds
f is Function of X,Z by RELSET_1:7;

scheme :: FUNCT_2:sch 1
FuncEx1{ F1() ->  set , F2() ->  set , P1[ set , set ] } :
 ex f being Function of F1(),F2() st
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
consider f being Function such that
A2: ( dom f = F1() & rng f c= F2() ) and
A3: for x being set st x in F1() holds
P1[x,f . x] from FUNCT_1:sch_5(A1);
reconsider f = f as Function of F1(),F2() by A2, Th2;
take  f ; ::_thesis: for x being set st x in F1() holds
P1[x,f . x]
thus  for x being set st x in F1() holds
P1[x,f . x] by A3; ::_thesis: verum
end;

scheme :: FUNCT_2:sch 2
Lambda1{ F1() ->  set , F2() ->  set , F3( set ) ->  set } :
 ex f being Function of F1(),F2() st
for x being set st x in F1() holds
f . x = F3(x)
provided
A1: for x being set st x in F1() holds
F3(x) in F2()
proof
defpred S1[ set , set ] means $2 = F3($1);
A2: for x being set st x in F1() holds
ex y being set st
( y in F2() & S1[x,y] ) by A1;
thus  ex f being Function of F1(),F2() st
for x being set st x in F1() holds
S1[x,f . x] from FUNCT_2:sch_1(A2); ::_thesis: verum
end;

definition
let X, Y be set ;
func Funcs (X,Y) ->  set  means :Def2: :: FUNCT_2:def 2
 for x being set holds
( x in it iff ex f being Function st
( x = f & dom f = X & rng f c= Y ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex f being Function st
( x = f & dom f = X & rng f c= Y ) )
proof
defpred S1[ set ] means  ex f being Function st
( $1 = f & dom f = X & rng f c= Y );
consider F being set  such that
A1: for z being set holds
( z in F iff ( z in bool [:X,Y:] & S1[z] ) ) from XBOOLE_0:sch_1();
take  F ; ::_thesis: for x being set holds
( x in F iff ex f being Function st
( x = f & dom f = X & rng f c= Y ) )
let z be set ; ::_thesis: ( z in F iff ex f being Function st
( z = f & dom f = X & rng f c= Y ) )
thus  ( z in F implies ex f being Function st
( z = f & dom f = X & rng f c= Y ) ) by A1; ::_thesis: ( ex f being Function st
( z = f & dom f = X & rng f c= Y ) implies z in F )
given f being Function such that A2: z = f and
A3: ( dom f = X & rng f c= Y ) ; ::_thesis: z in F
 f c= [:X,Y:]
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in f or p in [:X,Y:] )
assume A4: p in f ; ::_thesis: p in [:X,Y:]
then consider x, y being set  such that
A5: p = [x,y] by RELAT_1:def_1;
A6: x in dom f by A4, A5, XTUPLE_0:def_12;
then  y = f . x by A4, A5, FUNCT_1:def_2;
then  y in rng f by A6, FUNCT_1:def_3;
hence  p in [:X,Y:] by A3, A5, A6, ZFMISC_1:def_2; ::_thesis: verum
end;
hence  z in F by A1, A2, A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex f being Function st
( x = f & dom f = X & rng f c= Y ) ) ) & ( for x being set holds
( x in b2 iff ex f being Function st
( x = f & dom f = X & rng f c= Y ) ) ) holds
b1 = b2
proof
let F1, F2 be set ; ::_thesis: ( ( for x being set holds
( x in F1 iff ex f being Function st
( x = f & dom f = X & rng f c= Y ) ) ) & ( for x being set holds
( x in F2 iff ex f being Function st
( x = f & dom f = X & rng f c= Y ) ) ) implies F1 = F2 )
assume that
A7: for x being set holds
( x in F1 iff ex f being Function st
( x = f & dom f = X & rng f c= Y ) ) and
A8: for x being set holds
( x in F2 iff ex f being Function st
( x = f & dom f = X & rng f c= Y ) ) ; ::_thesis: F1 = F2
 for x being set holds
( x in F1 iff x in F2 )
proof
let x be set ; ::_thesis: ( x in F1 iff x in F2 )
 ( x in F1 iff ex f being Function st
( x = f & dom f = X & rng f c= Y ) ) by A7;
hence  ( x in F1 iff x in F2 ) by A8; ::_thesis: verum
end;
hence  F1 = F2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines Funcs FUNCT_2:def_2_:_
 for X, Y, b3 being set holds
( b3 = Funcs (X,Y) iff for x being set holds
( x in b3 iff ex f being Function st
( x = f & dom f = X & rng f c= Y ) ) );

theorem Th8: :: FUNCT_2:8
for X, Y being set
for f being Function of X,Y st ( Y = {} implies X = {} ) holds
f in Funcs (X,Y)
proof
let X, Y be set ; ::_thesis: for f being Function of X,Y st ( Y = {} implies X = {} ) holds
f in Funcs (X,Y)
let f be Function of X,Y; ::_thesis: ( ( Y = {} implies X = {} ) implies f in Funcs (X,Y) )
assume  ( Y = {} implies X = {} ) ; ::_thesis: f in Funcs (X,Y)
then A1: dom f = X by Def1;
 rng f c= Y ;
hence  f in Funcs (X,Y) by A1, Def2; ::_thesis: verum
end;

theorem :: FUNCT_2:9
for X being set
for f being Function of X,X holds f in Funcs (X,X) by Th8;

registration
let X be set ;
let Y be non empty set ;
cluster Funcs (X,Y) ->  non empty ;
coherence
 not Funcs (X,Y) is empty by Th8;
end;

registration
let X be set ;
cluster Funcs (X,X) ->  non empty ;
coherence
 not Funcs (X,X) is empty by Th8;
end;

registration
let X be non empty set ;
let Y be empty set ;
cluster Funcs (X,Y) ->  empty ;
coherence
 Funcs (X,Y) is empty
proof
assume  not Funcs (X,Y) is empty ; ::_thesis: contradiction
then consider f being Function such that
 the Element of Funcs (X,Y) = f and
A1: dom f = X and
A2: rng f c= {} by Def2;
 rng f = {} by A2;
hence  contradiction by A1, RELAT_1:42; ::_thesis: verum
end;
end;

theorem :: FUNCT_2:10
for X, Y being set
for f being Function of X,Y st ( for y being set st y in Y holds
ex x being set st
( x in X & y = f . x ) ) holds
rng f = Y
proof
let X, Y be set ; ::_thesis: for f being Function of X,Y st ( for y being set st y in Y holds
ex x being set st
( x in X & y = f . x ) ) holds
rng f = Y
let f be Function of X,Y; ::_thesis: ( ( for y being set st y in Y holds
ex x being set st
( x in X & y = f . x ) ) implies rng f = Y )
assume A1: for y being set st y in Y holds
ex x being set st
( x in X & y = f . x ) ; ::_thesis: rng f = Y
percases ( Y = {} or Y <> {} ) ;
suppose Y = {} ; ::_thesis: rng f = Y
hence  rng f = Y ; ::_thesis: verum
end;
supposeA2: Y <> {} ; ::_thesis: rng f = Y
 for y being set holds
( y in rng f iff y in Y )
proof
let y be set ; ::_thesis: ( y in rng f iff y in Y )
 dom f = X by A2, Def1;
then  ( y in rng f iff ex x being set st
( x in X & y = f . x ) ) by FUNCT_1:def_3;
hence  ( y in rng f iff y in Y ) by A1; ::_thesis: verum
end;
hence  rng f = Y by TARSKI:1; ::_thesis: verum
end;
end;
end;

theorem Th11: :: FUNCT_2:11
for X, Y, y being set
for f being Function of X,Y st y in rng f holds
ex x being set st
( x in X & f . x = y )
proof
let X, Y, y be set ; ::_thesis: for f being Function of X,Y st y in rng f holds
ex x being set st
( x in X & f . x = y )
let f be Function of X,Y; ::_thesis: ( y in rng f implies ex x being set st
( x in X & f . x = y ) )
assume A1: y in rng f ; ::_thesis: ex x being set st
( x in X & f . x = y )
then  dom f = X by Def1;
hence  ex x being set st
( x in X & f . x = y ) by A1, FUNCT_1:def_3; ::_thesis: verum
end;

theorem Th12: :: FUNCT_2:12
for X, Y being set
for f1, f2 being Function of X,Y st ( for x being set st x in X holds
f1 . x = f2 . x ) holds
f1 = f2
proof
let X, Y be set ; ::_thesis: for f1, f2 being Function of X,Y st ( for x being set st x in X holds
f1 . x = f2 . x ) holds
f1 = f2
let f1, f2 be Function of X,Y; ::_thesis: ( ( for x being set st x in X holds
f1 . x = f2 . x ) implies f1 = f2 )
percases ( Y = {} or Y <> {} ) ;
suppose Y = {} ; ::_thesis: ( ( for x being set st x in X holds
f1 . x = f2 . x ) implies f1 = f2 )
hence  ( ( for x being set st x in X holds
f1 . x = f2 . x ) implies f1 = f2 ) ; ::_thesis: verum
end;
suppose Y <> {} ; ::_thesis: ( ( for x being set st x in X holds
f1 . x = f2 . x ) implies f1 = f2 )
then  ( dom f1 = X & dom f2 = X ) by Def1;
hence  ( ( for x being set st x in X holds
f1 . x = f2 . x ) implies f1 = f2 ) by FUNCT_1:2; ::_thesis: verum
end;
end;
end;

theorem Th13: :: FUNCT_2:13
for X, Y, Z being set
for f being quasi_total Relation of X,Y
for g being quasi_total Relation of Y,Z st ( not Y = {} or Z = {} or X = {} ) holds
f * g is quasi_total
proof
let X, Y, Z be set ; ::_thesis: for f being quasi_total Relation of X,Y
for g being quasi_total Relation of Y,Z st ( not Y = {} or Z = {} or X = {} ) holds
f * g is quasi_total
let f be quasi_total Relation of X,Y; ::_thesis: for g being quasi_total Relation of Y,Z st ( not Y = {} or Z = {} or X = {} ) holds
f * g is quasi_total
let g be quasi_total Relation of Y,Z; ::_thesis: ( ( not Y = {} or Z = {} or X = {} ) implies f * g is quasi_total )
assume A1: ( not Y = {} or Z = {} or X = {} ) ; ::_thesis: f * g is quasi_total
percases ( Z <> {} or Z = {} ) ;
:: according to FUNCT_2:def_1
caseA2: Z <> {} ; ::_thesis: X = dom (f * g)
then A3: dom g = Y by Def1;
 ( dom f = X & rng f c= Y ) by A1, A2, Def1;
hence  X = dom (f * g) by A3, RELAT_1:27; ::_thesis: verum
end;
case Z = {} ; ::_thesis: f * g = {}
hence  f * g = {} ; ::_thesis: verum
end;
end;
end;

theorem :: FUNCT_2:14
for X, Y, Z being set
for f being Function of X,Y
for g being Function of Y,Z st Z <> {} & rng f = Y & rng g = Z holds
rng (g * f) = Z
proof
let X, Y, Z be set ; ::_thesis: for f being Function of X,Y
for g being Function of Y,Z st Z <> {} & rng f = Y & rng g = Z holds
rng (g * f) = Z
let f be Function of X,Y; ::_thesis: for g being Function of Y,Z st Z <> {} & rng f = Y & rng g = Z holds
rng (g * f) = Z
let g be Function of Y,Z; ::_thesis: ( Z <> {} & rng f = Y & rng g = Z implies rng (g * f) = Z )
assume  Z <> {} ; ::_thesis: ( not rng f = Y or not rng g = Z or rng (g * f) = Z )
then  dom g = Y by Def1;
hence  ( not rng f = Y or not rng g = Z or rng (g * f) = Z ) by RELAT_1:28; ::_thesis: verum
end;

theorem Th15: :: FUNCT_2:15
for X, Y, x being set
for f being Function of X,Y
for g being Function st Y <> {} & x in X holds
(g * f) . x = g . (f . x)
proof
let X, Y, x be set ; ::_thesis: for f being Function of X,Y
for g being Function st Y <> {} & x in X holds
(g * f) . x = g . (f . x)
let f be Function of X,Y; ::_thesis: for g being Function st Y <> {} & x in X holds
(g * f) . x = g . (f . x)
let g be Function; ::_thesis: ( Y <> {} & x in X implies (g * f) . x = g . (f . x) )
assume  Y <> {} ; ::_thesis: ( not x in X or (g * f) . x = g . (f . x) )
then  X = dom f by Def1;
hence  ( not x in X or (g * f) . x = g . (f . x) ) by FUNCT_1:13; ::_thesis: verum
end;

theorem :: FUNCT_2:16
for X, Y being set
for f being Function of X,Y st Y <> {} holds
( rng f = Y iff for Z being set st Z <> {} holds
for g, h being Function of Y,Z st g * f = h * f holds
g = h )
proof
let X, Y be set ; ::_thesis: for f being Function of X,Y st Y <> {} holds
( rng f = Y iff for Z being set st Z <> {} holds
for g, h being Function of Y,Z st g * f = h * f holds
g = h )
let f be Function of X,Y; ::_thesis: ( Y <> {} implies ( rng f = Y iff for Z being set st Z <> {} holds
for g, h being Function of Y,Z st g * f = h * f holds
g = h ) )
assume A1: Y <> {} ; ::_thesis: ( rng f = Y iff for Z being set st Z <> {} holds
for g, h being Function of Y,Z st g * f = h * f holds
g = h )
thus  ( rng f = Y implies for Z being set st Z <> {} holds
for g, h being Function of Y,Z st g * f = h * f holds
g = h ) ::_thesis: ( ( for Z being set st Z <> {} holds
for g, h being Function of Y,Z st g * f = h * f holds
g = h ) implies rng f = Y )
proof
assume A2: rng f = Y ; ::_thesis: for Z being set st Z <> {} holds
for g, h being Function of Y,Z st g * f = h * f holds
g = h
let Z be set ; ::_thesis: ( Z <> {} implies for g, h being Function of Y,Z st g * f = h * f holds
g = h )
assume A3: Z <> {} ; ::_thesis: for g, h being Function of Y,Z st g * f = h * f holds
g = h
let g, h be Function of Y,Z; ::_thesis: ( g * f = h * f implies g = h )
 ( dom g = Y & dom h = Y ) by A3, Def1;
hence  ( g * f = h * f implies g = h ) by A2, FUNCT_1:86; ::_thesis: verum
end;
assume A4: for Z being set st Z <> {} holds
for g, h being Function of Y,Z st g * f = h * f holds
g = h ; ::_thesis: rng f = Y
 for g, h being Function st dom g = Y & dom h = Y & g * f = h * f holds
g = h
proof
let g, h be Function; ::_thesis: ( dom g = Y & dom h = Y & g * f = h * f implies g = h )
assume that
A5: dom g = Y and
A6: dom h = Y ; ::_thesis: ( not g * f = h * f or g = h )
A7: rng g <> {} by A1, A5, RELAT_1:42;
A8: g is Function of Y,((rng g) \/ (rng h)) by A5, Th2, XBOOLE_1:7;
 h is Function of Y,((rng g) \/ (rng h)) by A6, Th2, XBOOLE_1:7;
hence  ( not g * f = h * f or g = h ) by A4, A7, A8; ::_thesis: verum
end;
hence  rng f = Y by FUNCT_1:16; ::_thesis: verum
end;

theorem :: FUNCT_2:17
for X, Y being set
for f being Relation of X,Y holds
( (id X) * f = f & f * (id Y) = f )
proof
let X, Y be set ; ::_thesis: for f being Relation of X,Y holds
( (id X) * f = f & f * (id Y) = f )
let f be Relation of X,Y; ::_thesis: ( (id X) * f = f & f * (id Y) = f )
 dom f c= X ;
hence  (id X) * f = f by RELAT_1:51; ::_thesis: f * (id Y) = f
 rng f c= Y ;
hence  f * (id Y) = f by RELAT_1:53; ::_thesis: verum
end;

theorem :: FUNCT_2:18
for X, Y being set
for f being Function of X,Y
for g being Function of Y,X st f * g = id Y holds
rng f = Y
proof
let X, Y be set ; ::_thesis: for f being Function of X,Y
for g being Function of Y,X st f * g = id Y holds
rng f = Y
let f be Function of X,Y; ::_thesis: for g being Function of Y,X st f * g = id Y holds
rng f = Y
let g be Function of Y,X; ::_thesis: ( f * g = id Y implies rng f = Y )
assume  f * g = id Y ; ::_thesis: rng f = Y
then  rng (f * g) = Y by RELAT_1:45;
then  Y c= rng f by RELAT_1:26;
hence  rng f = Y by XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: FUNCT_2:19
for X, Y being set
for f being Function of X,Y st ( Y = {} implies X = {} ) holds
( f is one-to-one iff for x1, x2 being set st x1 in X & x2 in X & f . x1 = f . x2 holds
x1 = x2 )
proof
let X, Y be set ; ::_thesis: for f being Function of X,Y st ( Y = {} implies X = {} ) holds
( f is one-to-one iff for x1, x2 being set st x1 in X & x2 in X & f . x1 = f . x2 holds
x1 = x2 )
let f be Function of X,Y; ::_thesis: ( ( Y = {} implies X = {} ) implies ( f is one-to-one iff for x1, x2 being set st x1 in X & x2 in X & f . x1 = f . x2 holds
x1 = x2 ) )
assume  ( Y = {} implies X = {} ) ; ::_thesis: ( f is one-to-one iff for x1, x2 being set st x1 in X & x2 in X & f . x1 = f . x2 holds
x1 = x2 )
then  dom f = X by Def1;
hence  ( f is one-to-one iff for x1, x2 being set st x1 in X & x2 in X & f . x1 = f . x2 holds
x1 = x2 ) by FUNCT_1:def_4; ::_thesis: verum
end;

theorem :: FUNCT_2:20
for X, Y, Z being set
for f being Function of X,Y
for g being Function of Y,Z st ( Z = {} implies Y = {} ) & g * f is one-to-one holds
f is one-to-one
proof
let X, Y, Z be set ; ::_thesis: for f being Function of X,Y
for g being Function of Y,Z st ( Z = {} implies Y = {} ) & g * f is one-to-one holds
f is one-to-one
let f be Function of X,Y; ::_thesis: for g being Function of Y,Z st ( Z = {} implies Y = {} ) & g * f is one-to-one holds
f is one-to-one
let g be Function of Y,Z; ::_thesis: ( ( Z = {} implies Y = {} ) & g * f is one-to-one implies f is one-to-one )
assume  ( Z <> {} or Y = {} ) ; ::_thesis: ( not g * f is one-to-one or f is one-to-one )
then A1: Y = dom g by Def1;
 rng f c= Y ;
hence  ( not g * f is one-to-one or f is one-to-one ) by A1, FUNCT_1:25; ::_thesis: verum
end;

theorem :: FUNCT_2:21
for X, Y being set
for f being Function of X,Y st X <> {} & Y <> {} holds
( f is one-to-one iff for Z being set
for g, h being Function of Z,X st f * g = f * h holds
g = h )
proof
let X, Y be set ; ::_thesis: for f being Function of X,Y st X <> {} & Y <> {} holds
( f is one-to-one iff for Z being set
for g, h being Function of Z,X st f * g = f * h holds
g = h )
let f be Function of X,Y; ::_thesis: ( X <> {} & Y <> {} implies ( f is one-to-one iff for Z being set
for g, h being Function of Z,X st f * g = f * h holds
g = h ) )
assume that
A1: X <> {} and
A2: Y <> {} ; ::_thesis: ( f is one-to-one iff for Z being set
for g, h being Function of Z,X st f * g = f * h holds
g = h )
A3: dom f = X by A2, Def1;
thus  ( f is one-to-one implies for Z being set
for g, h being Function of Z,X st f * g = f * h holds
g = h ) ::_thesis: ( ( for Z being set
for g, h being Function of Z,X st f * g = f * h holds
g = h ) implies f is one-to-one )
proof
assume A4: f is one-to-one ; ::_thesis: for Z being set
for g, h being Function of Z,X st f * g = f * h holds
g = h
let Z be set ; ::_thesis: for g, h being Function of Z,X st f * g = f * h holds
g = h
let g, h be Function of Z,X; ::_thesis: ( f * g = f * h implies g = h )
A5: ( rng g c= X & rng h c= X ) ;
 ( dom g = Z & dom h = Z ) by A1, Def1;
hence  ( f * g = f * h implies g = h ) by A3, A4, A5, FUNCT_1:27; ::_thesis: verum
end;
assume A6: for Z being set
for g, h being Function of Z,X st f * g = f * h holds
g = h ; ::_thesis: f is one-to-one
now__::_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  ( rng g c= dom f & rng h c= dom f & dom g = dom h ) ; ::_thesis: ( f * g = f * h implies g = h )
then  ( g is Function of (dom g),X & h is Function of (dom g),X ) by A3, Th2;
hence  ( f * g = f * h implies g = h ) by A6; ::_thesis: verum
end;
hence  f is one-to-one by FUNCT_1:27; ::_thesis: verum
end;

theorem :: FUNCT_2:22
for X, Y, Z being set
for f being Function of X,Y
for g being Function of Y,Z st Z <> {} & rng (g * f) = Z & g is one-to-one holds
rng f = Y
proof
let X, Y, Z be set ; ::_thesis: for f being Function of X,Y
for g being Function of Y,Z st Z <> {} & rng (g * f) = Z & g is one-to-one holds
rng f = Y
let f be Function of X,Y; ::_thesis: for g being Function of Y,Z st Z <> {} & rng (g * f) = Z & g is one-to-one holds
rng f = Y
let g be Function of Y,Z; ::_thesis: ( Z <> {} & rng (g * f) = Z & g is one-to-one implies rng f = Y )
assume that
A1: Z <> {} and
A2: rng (g * f) = Z and
A3: g is one-to-one ; ::_thesis: rng f = Y
A4: dom g = Y by A1, Def1;
 rng (g * f) c= rng g by RELAT_1:26;
then  rng g = rng (g * f) by A2, XBOOLE_0:def_10;
then  Y c= rng f by A3, A4, FUNCT_1:29;
hence  rng f = Y by XBOOLE_0:def_10; ::_thesis: verum
end;

definition
let Y be set ;
let f be Y -valued Relation;
attrf is onto  means :Def3: :: FUNCT_2:def 3
 rng f = Y;
end;

:: deftheorem Def3 defines onto FUNCT_2:def_3_:_
 for Y being set
for f being b1 -valued Relation holds
( f is onto iff rng f = Y );

theorem :: FUNCT_2:23
for X, Y being set
for f being Function of X,Y
for g being Function of Y,X st g * f = id X holds
( f is one-to-one & g is onto )
proof
let X, Y be set ; ::_thesis: for f being Function of X,Y
for g being Function of Y,X st g * f = id X holds
( f is one-to-one & g is onto )
let f be Function of X,Y; ::_thesis: for g being Function of Y,X st g * f = id X holds
( f is one-to-one & g is onto )
let g be Function of Y,X; ::_thesis: ( g * f = id X implies ( f is one-to-one & g is onto ) )
assume A1: g * f = id X ; ::_thesis: ( f is one-to-one & g is onto )
thus  f is one-to-one ::_thesis: g is onto
proof
percases ( Y = {} or Y <> {} ) ;
suppose Y = {} ; ::_thesis: f is one-to-one
hence  f is one-to-one ; ::_thesis: verum
end;
suppose Y <> {} ; ::_thesis: f is one-to-one
then  dom f = X by Def1;
hence  f is one-to-one by A1, FUNCT_1:31; ::_thesis: verum
end;
end;
end;
 rng (g * f) = X by A1, RELAT_1:45;
then  X c= rng g by RELAT_1:26;
hence  rng g = X by XBOOLE_0:def_10; :: according to FUNCT_2:def_3 ::_thesis: verum
end;

theorem :: FUNCT_2:24
for X, Y, Z being set
for f being Function of X,Y
for g being Function of Y,Z st ( Z = {} implies Y = {} ) & g * f is one-to-one & rng f = Y holds
( f is one-to-one & g is one-to-one )
proof
let X, Y, Z be set ; ::_thesis: for f being Function of X,Y
for g being Function of Y,Z st ( Z = {} implies Y = {} ) & g * f is one-to-one & rng f = Y holds
( f is one-to-one & g is one-to-one )
let f be Function of X,Y; ::_thesis: for g being Function of Y,Z st ( Z = {} implies Y = {} ) & g * f is one-to-one & rng f = Y holds
( f is one-to-one & g is one-to-one )
let g be Function of Y,Z; ::_thesis: ( ( Z = {} implies Y = {} ) & g * f is one-to-one & rng f = Y implies ( f is one-to-one & g is one-to-one ) )
assume  ( Z <> {} or Y = {} ) ; ::_thesis: ( not g * f is one-to-one or not rng f = Y or ( f is one-to-one & g is one-to-one ) )
then  Y = dom g by Def1;
hence  ( not g * f is one-to-one or not rng f = Y or ( f is one-to-one & g is one-to-one ) ) by FUNCT_1:26; ::_thesis: verum
end;

theorem Th25: :: FUNCT_2:25
for X, Y being set
for f being Function of X,Y st f is one-to-one & rng f = Y holds
f " is Function of Y,X
proof
let X, Y be set ; ::_thesis: for f being Function of X,Y st f is one-to-one & rng f = Y holds
f " is Function of Y,X
let f be Function of X,Y; ::_thesis: ( f is one-to-one & rng f = Y implies f " is Function of Y,X )
assume that
A1: f is one-to-one and
A2: rng f = Y ; ::_thesis: f " is Function of Y,X
A3: rng (f ") c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (f ") or x in X )
assume  x in rng (f ") ; ::_thesis: x in X
then  x in dom f by A1, FUNCT_1:33;
hence  x in X ; ::_thesis: verum
end;
 dom (f ") = Y by A1, A2, FUNCT_1:33;
then reconsider R = f " as Relation of Y,X by A3, RELSET_1:4;
 R is quasi_total
proof
percases ( X <> {} or X = {} ) ;
:: according to FUNCT_2:def_1
case X <> {} ; ::_thesis: Y = dom R
thus  Y = dom R by A1, A2, FUNCT_1:33; ::_thesis: verum
end;
case X = {} ; ::_thesis: R = {}
then  rng f = {} ;
then  dom (f ") = {} by A1, FUNCT_1:32;
hence  R = {} ; ::_thesis: verum
end;
end;
end;
hence  f " is Function of Y,X ; ::_thesis: verum
end;

theorem :: FUNCT_2:26
for X, Y, x being set
for f being Function of X,Y st Y <> {} & f is one-to-one & x in X holds
(f ") . (f . x) = x
proof
let X, Y, x be set ; ::_thesis: for f being Function of X,Y st Y <> {} & f is one-to-one & x in X holds
(f ") . (f . x) = x
let f be Function of X,Y; ::_thesis: ( Y <> {} & f is one-to-one & x in X implies (f ") . (f . x) = x )
assume  Y <> {} ; ::_thesis: ( not f is one-to-one or not x in X or (f ") . (f . x) = x )
then  dom f = X by Def1;
hence  ( not f is one-to-one or not x in X or (f ") . (f . x) = x ) by FUNCT_1:34; ::_thesis: verum
end;

theorem :: FUNCT_2:27
for X being set
for Y, Z being non empty set
for f being Function of X,Y
for g being Function of Y,Z st f is onto & g is onto holds
g * f is onto
proof
let X be set ; ::_thesis: for Y, Z being non empty set
for f being Function of X,Y
for g being Function of Y,Z st f is onto & g is onto holds
g * f is onto
let Y, Z be non empty set ; ::_thesis: for f being Function of X,Y
for g being Function of Y,Z st f is onto & g is onto holds
g * f is onto
let f be Function of X,Y; ::_thesis: for g being Function of Y,Z st f is onto & g is onto holds
g * f is onto
let g be Function of Y,Z; ::_thesis: ( f is onto & g is onto implies g * f is onto )
assume that
A1: f is onto and
A2: g is onto ; ::_thesis: g * f is onto
rng f = Y by A1, Def3
.= dom g by Def1 ;
then  rng (g * f) = rng g by RELAT_1:28
.= Z by A2, Def3 ;
hence  g * f is onto by Def3; ::_thesis: verum
end;

theorem :: FUNCT_2:28
for X, Y being set
for f being Function of X,Y
for g being Function of Y,X st X <> {} & Y <> {} & rng f = Y & f is one-to-one & ( for y, x being set holds
( y in Y & g . y = x iff ( x in X & f . x = y ) ) ) holds
g = f "
proof
let X, Y be set ; ::_thesis: for f being Function of X,Y
for g being Function of Y,X st X <> {} & Y <> {} & rng f = Y & f is one-to-one & ( for y, x being set holds
( y in Y & g . y = x iff ( x in X & f . x = y ) ) ) holds
g = f "
let f be Function of X,Y; ::_thesis: for g being Function of Y,X st X <> {} & Y <> {} & rng f = Y & f is one-to-one & ( for y, x being set holds
( y in Y & g . y = x iff ( x in X & f . x = y ) ) ) holds
g = f "
let g be Function of Y,X; ::_thesis: ( X <> {} & Y <> {} & rng f = Y & f is one-to-one & ( for y, x being set holds
( y in Y & g . y = x iff ( x in X & f . x = y ) ) ) implies g = f " )
assume  ( X <> {} & Y <> {} ) ; ::_thesis: ( not rng f = Y or not f is one-to-one or ex y, x being set st
( ( y in Y & g . y = x implies ( x in X & f . x = y ) ) implies ( x in X & f . x = y & not ( y in Y & g . y = x ) ) ) or g = f " )
then  ( dom f = X & dom g = Y ) by Def1;
hence  ( not rng f = Y or not f is one-to-one or ex y, x being set st
( ( y in Y & g . y = x implies ( x in X & f . x = y ) ) implies ( x in X & f . x = y & not ( y in Y & g . y = x ) ) ) or g = f " ) by FUNCT_1:32; ::_thesis: verum
end;

theorem :: FUNCT_2:29
for X, Y being set
for f being Function of X,Y st Y <> {} & rng f = Y & f is one-to-one holds
( (f ") * f = id X & f * (f ") = id Y )
proof
let X, Y be set ; ::_thesis: for f being Function of X,Y st Y <> {} & rng f = Y & f is one-to-one holds
( (f ") * f = id X & f * (f ") = id Y )
let f be Function of X,Y; ::_thesis: ( Y <> {} & rng f = Y & f is one-to-one implies ( (f ") * f = id X & f * (f ") = id Y ) )
assume  Y <> {} ; ::_thesis: ( not rng f = Y or not f is one-to-one or ( (f ") * f = id X & f * (f ") = id Y ) )
then  dom f = X by Def1;
hence  ( not rng f = Y or not f is one-to-one or ( (f ") * f = id X & f * (f ") = id Y ) ) by FUNCT_1:39; ::_thesis: verum
end;

theorem :: FUNCT_2:30
for X, Y being set
for f being Function of X,Y
for g being Function of Y,X st X <> {} & Y <> {} & rng f = Y & g * f = id X & f is one-to-one holds
g = f "
proof
let X, Y be set ; ::_thesis: for f being Function of X,Y
for g being Function of Y,X st X <> {} & Y <> {} & rng f = Y & g * f = id X & f is one-to-one holds
g = f "
let f be Function of X,Y; ::_thesis: for g being Function of Y,X st X <> {} & Y <> {} & rng f = Y & g * f = id X & f is one-to-one holds
g = f "
let g be Function of Y,X; ::_thesis: ( X <> {} & Y <> {} & rng f = Y & g * f = id X & f is one-to-one implies g = f " )
assume  ( X <> {} & Y <> {} ) ; ::_thesis: ( not rng f = Y or not g * f = id X or not f is one-to-one or g = f " )
then  ( dom f = X & dom g = Y ) by Def1;
hence  ( not rng f = Y or not g * f = id X or not f is one-to-one or g = f " ) by FUNCT_1:41; ::_thesis: verum
end;

theorem :: FUNCT_2:31
for X, Y being set
for f being Function of X,Y st Y <> {} & ex g being Function of Y,X st g * f = id X holds
f is one-to-one
proof
let X, Y be set ; ::_thesis: for f being Function of X,Y st Y <> {} & ex g being Function of Y,X st g * f = id X holds
f is one-to-one
let f be Function of X,Y; ::_thesis: ( Y <> {} & ex g being Function of Y,X st g * f = id X implies f is one-to-one )
assume  Y <> {} ; ::_thesis: ( for g being Function of Y,X holds not g * f = id X or f is one-to-one )
then A1: dom f = X by Def1;
given g being Function of Y,X such that A2: g * f = id X ; ::_thesis: f is one-to-one
thus  f is one-to-one by A2, A1, FUNCT_1:31; ::_thesis: verum
end;

theorem Th32: :: FUNCT_2:32
for X, Y, Z being set
for f being Function of X,Y st ( Y = {} implies X = {} ) & Z c= X holds
f | Z is Function of Z,Y
proof
let X, Y, Z be set ; ::_thesis: for f being Function of X,Y st ( Y = {} implies X = {} ) & Z c= X holds
f | Z is Function of Z,Y
let f be Function of X,Y; ::_thesis: ( ( Y = {} implies X = {} ) & Z c= X implies f | Z is Function of Z,Y )
assume that
A1: ( Y = {} implies X = {} ) and
A2: Z c= X ; ::_thesis: f | Z is Function of Z,Y
 dom f = X by A1, Def1;
then A3: Z = dom (f | Z) by A2, RELAT_1:62;
 rng (f | Z) c= Y ;
then reconsider R = f | Z as Relation of Z,Y by A3, RELSET_1:4;
 R is quasi_total
proof
percases ( Y <> {} or Y = {} ) ;
:: according to FUNCT_2:def_1
case Y <> {} ; ::_thesis: Z = dom R
 dom f = X by A1, Def1;
hence  Z = dom R by A2, RELAT_1:62; ::_thesis: verum
end;
case Y = {} ; ::_thesis: R = {}
hence  R = {} ; ::_thesis: verum
end;
end;
end;
hence  f | Z is Function of Z,Y ; ::_thesis: verum
end;

theorem :: FUNCT_2:33
for X, Y, Z being set
for f being Function of X,Y st X c= Z holds
f | Z = f by RELSET_1:19;

theorem :: FUNCT_2:34
for X, Y, x, Z being set
for f being Function of X,Y st Y <> {} & x in X & f . x in Z holds
(Z |` f) . x = f . x
proof
let X, Y, x, Z be set ; ::_thesis: for f being Function of X,Y st Y <> {} & x in X & f . x in Z holds
(Z |` f) . x = f . x
let f be Function of X,Y; ::_thesis: ( Y <> {} & x in X & f . x in Z implies (Z |` f) . x = f . x )
assume that
A1: ( Y <> {} & x in X ) and
A2: f . x in Z ; ::_thesis: (Z |` f) . x = f . x
 x in dom f by A1, Def1;
then  x in dom (Z |` f) by A2, FUNCT_1:54;
hence  (Z |` f) . x = f . x by FUNCT_1:55; ::_thesis: verum
end;

theorem :: FUNCT_2:35
for X, Y, P being set
for f being Function of X,Y st Y <> {} holds
for y being set st ex x being set st
( x in X & x in P & y = f . x ) holds
y in f .: P
proof
let X, Y, P be set ; ::_thesis: for f being Function of X,Y st Y <> {} holds
for y being set st ex x being set st
( x in X & x in P & y = f . x ) holds
y in f .: P
let f be Function of X,Y; ::_thesis: ( Y <> {} implies for y being set st ex x being set st
( x in X & x in P & y = f . x ) holds
y in f .: P )
assume  Y <> {} ; ::_thesis: for y being set st ex x being set st
( x in X & x in P & y = f . x ) holds
y in f .: P
then A1: dom f = X by Def1;
let y be set ; ::_thesis: ( ex x being set st
( x in X & x in P & y = f . x ) implies y in f .: P )
given x being set  such that A2: ( x in X & x in P & y = f . x ) ; ::_thesis: y in f .: P
thus  y in f .: P by A1, A2, FUNCT_1:def_6; ::_thesis: verum
end;

theorem :: FUNCT_2:36
for X, Y, P being set
for f being Function of X,Y holds f .: P c= Y ;

theorem :: FUNCT_2:37
canceled;

theorem :: FUNCT_2:38
for X, Y, Q being set
for f being Function of X,Y st Y <> {} holds
for x being set holds
( x in f " Q iff ( x in X & f . x in Q ) )
proof
let X, Y, Q be set ; ::_thesis: for f being Function of X,Y st Y <> {} holds
for x being set holds
( x in f " Q iff ( x in X & f . x in Q ) )
let f be Function of X,Y; ::_thesis: ( Y <> {} implies for x being set holds
( x in f " Q iff ( x in X & f . x in Q ) ) )
assume  Y <> {} ; ::_thesis: for x being set holds
( x in f " Q iff ( x in X & f . x in Q ) )
then  dom f = X by Def1;
hence  for x being set holds
( x in f " Q iff ( x in X & f . x in Q ) ) by FUNCT_1:def_7; ::_thesis: verum
end;

theorem :: FUNCT_2:39
for X, Y, Q being set
for f being PartFunc of X,Y holds f " Q c= X ;

theorem Th40: :: FUNCT_2:40
for X, Y being set
for f being Function of X,Y st ( Y = {} implies X = {} ) holds
f " Y = X
proof
let X, Y be set ; ::_thesis: for f being Function of X,Y st ( Y = {} implies X = {} ) holds
f " Y = X
let f be Function of X,Y; ::_thesis: ( ( Y = {} implies X = {} ) implies f " Y = X )
 (rng f) /\ Y = rng f by XBOOLE_1:28;
then A1: f " Y = f " (rng f) by RELAT_1:133;
assume  ( Y <> {} or X = {} ) ; ::_thesis: f " Y = X
then  dom f = X by Def1;
hence  f " Y = X by A1, RELAT_1:134; ::_thesis: verum
end;

theorem :: FUNCT_2:41
for X, Y being set
for f being Function of X,Y holds
( ( for y being set st y in Y holds
f " {y} <> {} ) iff rng f = Y )
proof
let X, Y be set ; ::_thesis: for f being Function of X,Y holds
( ( for y being set st y in Y holds
f " {y} <> {} ) iff rng f = Y )
let f be Function of X,Y; ::_thesis: ( ( for y being set st y in Y holds
f " {y} <> {} ) iff rng f = Y )
thus  ( ( for y being set st y in Y holds
f " {y} <> {} ) implies rng f = Y ) ::_thesis: ( rng f = Y implies for y being set st y in Y holds
f " {y} <> {} )
proof
assume  for y being set st y in Y holds
f " {y} <> {} ; ::_thesis: rng f = Y
then  Y c= rng f by FUNCT_1:73;
hence  rng f = Y by XBOOLE_0:def_10; ::_thesis: verum
end;
thus  ( rng f = Y implies for y being set st y in Y holds
f " {y} <> {} ) by FUNCT_1:72; ::_thesis: verum
end;

theorem Th42: :: FUNCT_2:42
for X, Y, P being set
for f being Function of X,Y st ( Y = {} implies X = {} ) & P c= X holds
P c= f " (f .: P)
proof
let X, Y, P be set ; ::_thesis: for f being Function of X,Y st ( Y = {} implies X = {} ) & P c= X holds
P c= f " (f .: P)
let f be Function of X,Y; ::_thesis: ( ( Y = {} implies X = {} ) & P c= X implies P c= f " (f .: P) )
assume  ( Y <> {} or X = {} ) ; ::_thesis: ( not P c= X or P c= f " (f .: P) )
then  dom f = X by Def1;
hence  ( not P c= X or P c= f " (f .: P) ) by FUNCT_1:76; ::_thesis: verum
end;

theorem :: FUNCT_2:43
for X, Y being set
for f being Function of X,Y st ( Y = {} implies X = {} ) holds
f " (f .: X) = X
proof
let X, Y be set ; ::_thesis: for f being Function of X,Y st ( Y = {} implies X = {} ) holds
f " (f .: X) = X
let f be Function of X,Y; ::_thesis: ( ( Y = {} implies X = {} ) implies f " (f .: X) = X )
assume  ( Y <> {} or X = {} ) ; ::_thesis: f " (f .: X) = X
then A1: dom f = X by Def1;
then  f " (rng f) = X by RELAT_1:134;
hence  f " (f .: X) = X by A1, RELAT_1:113; ::_thesis: verum
end;

theorem :: FUNCT_2:44
for X, Y, Z, Q being set
for f being Function of X,Y
for g being Function of Y,Z st ( Z = {} implies Y = {} ) holds
f " Q c= (g * f) " (g .: Q)
proof
let X, Y, Z, Q be set ; ::_thesis: for f being Function of X,Y
for g being Function of Y,Z st ( Z = {} implies Y = {} ) holds
f " Q c= (g * f) " (g .: Q)
let f be Function of X,Y; ::_thesis: for g being Function of Y,Z st ( Z = {} implies Y = {} ) holds
f " Q c= (g * f) " (g .: Q)
let g be Function of Y,Z; ::_thesis: ( ( Z = {} implies Y = {} ) implies f " Q c= (g * f) " (g .: Q) )
assume  ( Z <> {} or Y = {} ) ; ::_thesis: f " Q c= (g * f) " (g .: Q)
then A1: dom g = Y by Def1;
 rng f c= Y ;
hence  f " Q c= (g * f) " (g .: Q) by A1, FUNCT_1:90; ::_thesis: verum
end;

theorem :: FUNCT_2:45
for Y, P being set
for f being Function of {},Y holds f .: P = {} ;

theorem :: FUNCT_2:46
for Y, Q being set
for f being Function of {},Y holds f " Q = {} ;

theorem :: FUNCT_2:47
for x, Y being set
for f being Function of {x},Y st Y <> {} holds
f . x in Y
proof
let x, Y be set ; ::_thesis: for f being Function of {x},Y st Y <> {} holds
f . x in Y
let f be Function of {x},Y; ::_thesis: ( Y <> {} implies f . x in Y )
assume  Y <> {} ; ::_thesis: f . x in Y
then A1: dom f = {x} by Def1;
 rng f c= Y ;
then  {(f . x)} c= Y by A1, FUNCT_1:4;
hence  f . x in Y by ZFMISC_1:31; ::_thesis: verum
end;

theorem Th48: :: FUNCT_2:48
for x, Y being set
for f being Function of {x},Y st Y <> {} holds
rng f = {(f . x)}
proof
let x, Y be set ; ::_thesis: for f being Function of {x},Y st Y <> {} holds
rng f = {(f . x)}
let f be Function of {x},Y; ::_thesis: ( Y <> {} implies rng f = {(f . x)} )
assume  Y <> {} ; ::_thesis: rng f = {(f . x)}
then  dom f = {x} by Def1;
hence  rng f = {(f . x)} by FUNCT_1:4; ::_thesis: verum
end;

theorem :: FUNCT_2:49
for x, Y, P being set
for f being Function of {x},Y st Y <> {} holds
f .: P c= {(f . x)}
proof
let x, Y, P be set ; ::_thesis: for f being Function of {x},Y st Y <> {} holds
f .: P c= {(f . x)}
let f be Function of {x},Y; ::_thesis: ( Y <> {} implies f .: P c= {(f . x)} )
 f .: P c= rng f by RELAT_1:111;
hence  ( Y <> {} implies f .: P c= {(f . x)} ) by Th48; ::_thesis: verum
end;

theorem Th50: :: FUNCT_2:50
for X, y, x being set
for f being Function of X,{y} st x in X holds
f . x = y
proof
let X, y, x be set ; ::_thesis: for f being Function of X,{y} st x in X holds
f . x = y
let f be Function of X,{y}; ::_thesis: ( x in X implies f . x = y )
 ( x in X implies f . x in {y} ) by Th5;
hence  ( x in X implies f . x = y ) by TARSKI:def_1; ::_thesis: verum
end;

theorem Th51: :: FUNCT_2:51
for X, y being set
for f1, f2 being Function of X,{y} holds f1 = f2
proof
let X, y be set ; ::_thesis: for f1, f2 being Function of X,{y} holds f1 = f2
let f1, f2 be Function of X,{y}; ::_thesis: f1 = f2
 for x being set st x in X holds
f1 . x = f2 . x
proof
let x be set ; ::_thesis: ( x in X implies f1 . x = f2 . x )
assume A1: x in X ; ::_thesis: f1 . x = f2 . x
then  f1 . x = y by Th50;
hence  f1 . x = f2 . x by A1, Th50; ::_thesis: verum
end;
hence  f1 = f2 by Th12; ::_thesis: verum
end;

theorem Th52: :: FUNCT_2:52
for X being set
for f being Function of X,X holds dom f = X
proof
let X be set ; ::_thesis: for f being Function of X,X holds dom f = X
 ( X = {} implies X = {} ) ;
hence  for f being Function of X,X holds dom f = X by Def1; ::_thesis: verum
end;

registration
let X, Y be set ;
let f be quasi_total PartFunc of X,Y;
let g be quasi_total PartFunc of X,X;
clusterg * f ->  quasi_total for PartFunc of X,Y;
coherence
 for b1 being PartFunc of X,Y st b1 = f * g holds
b1 is quasi_total
proof
percases ( Y = {} or Y <> {} ) ;
suppose Y = {} ; ::_thesis: for b1 being PartFunc of X,Y st b1 = f * g holds
b1 is quasi_total
hence  for b1 being PartFunc of X,Y st b1 = f * g holds
b1 is quasi_total ; ::_thesis: verum
end;
supposeA1: Y <> {} ; ::_thesis: for b1 being PartFunc of X,Y st b1 = f * g holds
b1 is quasi_total
then  dom f = X by Def1;
then  dom (f * g) = g " X by RELAT_1:147
.= dom g by RELSET_1:22
.= X by Th52 ;
hence  for b1 being PartFunc of X,Y st b1 = f * g holds
b1 is quasi_total by A1, Def1; ::_thesis: verum
end;
end;
end;
end;

registration
let X, Y be set ;
let f be quasi_total PartFunc of Y,Y;
let g be quasi_total PartFunc of X,Y;
clusterg * f ->  quasi_total for PartFunc of X,Y;
coherence
 for b1 being PartFunc of X,Y st b1 = f * g holds
b1 is quasi_total
proof
percases ( Y = {} or Y <> {} ) ;
suppose Y = {} ; ::_thesis: for b1 being PartFunc of X,Y st b1 = f * g holds
b1 is quasi_total
hence  for b1 being PartFunc of X,Y st b1 = f * g holds
b1 is quasi_total ; ::_thesis: verum
end;
supposeA1: Y <> {} ; ::_thesis: for b1 being PartFunc of X,Y st b1 = f * g holds
b1 is quasi_total
 dom f = Y by Th52;
then  dom (f * g) = g " Y by RELAT_1:147
.= dom g by RELSET_1:22
.= X by A1, Def1 ;
hence  for b1 being PartFunc of X,Y st b1 = f * g holds
b1 is quasi_total by A1, Def1; ::_thesis: verum
end;
end;
end;
end;

theorem Th53: :: FUNCT_2:53
for X being set
for f, g being Relation of X,X st rng f = X & rng g = X holds
rng (g * f) = X
proof
let X be set ; ::_thesis: for f, g being Relation of X,X st rng f = X & rng g = X holds
rng (g * f) = X
let f, g be Relation of X,X; ::_thesis: ( rng f = X & rng g = X implies rng (g * f) = X )
assume that
A1: rng f = X and
A2: rng g = X ; ::_thesis: rng (g * f) = X
thus  rng (g * f) = f .: X by A2, RELAT_1:127
.= X by A1, RELSET_1:22 ; ::_thesis: verum
end;

theorem :: FUNCT_2:54
for X being set
for f, g being Function of X,X st g * f = f & rng f = X holds
g = id X
proof
let X be set ; ::_thesis: for f, g being Function of X,X st g * f = f & rng f = X holds
g = id X
let f, g be Function of X,X; ::_thesis: ( g * f = f & rng f = X implies g = id X )
 dom g = X by Th52;
hence  ( g * f = f & rng f = X implies g = id X ) by FUNCT_1:23; ::_thesis: verum
end;

theorem :: FUNCT_2:55
for X being set
for f, g being Function of X,X st f * g = f & f is one-to-one holds
g = id X
proof
let X be set ; ::_thesis: for f, g being Function of X,X st f * g = f & f is one-to-one holds
g = id X
let f, g be Function of X,X; ::_thesis: ( f * g = f & f is one-to-one implies g = id X )
A1: rng g c= X ;
 ( dom f = X & dom g = X ) by Th52;
hence  ( f * g = f & f is one-to-one implies g = id X ) by A1, FUNCT_1:28; ::_thesis: verum
end;

theorem Th56: :: FUNCT_2:56
for X being set
for f being Function of X,X holds
( f is one-to-one iff for x1, x2 being set st x1 in X & x2 in X & f . x1 = f . x2 holds
x1 = x2 )
proof
let X be set ; ::_thesis: for f being Function of X,X holds
( f is one-to-one iff for x1, x2 being set st x1 in X & x2 in X & f . x1 = f . x2 holds
x1 = x2 )
let f be Function of X,X; ::_thesis: ( f is one-to-one iff for x1, x2 being set st x1 in X & x2 in X & f . x1 = f . x2 holds
x1 = x2 )
 dom f = X by Th52;
hence  ( f is one-to-one iff for x1, x2 being set st x1 in X & x2 in X & f . x1 = f . x2 holds
x1 = x2 ) by FUNCT_1:def_4; ::_thesis: verum
end;

definition
let X, Y be set ;
let f be X -defined Y -valued Function;
attrf is bijective  means :Def4: :: FUNCT_2:def 4
( f is one-to-one & f is onto );
end;

:: deftheorem Def4 defines bijective FUNCT_2:def_4_:_
 for X, Y being set
for f being b1 -defined b2 -valued Function holds
( f is bijective iff ( f is one-to-one & f is onto ) );

registration
let X, Y be set ;
cluster Function-like bijective  ->  one-to-one onto for Element of bool [:X,Y:];
coherence
 for b1 being PartFunc of X,Y st b1 is bijective holds
( b1 is one-to-one & b1 is onto ) by Def4;
cluster Function-like one-to-one onto  ->  bijective for Element of bool [:X,Y:];
coherence
 for b1 being PartFunc of X,Y st b1 is one-to-one & b1 is onto holds
b1 is bijective by Def4;
end;

registration
let X be set ;
cluster Relation-like X -defined X -valued Function-like total quasi_total bijective for Element of bool [:X,X:];
existence
 ex b1 being Function of X,X st b1 is bijective
proof
take  id X ; ::_thesis: id X is bijective
thus  ( id X is one-to-one & rng (id X) = X ) ; :: according to FUNCT_2:def_3,FUNCT_2:def_4 ::_thesis: verum
end;
end;

definition
let X be set ;
mode Permutation of X is bijective Function of X,X;
end;

theorem Th57: :: FUNCT_2:57
for X being set
for f being Function of X,X st f is one-to-one & rng f = X holds
f is Permutation of X
proof
let X be set ; ::_thesis: for f being Function of X,X st f is one-to-one & rng f = X holds
f is Permutation of X
let f be Function of X,X; ::_thesis: ( f is one-to-one & rng f = X implies f is Permutation of X )
assume that
A1: f is one-to-one and
A2: rng f = X ; ::_thesis: f is Permutation of X
 f is onto by A2, Def3;
hence  f is Permutation of X by A1; ::_thesis: verum
end;

theorem :: FUNCT_2:58
for X being set
for f being Function of X,X st f is one-to-one holds
for x1, x2 being set st x1 in X & x2 in X & f . x1 = f . x2 holds
x1 = x2 by Th56;

registration
let X be set ;
let f, g be onto PartFunc of X,X;
clusterg * f ->  onto for PartFunc of X,X;
coherence
 for b1 being PartFunc of X,X st b1 = f * g holds
b1 is onto
proof
 ( rng f = X & rng g = X ) by Def3;
then  rng (f * g) = X by Th53;
hence  for b1 being PartFunc of X,X st b1 = f * g holds
b1 is onto by Def3; ::_thesis: verum
end;
end;

registration
let X be set ;
let f, g be bijective Function of X,X;
clusterf * g ->  bijective for Function of X,X;
coherence
 for b1 being Function of X,X st b1 = g * f holds
b1 is bijective ;
end;

registration
let X be set ;
cluster reflexive Function-like total quasi_total  ->  bijective for Element of bool [:X,X:];
coherence
 for b1 being Function of X,X st b1 is reflexive & b1 is total holds
b1 is bijective
proof
let f be Function of X,X; ::_thesis: ( f is reflexive & f is total implies f is bijective )
assume A1: ( f is reflexive & f is total ) ; ::_thesis: f is bijective
A3: field f = (dom f) \/ (rng f) by RELAT_1:def_6;
thus  f is one-to-one :: according to FUNCT_2:def_4 ::_thesis: f is onto
proof
let x1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x1 in proj1 f or not b1 in proj1 f or not f . x1 = f . b1 or x1 = b1 )
let x2 be set ; ::_thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume that
A4: x1 in dom f and
A5: x2 in dom f and
A6: f . x1 = f . x2 ; ::_thesis: x1 = x2
 x1 in field f by A3, A4, XBOOLE_0:def_3;
then  [x1,x1] in f by A1, RELAT_2:def_1, RELAT_2:def_9;
then A7: x1 = f . x1 by A4, FUNCT_1:def_2;
 x2 in field f by A3, A5, XBOOLE_0:def_3;
then  [x2,x2] in f by A1, RELAT_2:def_1, RELAT_2:def_9;
hence  x1 = x2 by A5, A6, A7, FUNCT_1:def_2; ::_thesis: verum
end;
thus  rng f c= X ; :: according to XBOOLE_0:def_10,FUNCT_2:def_3 ::_thesis: X c= rng f
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in rng f )
assume  x in X ; ::_thesis: x in rng f
then  x in dom f by PARTFUN1:def_2;
then  x in field f by A3, XBOOLE_0:def_3;
then  [x,x] in f by A1, RELAT_2:def_1, RELAT_2:def_9;
hence  x in rng f by XTUPLE_0:def_13; ::_thesis: verum
end;
end;

definition
let X be set ;
let f be Permutation of X;
:: original: "
redefine funcf "  ->  Permutation of X;
coherence
 f " is Permutation of X
proof
 dom f = X by Th52;
then A1: rng (f ") = X by FUNCT_1:33;
 rng f = X by Def3;
then  f " is Function of X,X by Th25;
hence  f " is Permutation of X by A1, Th57; ::_thesis: verum
end;
end;

theorem :: FUNCT_2:59
for X being set
for f, g being Permutation of X st g * f = g holds
f = id X
proof
let X be set ; ::_thesis: for f, g being Permutation of X st g * f = g holds
f = id X
let f, g be Permutation of X; ::_thesis: ( g * f = g implies f = id X )
A1: rng f c= X ;
 ( dom f = X & dom g = X ) by Th52;
hence  ( g * f = g implies f = id X ) by A1, FUNCT_1:28; ::_thesis: verum
end;

theorem :: FUNCT_2:60
for X being set
for f, g being Permutation of X st g * f = id X holds
g = f "
proof
let X be set ; ::_thesis: for f, g being Permutation of X st g * f = id X holds
g = f "
let f, g be Permutation of X; ::_thesis: ( g * f = id X implies g = f " )
A1: dom f = X by Th52;
 ( rng f = X & dom g = X ) by Def3, Th52;
hence  ( g * f = id X implies g = f " ) by A1, FUNCT_1:41; ::_thesis: verum
end;

theorem :: FUNCT_2:61
for X being set
for f being Permutation of X holds
( (f ") * f = id X & f * (f ") = id X )
proof
let X be set ; ::_thesis: for f being Permutation of X holds
( (f ") * f = id X & f * (f ") = id X )
let f be Permutation of X; ::_thesis: ( (f ") * f = id X & f * (f ") = id X )
 ( dom f = X & rng f = X ) by Def3, Th52;
hence  ( (f ") * f = id X & f * (f ") = id X ) by FUNCT_1:39; ::_thesis: verum
end;

theorem Th62: :: FUNCT_2:62
for X, P being set
for f being Permutation of X st P c= X holds
( f .: (f " P) = P & f " (f .: P) = P )
proof
let X, P be set ; ::_thesis: for f being Permutation of X st P c= X holds
( f .: (f " P) = P & f " (f .: P) = P )
let f be Permutation of X; ::_thesis: ( P c= X implies ( f .: (f " P) = P & f " (f .: P) = P ) )
assume A1: P c= X ; ::_thesis: ( f .: (f " P) = P & f " (f .: P) = P )
 dom f = X by Th52;
then A2: P c= f " (f .: P) by A1, FUNCT_1:76;
 ( f " (f .: P) c= P & rng f = X ) by Def3, FUNCT_1:82;
hence  ( f .: (f " P) = P & f " (f .: P) = P ) by A1, A2, FUNCT_1:77, XBOOLE_0:def_10; ::_thesis: verum
end;

registration
let X be set ;
let D be non empty set ;
let Z be set ;
let f be Function of X,D;
let g be Function of D,Z;
clusterf * g ->  quasi_total for PartFunc of X,Z;
coherence
 for b1 being PartFunc of X,Z st b1 = g * f holds
b1 is quasi_total by Th13;
end;

definition
let C be non empty set ;
let D be set ;
let f be Function of C,D;
let c be Element of C;
:: original: .
redefine funcf . c ->  Element of D;
coherence
 f . c is Element of D
proof
 ( not D is empty or D is empty ) ;
hence  f . c is Element of D by Th5, SUBSET_1:def_1; ::_thesis: verum
end;
end;

scheme :: FUNCT_2:sch 3
FuncExD{ F1() ->  non empty set , F2() ->  non empty set , P1[ set , set ] } :
 ex f being Function of F1(),F2() st
for x being Element of F1() holds P1[x,f . x]
provided
A1: for x being Element of F1() ex y being Element of F2() st P1[x,y]
proof
defpred S1[ set , set ] means ( $1 in F1() & $2 in F2() & P1[$1,$2] );
A2: for x being set st x in F1() holds
ex y being set st
( y in F2() & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in F1() implies ex y being set st
( y in F2() & S1[x,y] ) )
assume A3: x in F1() ; ::_thesis: ex y being set st
( y in F2() & S1[x,y] )
then  ex y being Element of F2() st P1[x,y] by A1;
hence  ex y being set st
( y in F2() & S1[x,y] ) by A3; ::_thesis: verum
end;
consider f being Function of F1(),F2() such that
A4: for x being set st x in F1() holds
S1[x,f . x] from FUNCT_2:sch_1(A2);
take  f ; ::_thesis: for x being Element of F1() holds P1[x,f . x]
let x be Element of F1(); ::_thesis: P1[x,f . x]
thus  P1[x,f . x] by A4; ::_thesis: verum
end;

scheme :: FUNCT_2:sch 4
LambdaD{ F1() ->  non empty set , F2() ->  non empty set , F3( Element of F1()) ->  Element of F2() } :
 ex f being Function of F1(),F2() st
for x being Element of F1() holds f . x = F3(x)
proof
defpred S1[ Element of F1(), set ] means $2 = F3($1);
A1: for x being Element of F1() ex y being Element of F2() st S1[x,y] ;
thus  ex f being Function of F1(),F2() st
for x being Element of F1() holds S1[x,f . x] from FUNCT_2:sch_3(A1); ::_thesis: verum
end;

theorem Th63: :: FUNCT_2:63
for X, Y being set
for f1, f2 being Function of X,Y st ( for x being Element of X holds f1 . x = f2 . x ) holds
f1 = f2
proof
let X, Y be set ; ::_thesis: for f1, f2 being Function of X,Y st ( for x being Element of X holds f1 . x = f2 . x ) holds
f1 = f2
let f1, f2 be Function of X,Y; ::_thesis: ( ( for x being Element of X holds f1 . x = f2 . x ) implies f1 = f2 )
assume  for x being Element of X holds f1 . x = f2 . x ; ::_thesis: f1 = f2
then  for x being set st x in X holds
f1 . x = f2 . x ;
hence  f1 = f2 by Th12; ::_thesis: verum
end;

theorem Th64: :: FUNCT_2:64
for X, Y, P being set
for f being Function of X,Y
for y being set st y in f .: P holds
ex x being set st
( x in X & x in P & y = f . x )
proof
let X, Y, P be set ; ::_thesis: for f being Function of X,Y
for y being set st y in f .: P holds
ex x being set st
( x in X & x in P & y = f . x )
let f be Function of X,Y; ::_thesis: for y being set st y in f .: P holds
ex x being set st
( x in X & x in P & y = f . x )
let y be set ; ::_thesis: ( y in f .: P implies ex x being set st
( x in X & x in P & y = f . x ) )
assume  y in f .: P ; ::_thesis: ex x being set st
( x in X & x in P & y = f . x )
then consider x being set  such that
A1: x in dom f and
A2: ( x in P & y = f . x ) by FUNCT_1:def_6;
take  x ; ::_thesis: ( x in X & x in P & y = f . x )
thus  x in X by A1; ::_thesis: ( x in P & y = f . x )
thus  ( x in P & y = f . x ) by A2; ::_thesis: verum
end;

theorem :: FUNCT_2:65
for X, Y, P being set
for f being Function of X,Y
for y being set st y in f .: P holds
ex c being Element of X st
( c in P & y = f . c )
proof
let X, Y, P be set ; ::_thesis: for f being Function of X,Y
for y being set st y in f .: P holds
ex c being Element of X st
( c in P & y = f . c )
let f be Function of X,Y; ::_thesis: for y being set st y in f .: P holds
ex c being Element of X st
( c in P & y = f . c )
let y be set ; ::_thesis: ( y in f .: P implies ex c being Element of X st
( c in P & y = f . c ) )
assume  y in f .: P ; ::_thesis: ex c being Element of X st
( c in P & y = f . c )
then consider x being set  such that
A1: x in X and
A2: ( x in P & y = f . x ) by Th64;
reconsider c = x as Element of X by A1;
take  c ; ::_thesis: ( c in P & y = f . c )
thus  ( c in P & y = f . c ) by A2; ::_thesis: verum
end;

begin

theorem Th66: :: FUNCT_2:66
for X, Y, f being set st f in Funcs (X,Y) holds
f is Function of X,Y
proof
let X, Y, f be set ; ::_thesis: ( f in Funcs (X,Y) implies f is Function of X,Y )
assume  f in Funcs (X,Y) ; ::_thesis: f is Function of X,Y
then  ( ( not Y = {} or not X <> {} ) & ex f9 being Function st
( f9 = f & dom f9 = X & rng f9 c= Y ) ) by Def2;
hence  f is Function of X,Y by Def1, RELSET_1:4; ::_thesis: verum
end;

scheme :: FUNCT_2:sch 5
Lambda1C{ F1() ->  set , F2() ->  set , P1[ set ], F3( set ) ->  set , F4( set ) ->  set } :
 ex f being Function of F1(),F2() st
for x being set st x in F1() holds
( ( P1[x] implies f . x = F3(x) ) & ( P1[x] implies f . x = F4(x) ) )
provided
A1: for x being set st x in F1() holds
( ( P1[x] implies F3(x) in F2() ) & ( P1[x] implies F4(x) in F2() ) )
proof
A2: now__::_thesis:_(_F2()_=_{}_implies_not_F1()_<>_{}_)
set x = the Element of F1();
assume A3: F2() = {} ; ::_thesis: not F1() <> {}
assume A4: F1() <> {} ; ::_thesis: contradiction
then  ( P1[ the Element of F1()] implies F3( the Element of F1()) in F2() ) by A1;
hence  contradiction by A1, A3, A4; ::_thesis: verum
end;
consider f being Function such that
A5: dom f = F1() and
A6: for x being set st x in F1() holds
( ( P1[x] implies f . x = F3(x) ) & ( P1[x] implies f . x = F4(x) ) ) from PARTFUN1:sch_1();
 rng f c= F2()
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in F2() )
assume  y in rng f ; ::_thesis: y in F2()
then consider x being set  such that
A7: x in dom f and
A8: y = f . x by FUNCT_1:def_3;
A9: ( P1[x] implies f . x = F4(x) ) by A5, A6, A7;
 ( P1[x] implies f . x = F3(x) ) by A5, A6, A7;
hence  y in F2() by A1, A5, A7, A8, A9; ::_thesis: verum
end;
then  f is Function of F1(),F2() by A5, A2, Def1, RELSET_1:4;
hence  ex f being Function of F1(),F2() st
for x being set st x in F1() holds
( ( P1[x] implies f . x = F3(x) ) & ( P1[x] implies f . x = F4(x) ) ) by A6; ::_thesis: verum
end;

theorem :: FUNCT_2:67
for X, Y being set
for f being PartFunc of X,Y st dom f = X holds
f is Function of X,Y
proof
let X, Y be set ; ::_thesis: for f being PartFunc of X,Y st dom f = X holds
f is Function of X,Y
let f be PartFunc of X,Y; ::_thesis: ( dom f = X implies f is Function of X,Y )
 rng f c= Y ;
hence  ( dom f = X implies f is Function of X,Y ) by Th2; ::_thesis: verum
end;

theorem :: FUNCT_2:68
for X, Y being set
for f being PartFunc of X,Y st f is total holds
f is Function of X,Y ;

theorem :: FUNCT_2:69
for X, Y being set
for f being PartFunc of X,Y st ( Y = {} implies X = {} ) & f is Function of X,Y holds
f is total ;

theorem :: FUNCT_2:70
for X, Y being set
for f being Function of X,Y st ( Y = {} implies X = {} ) holds
<:f,X,Y:> is total ;

registration
let X be set ;
let f be Function of X,X;
cluster<:f,X,X:> ->  total ;
coherence
 <:f,X,X:> is total ;
end;

theorem Th71: :: FUNCT_2:71
for X, Y being set
for f being PartFunc of X,Y st ( Y = {} implies X = {} ) holds
ex g being Function of X,Y st
for x being set st x in dom f holds
g . x = f . x
proof
let X, Y be set ; ::_thesis: for f being PartFunc of X,Y st ( Y = {} implies X = {} ) holds
ex g being Function of X,Y st
for x being set st x in dom f holds
g . x = f . x
let f be PartFunc of X,Y; ::_thesis: ( ( Y = {} implies X = {} ) implies ex g being Function of X,Y st
for x being set st x in dom f holds
g . x = f . x )
assume A1: ( Y = {} implies X = {} ) ; ::_thesis: ex g being Function of X,Y st
for x being set st x in dom f holds
g . x = f . x
percases ( Y = {} or Y <> {} ) ;
suppose Y = {} ; ::_thesis: ex g being Function of X,Y st
for x being set st x in dom f holds
g . x = f . x
then reconsider g = f as Function of X,Y by A1;
take  g ; ::_thesis: for x being set st x in dom f holds
g . x = f . x
thus  for x being set st x in dom f holds
g . x = f . x ; ::_thesis: verum
end;
supposeA2: Y <> {} ; ::_thesis: ex g being Function of X,Y st
for x being set st x in dom f holds
g . x = f . x
deffunc H1( set ) ->  set = f . $1;
defpred S1[ set ] means $1 in dom f;
set y = the Element of Y;
deffunc H2( set ) ->  Element of Y = the Element of Y;
A3: for x being set st x in X holds
( ( S1[x] implies H1(x) in Y ) & ( not S1[x] implies H2(x) in Y ) ) by A2, PARTFUN1:4;
consider g being Function of X,Y such that
A4: for x being set st x in X holds
( ( S1[x] implies g . x = H1(x) ) & ( not S1[x] implies g . x = H2(x) ) ) from FUNCT_2:sch_5(A3);
take  g ; ::_thesis: for x being set st x in dom f holds
g . x = f . x
thus  for x being set st x in dom f holds
g . x = f . x by A4; ::_thesis: verum
end;
end;
end;

theorem :: FUNCT_2:72
for X, Y being set holds Funcs (X,Y) c= PFuncs (X,Y)
proof
let X, Y be set ; ::_thesis: Funcs (X,Y) c= PFuncs (X,Y)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Funcs (X,Y) or x in PFuncs (X,Y) )
assume  x in Funcs (X,Y) ; ::_thesis: x in PFuncs (X,Y)
then  ex f being Function st
( x = f & dom f = X & rng f c= Y ) by Def2;
hence  x in PFuncs (X,Y) by PARTFUN1:def_3; ::_thesis: verum
end;

theorem :: FUNCT_2:73
for X, Y being set
for f, g being Function of X,Y st ( Y = {} implies X = {} ) & f tolerates g holds
f = g by PARTFUN1:66;

theorem :: FUNCT_2:74
for X being set
for f, g being Function of X,X st f tolerates g holds
f = g by PARTFUN1:66;

theorem Th75: :: FUNCT_2:75
for X, Y being set
for f being PartFunc of X,Y
for g being Function of X,Y st ( Y = {} implies X = {} ) holds
( f tolerates g iff for x being set st x in dom f holds
f . x = g . x )
proof
let X, Y be set ; ::_thesis: for f being PartFunc of X,Y
for g being Function of X,Y st ( Y = {} implies X = {} ) holds
( f tolerates g iff for x being set st x in dom f holds
f . x = g . x )
let f be PartFunc of X,Y; ::_thesis: for g being Function of X,Y st ( Y = {} implies X = {} ) holds
( f tolerates g iff for x being set st x in dom f holds
f . x = g . x )
let g be Function of X,Y; ::_thesis: ( ( Y = {} implies X = {} ) implies ( f tolerates g iff for x being set st x in dom f holds
f . x = g . x ) )
assume  ( Y = {} implies X = {} ) ; ::_thesis: ( f tolerates g iff for x being set st x in dom f holds
f . x = g . x )
then  dom g = X by Def1;
hence  ( f tolerates g iff for x being set st x in dom f holds
f . x = g . x ) by PARTFUN1:53; ::_thesis: verum
end;

theorem :: FUNCT_2:76
for X being set
for f being PartFunc of X,X
for g being Function of X,X holds
( f tolerates g iff for x being set st x in dom f holds
f . x = g . x )
proof
let X be set ; ::_thesis: for f being PartFunc of X,X
for g being Function of X,X holds
( f tolerates g iff for x being set st x in dom f holds
f . x = g . x )
let f be PartFunc of X,X; ::_thesis: for g being Function of X,X holds
( f tolerates g iff for x being set st x in dom f holds
f . x = g . x )
let g be Function of X,X; ::_thesis: ( f tolerates g iff for x being set st x in dom f holds
f . x = g . x )
 ( X = {} implies X = {} ) ;
hence  ( f tolerates g iff for x being set st x in dom f holds
f . x = g . x ) by Th75; ::_thesis: verum
end;

theorem Th77: :: FUNCT_2:77
for X, Y being set
for f being PartFunc of X,Y st ( Y = {} implies X = {} ) holds
ex g being Function of X,Y st f tolerates g
proof
let X, Y be set ; ::_thesis: for f being PartFunc of X,Y st ( Y = {} implies X = {} ) holds
ex g being Function of X,Y st f tolerates g
let f be PartFunc of X,Y; ::_thesis: ( ( Y = {} implies X = {} ) implies ex g being Function of X,Y st f tolerates g )
assume A1: ( Y = {} implies X = {} ) ; ::_thesis: ex g being Function of X,Y st f tolerates g
then consider g being Function of X,Y such that
A2: for x being set st x in dom f holds
g . x = f . x by Th71;
take  g ; ::_thesis: f tolerates g
thus  f tolerates g by A1, A2, Th75; ::_thesis: verum
end;

theorem :: FUNCT_2:78
for X being set
for f, g being PartFunc of X,X
for h being Function of X,X st f tolerates h & g tolerates h holds
f tolerates g by PARTFUN1:67;

theorem :: FUNCT_2:79
for X, Y being set
for f, g being PartFunc of X,Y st ( Y = {} implies X = {} ) & f tolerates g holds
ex h being Function of X,Y st
( f tolerates h & g tolerates h )
proof
let X, Y be set ; ::_thesis: for f, g being PartFunc of X,Y st ( Y = {} implies X = {} ) & f tolerates g holds
ex h being Function of X,Y st
( f tolerates h & g tolerates h )
let f, g be PartFunc of X,Y; ::_thesis: ( ( Y = {} implies X = {} ) & f tolerates g implies ex h being Function of X,Y st
( f tolerates h & g tolerates h ) )
assume  ( ( Y = {} implies X = {} ) & f tolerates g ) ; ::_thesis: ex h being Function of X,Y st
( f tolerates h & g tolerates h )
then  ex h being PartFunc of X,Y st
( h is total & f tolerates h & g tolerates h ) by PARTFUN1:68;
hence  ex h being Function of X,Y st
( f tolerates h & g tolerates h ) ; ::_thesis: verum
end;

theorem :: FUNCT_2:80
for X, Y being set
for f being PartFunc of X,Y
for g being Function of X,Y st ( Y = {} implies X = {} ) & f tolerates g holds
g in TotFuncs f by PARTFUN1:def_5;

theorem :: FUNCT_2:81
for X being set
for f being PartFunc of X,X
for g being Function of X,X st f tolerates g holds
g in TotFuncs f by PARTFUN1:def_5;

theorem Th82: :: FUNCT_2:82
for X, Y being set
for f being PartFunc of X,Y
for g being set st g in TotFuncs f holds
g is Function of X,Y
proof
let X, Y be set ; ::_thesis: for f being PartFunc of X,Y
for g being set st g in TotFuncs f holds
g is Function of X,Y
let f be PartFunc of X,Y; ::_thesis: for g being set st g in TotFuncs f holds
g is Function of X,Y
let g be set ; ::_thesis: ( g in TotFuncs f implies g is Function of X,Y )
assume  g in TotFuncs f ; ::_thesis: g is Function of X,Y
then  ex g9 being PartFunc of X,Y st
( g9 = g & g9 is total & f tolerates g9 ) by PARTFUN1:def_5;
hence  g is Function of X,Y ; ::_thesis: verum
end;

theorem :: FUNCT_2:83
for X, Y being set
for f being PartFunc of X,Y holds TotFuncs f c= Funcs (X,Y)
proof
let X, Y be set ; ::_thesis: for f being PartFunc of X,Y holds TotFuncs f c= Funcs (X,Y)
let f be PartFunc of X,Y; ::_thesis: TotFuncs f c= Funcs (X,Y)
percases ( ( Y = {} & X <> {} ) or Y <> {} or X = {} ) ;
suppose ( Y = {} & X <> {} ) ; ::_thesis: TotFuncs f c= Funcs (X,Y)
hence  TotFuncs f c= Funcs (X,Y) ; ::_thesis: verum
end;
supposeA1: ( Y <> {} or X = {} ) ; ::_thesis: TotFuncs f c= Funcs (X,Y)
let g be set ; :: according to TARSKI:def_3 ::_thesis: ( not g in TotFuncs f or g in Funcs (X,Y) )
assume  g in TotFuncs f ; ::_thesis: g in Funcs (X,Y)
then  g is Function of X,Y by Th82;
hence  g in Funcs (X,Y) by A1, Th8; ::_thesis: verum
end;
end;
end;

theorem :: FUNCT_2:84
for X, Y being set holds TotFuncs <:{},X,Y:> = Funcs (X,Y)
proof
let X, Y be set ; ::_thesis: TotFuncs <:{},X,Y:> = Funcs (X,Y)
percases not ( not ( Y = {} & X <> {} ) & Y = {} & not X = {} ) ;
supposeA1: ( Y = {} & X <> {} ) ; ::_thesis: TotFuncs <:{},X,Y:> = Funcs (X,Y)
then  TotFuncs <:{},X,Y:> = {} ;
hence  TotFuncs <:{},X,Y:> = Funcs (X,Y) by A1; ::_thesis: verum
end;
supposeA2: ( Y = {} implies X = {} ) ; ::_thesis: TotFuncs <:{},X,Y:> = Funcs (X,Y)
 for g being set holds
( g in TotFuncs <:{},X,Y:> iff g in Funcs (X,Y) )
proof
let g be set ; ::_thesis: ( g in TotFuncs <:{},X,Y:> iff g in Funcs (X,Y) )
thus  ( g in TotFuncs <:{},X,Y:> implies g in Funcs (X,Y) ) ::_thesis: ( g in Funcs (X,Y) implies g in TotFuncs <:{},X,Y:> )
proof
assume  g in TotFuncs <:{},X,Y:> ; ::_thesis: g in Funcs (X,Y)
then  g is Function of X,Y by Th82;
hence  g in Funcs (X,Y) by A2, Th8; ::_thesis: verum
end;
assume A3: g in Funcs (X,Y) ; ::_thesis: g in TotFuncs <:{},X,Y:>
then reconsider g9 = g as PartFunc of X,Y by Th66;
A4: <:{},X,Y:> tolerates g9 by PARTFUN1:60;
 g is Function of X,Y by A3, Th66;
hence  g in TotFuncs <:{},X,Y:> by A2, A4, PARTFUN1:def_5; ::_thesis: verum
end;
hence  TotFuncs <:{},X,Y:> = Funcs (X,Y) by TARSKI:1; ::_thesis: verum
end;
end;
end;

theorem :: FUNCT_2:85
for X, Y being set
for f being Function of X,Y st ( Y = {} implies X = {} ) holds
TotFuncs <:f,X,Y:> = {f} by PARTFUN1:72;

theorem :: FUNCT_2:86
for X being set
for f being Function of X,X holds TotFuncs <:f,X,X:> = {f} by PARTFUN1:72;

theorem :: FUNCT_2:87
for X, y being set
for f being PartFunc of X,{y}
for g being Function of X,{y} holds TotFuncs f = {g}
proof
let X, y be set ; ::_thesis: for f being PartFunc of X,{y}
for g being Function of X,{y} holds TotFuncs f = {g}
let f be PartFunc of X,{y}; ::_thesis: for g being Function of X,{y} holds TotFuncs f = {g}
let g be Function of X,{y}; ::_thesis: TotFuncs f = {g}
 for h being set holds
( h in TotFuncs f iff h = g )
proof
let h be set ; ::_thesis: ( h in TotFuncs f iff h = g )
thus  ( h in TotFuncs f implies h = g ) ::_thesis: ( h = g implies h in TotFuncs f )
proof
assume  h in TotFuncs f ; ::_thesis: h = g
then  h is Function of X,{y} by Th82;
hence  h = g by Th51; ::_thesis: verum
end;
 f tolerates g by PARTFUN1:61;
hence  ( h = g implies h in TotFuncs f ) by PARTFUN1:def_5; ::_thesis: verum
end;
hence  TotFuncs f = {g} by TARSKI:def_1; ::_thesis: verum
end;

theorem :: FUNCT_2:88
for X, Y being set
for f, g being PartFunc of X,Y st g c= f holds
TotFuncs f c= TotFuncs g
proof
let X, Y be set ; ::_thesis: for f, g being PartFunc of X,Y st g c= f holds
TotFuncs f c= TotFuncs g
let f, g be PartFunc of X,Y; ::_thesis: ( g c= f implies TotFuncs f c= TotFuncs g )
assume A1: g c= f ; ::_thesis: TotFuncs f c= TotFuncs g
let h be set ; :: according to TARSKI:def_3 ::_thesis: ( not h in TotFuncs f or h in TotFuncs g )
assume A2: h in TotFuncs f ; ::_thesis: h in TotFuncs g
then reconsider h9 = h as PartFunc of X,Y by PARTFUN1:69;
A3: h9 is total by A2, PARTFUN1:70;
 g tolerates h9 by A1, A2, PARTFUN1:58, PARTFUN1:71;
hence  h in TotFuncs g by A3, PARTFUN1:def_5; ::_thesis: verum
end;

theorem Th89: :: FUNCT_2:89
for X, Y being set
for f, g being PartFunc of X,Y st dom g c= dom f & TotFuncs f c= TotFuncs g holds
g c= f
proof
let X, Y be set ; ::_thesis: for f, g being PartFunc of X,Y st dom g c= dom f & TotFuncs f c= TotFuncs g holds
g c= f
let f, g be PartFunc of X,Y; ::_thesis: ( dom g c= dom f & TotFuncs f c= TotFuncs g implies g c= f )
assume A1: dom g c= dom f ; ::_thesis: ( not TotFuncs f c= TotFuncs g or g c= f )
now__::_thesis:_(_not_TotFuncs_f_c=_TotFuncs_g_or_g_c=_f_)
percases not ( not ( Y = {} & X <> {} ) & Y = {} & not X = {} ) ;
suppose ( Y = {} & X <> {} ) ; ::_thesis: ( not TotFuncs f c= TotFuncs g or g c= f )
hence  ( not TotFuncs f c= TotFuncs g or g c= f ) ; ::_thesis: verum
end;
supposeA2: ( Y = {} implies X = {} ) ; ::_thesis: ( TotFuncs f c= TotFuncs g implies g c= f )
thus  ( TotFuncs f c= TotFuncs g implies g c= f ) ::_thesis: verum
proof
assume A3: TotFuncs f c= TotFuncs g ; ::_thesis: g c= f
 for x being set st x in dom g holds
g . x = f . x
proof
let x be set ; ::_thesis: ( x in dom g implies g . x = f . x )
consider h being Function of X,Y such that
A4: f tolerates h by A2, Th77;
 h in TotFuncs f by A2, A4, PARTFUN1:def_5;
then B5: g tolerates h by A3, PARTFUN1:71;
assume  x in dom g ; ::_thesis: g . x = f . x
then  x in (dom f) /\ (dom g) by A1, XBOOLE_0:def_4;
hence  g . x = f . x by B5, PARTFUN1:def_4, A2, A4, PARTFUN1:67; ::_thesis: verum
end;
hence  g c= f by A1, GRFUNC_1:2; ::_thesis: verum
end;
end;
end;
end;
hence  ( not TotFuncs f c= TotFuncs g or g c= f ) ; ::_thesis: verum
end;

theorem Th90: :: FUNCT_2:90
for X, Y being set
for f, g being PartFunc of X,Y st TotFuncs f c= TotFuncs g & ( for y being set holds Y <> {y} ) holds
g c= f
proof
let X, Y be set ; ::_thesis: for f, g being PartFunc of X,Y st TotFuncs f c= TotFuncs g & ( for y being set holds Y <> {y} ) holds
g c= f
let f, g be PartFunc of X,Y; ::_thesis: ( TotFuncs f c= TotFuncs g & ( for y being set holds Y <> {y} ) implies g c= f )
assume that
A1: TotFuncs f c= TotFuncs g and
A2: for y being set holds Y <> {y} ; ::_thesis: g c= f
now__::_thesis:_dom_g_c=_dom_f
percases ( Y = {} or Y <> {} ) ;
suppose Y = {} ; ::_thesis: dom g c= dom f
hence  dom g c= dom f ; ::_thesis: verum
end;
supposeA3: Y <> {} ; ::_thesis: dom g c= dom f
thus  dom g c= dom f ::_thesis: verum
proof
deffunc H1( set ) ->  set = f . $1;
defpred S1[ set ] means $1 in dom f;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom g or x in dom f )
assume that
A4: x in dom g and
A5: not x in dom f ; ::_thesis: contradiction
A6: Y <> {(g . x)} by A2;
 g . x in Y by A4, PARTFUN1:4;
then consider y being set  such that
A7: y in Y and
A8: y <> g . x by A6, ZFMISC_1:35;
deffunc H2( set ) ->  set = y;
A9: for x9 being set st x9 in X holds
( ( S1[x9] implies H1(x9) in Y ) & ( not S1[x9] implies H2(x9) in Y ) ) by A7, PARTFUN1:4;
consider h being Function of X,Y such that
A10: for x9 being set st x9 in X holds
( ( S1[x9] implies h . x9 = H1(x9) ) & ( not S1[x9] implies h . x9 = H2(x9) ) ) from FUNCT_2:sch_5(A9);
 f tolerates h
proof
let x9 be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not x9 in (proj1 f) /\ (proj1 h) or f . x9 = h . x9 )
assume  x9 in (dom f) /\ (dom h) ; ::_thesis: f . x9 = h . x9
then  x9 in dom f by XBOOLE_0:def_4;
hence  f . x9 = h . x9 by A10; ::_thesis: verum
end;
then B11: h in TotFuncs f by A3, PARTFUN1:def_5;
 x in X by A4;
then  x in dom h by A3, Def1;
then A12: x in (dom g) /\ (dom h) by A4, XBOOLE_0:def_4;
 h . x = y by A4, A5, A10;
hence  contradiction by A8, B11, A12, PARTFUN1:def_4, A1, PARTFUN1:71; ::_thesis: verum
end;
end;
end;
end;
hence  g c= f by A1, Th89; ::_thesis: verum
end;

theorem :: FUNCT_2:91
for X, Y being set
for f, g being PartFunc of X,Y st ( for y being set holds Y <> {y} ) & TotFuncs f = TotFuncs g holds
f = g
proof
let X, Y be set ; ::_thesis: for f, g being PartFunc of X,Y st ( for y being set holds Y <> {y} ) & TotFuncs f = TotFuncs g holds
f = g
let f, g be PartFunc of X,Y; ::_thesis: ( ( for y being set holds Y <> {y} ) & TotFuncs f = TotFuncs g implies f = g )
assume A1: for y being set holds Y <> {y} ; ::_thesis: ( not TotFuncs f = TotFuncs g or f = g )
assume  TotFuncs f = TotFuncs g ; ::_thesis: f = g
then  ( g c= f & f c= g ) by A1, Th90;
hence  f = g by XBOOLE_0:def_10; ::_thesis: verum
end;

registration
let A, B be non empty set ;
cluster Function-like quasi_total  ->  non empty for Element of bool [:A,B:];
coherence
 for b1 being Function of A,B holds not b1 is empty by Def1, RELAT_1:38;
end;

begin

scheme :: FUNCT_2:sch 6
LambdaSep1{ F1() ->  non empty set , F2() ->  non empty set , F3() ->  Element of F1(), F4() ->  Element of F2(), F5( set ) ->  Element of F2() } :
 ex f being Function of F1(),F2() st
( f . F3() = F4() & ( for x being Element of F1() st x <> F3() holds
f . x = F5(x) ) )
proof
defpred S1[ set , set ] means ( ( $1 = F3() implies $2 = F4() ) & ( $1 <> F3() implies $2 = F5($1) ) );
A1: for x being Element of F1() ex y being Element of F2() st S1[x,y]
proof
let x be Element of F1(); ::_thesis: ex y being Element of F2() st S1[x,y]
 ( x = F3() implies ex y being Element of F2() st S1[x,y] ) ;
hence  ex y being Element of F2() st S1[x,y] ; ::_thesis: verum
end;
consider f being Function of F1(),F2() such that
A2: for x being Element of F1() holds S1[x,f . x] from FUNCT_2:sch_3(A1);
take  f ; ::_thesis: ( f . F3() = F4() & ( for x being Element of F1() st x <> F3() holds
f . x = F5(x) ) )
thus  ( f . F3() = F4() & ( for x being Element of F1() st x <> F3() holds
f . x = F5(x) ) ) by A2; ::_thesis: verum
end;

scheme :: FUNCT_2:sch 7
LambdaSep2{ F1() ->  non empty set , F2() ->  non empty set , F3() ->  Element of F1(), F4() ->  Element of F1(), F5() ->  Element of F2(), F6() ->  Element of F2(), F7( set ) ->  Element of F2() } :
 ex f being Function of F1(),F2() st
( f . F3() = F5() & f . F4() = F6() & ( for x being Element of F1() st x <> F3() & x <> F4() holds
f . x = F7(x) ) )
provided
A1: F3() <> F4()
proof
defpred S1[ set , set ] means ( ( $1 = F3() implies $2 = F5() ) & ( $1 = F4() implies $2 = F6() ) & ( $1 <> F3() & $1 <> F4() implies $2 = F7($1) ) );
A2: for x being Element of F1() ex y being Element of F2() st S1[x,y]
proof
let x be Element of F1(); ::_thesis: ex y being Element of F2() st S1[x,y]
A3: ( x = F4() implies ex y being Element of F2() st S1[x,y] ) by A1;
 ( x = F3() implies ex y being Element of F2() st S1[x,y] ) by A1;
hence  ex y being Element of F2() st S1[x,y] by A3; ::_thesis: verum
end;
consider f being Function of F1(),F2() such that
A4: for x being Element of F1() holds S1[x,f . x] from FUNCT_2:sch_3(A2);
take  f ; ::_thesis: ( f . F3() = F5() & f . F4() = F6() & ( for x being Element of F1() st x <> F3() & x <> F4() holds
f . x = F7(x) ) )
thus  ( f . F3() = F5() & f . F4() = F6() & ( for x being Element of F1() st x <> F3() & x <> F4() holds
f . x = F7(x) ) ) by A4; ::_thesis: verum
end;

theorem :: FUNCT_2:92
for A, B being set
for f being Function st f in Funcs (A,B) holds
( dom f = A & rng f c= B )
proof
let A, B be set ; ::_thesis: for f being Function st f in Funcs (A,B) holds
( dom f = A & rng f c= B )
let f be Function; ::_thesis: ( f in Funcs (A,B) implies ( dom f = A & rng f c= B ) )
assume  f in Funcs (A,B) ; ::_thesis: ( dom f = A & rng f c= B )
then  ex g being Function st
( f = g & dom g = A & rng g c= B ) by Def2;
hence  ( dom f = A & rng f c= B ) ; ::_thesis: verum
end;

scheme :: FUNCT_2:sch 8
FunctRealEx{ F1() ->  non empty set , F2() ->  set , F3( set ) ->  set } :
 ex f being Function of F1(),F2() st
for x being Element of F1() holds f . x = F3(x)
provided
A1: for x being Element of F1() holds F3(x) in F2()
proof
defpred S1[ set , set ] means $2 = F3($1);
A2: for x being set st x in F1() holds
ex y being set st
( y in F2() & S1[x,y] ) by A1;
 ex f being Function of F1(),F2() st
for x being set st x in F1() holds
S1[x,f . x] from FUNCT_2:sch_1(A2);
then consider f being Function of F1(),F2() such that
A3: for x being set st x in F1() holds
f . x = F3(x) ;
 for x being Element of F1() holds f . x = F3(x) by A3;
hence  ex f being Function of F1(),F2() st
for x being Element of F1() holds f . x = F3(x) ; ::_thesis: verum
end;

scheme :: FUNCT_2:sch 9
KappaMD{ F1() ->  non empty set , F2() ->  non empty set , F3( set ) ->  set } :
 ex f being Function of F1(),F2() st
for x being Element of F1() holds f . x = F3(x)
provided
A1: for x being Element of F1() holds F3(x) is Element of F2()
proof
A2: now__::_thesis:_for_x_being_Element_of_F1()_holds_F3(x)_in_F2()
let x be Element of F1(); ::_thesis: F3(x) in F2()
 F3(x) is Element of F2() by A1;
hence  F3(x) in F2() ; ::_thesis: verum
end;
consider f being Function of F1(),F2() such that
A3: for x being Element of F1() holds f . x = F3(x) from FUNCT_2:sch_8(A2);
take  f ; ::_thesis: for x being Element of F1() holds f . x = F3(x)
thus  for x being Element of F1() holds f . x = F3(x) by A3; ::_thesis: verum
end;

definition
let A, B, C be non empty set ;
let f be Function of A,[:B,C:];
:: original: pr1
redefine func pr1 f ->  Function of A,B means :Def5: :: FUNCT_2:def 5
 for x being Element of A holds it . x = (f . x) `1 ;
coherence
 pr1 f is Function of A,B
proof
A1: dom (pr1 f) = dom f by MCART_1:def_12;
A2: rng (pr1 f) c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (pr1 f) or x in B )
assume  x in rng (pr1 f) ; ::_thesis: x in B
then consider y being set  such that
A3: ( y in dom (pr1 f) & x = (pr1 f) . y ) by FUNCT_1:def_3;
 ( x = (f . y) `1 & f . y in [:B,C:] ) by A1, A3, Th5, MCART_1:def_12;
hence  x in B by MCART_1:10; ::_thesis: verum
end;
 dom (pr1 f) = A by A1, Def1;
hence  pr1 f is Function of A,B by A2, Th2; ::_thesis: verum
end;
compatibility
 for b1 being Function of A,B holds
( b1 = pr1 f iff for x being Element of A holds b1 . x = (f . x) `1 )
proof
let IT be Function of A,B; ::_thesis: ( IT = pr1 f iff for x being Element of A holds IT . x = (f . x) `1 )
A4: dom (pr1 f) = dom f by MCART_1:def_12;
then A5: dom (pr1 f) = A by Def1;
hence  ( IT = pr1 f implies for x being Element of A holds IT . x = (f . x) `1 ) by A4, MCART_1:def_12; ::_thesis: ( ( for x being Element of A holds IT . x = (f . x) `1 ) implies IT = pr1 f )
assume  for x being Element of A holds IT . x = (f . x) `1 ; ::_thesis: IT = pr1 f
then A6: for x being set st x in dom f holds
IT . x = (f . x) `1 ;
 dom IT = dom f by A4, A5, Def1;
hence  IT = pr1 f by A6, MCART_1:def_12; ::_thesis: verum
end;
:: original: pr2
redefine func pr2 f ->  Function of A,C means :Def6: :: FUNCT_2:def 6
 for x being Element of A holds it . x = (f . x) `2 ;
coherence
 pr2 f is Function of A,C
proof
A7: dom (pr2 f) = dom f by MCART_1:def_13;
A8: rng (pr2 f) c= C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (pr2 f) or x in C )
assume  x in rng (pr2 f) ; ::_thesis: x in C
then consider y being set  such that
A9: ( y in dom (pr2 f) & x = (pr2 f) . y ) by FUNCT_1:def_3;
 ( x = (f . y) `2 & f . y in [:B,C:] ) by A7, A9, Th5, MCART_1:def_13;
hence  x in C by MCART_1:10; ::_thesis: verum
end;
 dom (pr2 f) = A by A7, Def1;
hence  pr2 f is Function of A,C by A8, Th2; ::_thesis: verum
end;
compatibility
 for b1 being Function of A,C holds
( b1 = pr2 f iff for x being Element of A holds b1 . x = (f . x) `2 )
proof
let IT be Function of A,C; ::_thesis: ( IT = pr2 f iff for x being Element of A holds IT . x = (f . x) `2 )
A10: dom (pr2 f) = dom f by MCART_1:def_13;
then A11: dom (pr2 f) = A by Def1;
hence  ( IT = pr2 f implies for x being Element of A holds IT . x = (f . x) `2 ) by A10, MCART_1:def_13; ::_thesis: ( ( for x being Element of A holds IT . x = (f . x) `2 ) implies IT = pr2 f )
assume  for x being Element of A holds IT . x = (f . x) `2 ; ::_thesis: IT = pr2 f
then A12: for x being set st x in dom f holds
IT . x = (f . x) `2 ;
 dom IT = dom f by A10, A11, Def1;
hence  IT = pr2 f by A12, MCART_1:def_13; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines pr1 FUNCT_2:def_5_:_
 for A, B, C being non empty set
for f being Function of A,[:B,C:]
for b5 being Function of A,B holds
( b5 = pr1 f iff for x being Element of A holds b5 . x = (f . x) `1 );

:: deftheorem Def6 defines pr2 FUNCT_2:def_6_:_
 for A, B, C being non empty set
for f being Function of A,[:B,C:]
for b5 being Function of A,C holds
( b5 = pr2 f iff for x being Element of A holds b5 . x = (f . x) `2 );

definition
let A1 be set ;
let B1 be non empty set ;
let A2 be set ;
let B2 be non empty set ;
let f1 be Function of A1,B1;
let f2 be Function of A2,B2;
:: original: =
redefine predf1 = f2 means :: FUNCT_2:def 7
( A1 = A2 & ( for a being Element of A1 holds f1 . a = f2 . a ) );
compatibility
 ( f1 = f2 iff ( A1 = A2 & ( for a being Element of A1 holds f1 . a = f2 . a ) ) )
proof
A1: dom f1 = A1 by Def1;
hence  ( f1 = f2 implies ( A1 = A2 & ( for a being Element of A1 holds f1 . a = f2 . a ) ) ) by Def1; ::_thesis: ( A1 = A2 & ( for a being Element of A1 holds f1 . a = f2 . a ) implies f1 = f2 )
assume that
A2: A1 = A2 and
A3: for a being Element of A1 holds f1 . a = f2 . a ; ::_thesis: f1 = f2
A4: dom f2 = A2 by Def1;
 for a being set st a in A1 holds
f1 . a = f2 . a by A3;
hence  f1 = f2 by A1, A4, A2, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem  defines = FUNCT_2:def_7_:_
 for A1 being set
for B1 being non empty set
for A2 being set
for B2 being non empty set
for f1 being Function of A1,B1
for f2 being Function of A2,B2 holds
( f1 = f2 iff ( A1 = A2 & ( for a being Element of A1 holds f1 . a = f2 . a ) ) );

definition
let A, B be set ;
let f1, f2 be Function of A,B;
:: original: =
redefine predf1 = f2 means :: FUNCT_2:def 8
 for a being Element of A holds f1 . a = f2 . a;
compatibility
 ( f1 = f2 iff for a being Element of A holds f1 . a = f2 . a ) by Th63;
end;

:: deftheorem  defines = FUNCT_2:def_8_:_
 for A, B being set
for f1, f2 being Function of A,B holds
( f1 = f2 iff for a being Element of A holds f1 . a = f2 . a );

theorem :: FUNCT_2:93
for N being set
for f being Function of N,(bool N) ex R being Relation of N st
for i being set st i in N holds
Im (R,i) = f . i
proof
let N be set ; ::_thesis: for f being Function of N,(bool N) ex R being Relation of N st
for i being set st i in N holds
Im (R,i) = f . i
let f be Function of N,(bool N); ::_thesis: ex R being Relation of N st
for i being set st i in N holds
Im (R,i) = f . i
deffunc H1( set ) ->  set = f . $1;
A1: for i being Element of N st i in [#] N holds
H1(i) c= [#] N
proof
let i be Element of N; ::_thesis: ( i in [#] N implies H1(i) c= [#] N )
assume  i in [#] N ; ::_thesis: H1(i) c= [#] N
then  f . i in bool N by Th5;
hence  H1(i) c= [#] N ; ::_thesis: verum
end;
consider R being Relation of ([#] N) such that
A2: for i being Element of N st i in [#] N holds
Im (R,i) = H1(i) from RELSET_1:sch_3(A1);
reconsider R = R as Relation of N ;
take  R ; ::_thesis: for i being set st i in N holds
Im (R,i) = f . i
thus  for i being set st i in N holds
Im (R,i) = f . i by A2; ::_thesis: verum
end;

theorem Th94: :: FUNCT_2:94
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
thus A = (id X) " ((id X) .: A) by Th62
.= (id X) " A by FUNCT_1:92 ; ::_thesis: verum
end;


theorem :: FUNCT_2:95
for A, B being non empty set
for f being Function of A,B
for A0 being Subset of A
for B0 being Subset of B holds
( f .: A0 c= B0 iff A0 c= f " B0 )
proof
let A, B be non empty set ; ::_thesis: for f being Function of A,B
for A0 being Subset of A
for B0 being Subset of B holds
( f .: A0 c= B0 iff A0 c= f " B0 )
let f be Function of A,B; ::_thesis: for A0 being Subset of A
for B0 being Subset of B holds
( f .: A0 c= B0 iff A0 c= f " B0 )
let A0 be Subset of A; ::_thesis: for B0 being Subset of B holds
( f .: A0 c= B0 iff A0 c= f " B0 )
let B0 be Subset of B; ::_thesis: ( f .: A0 c= B0 iff A0 c= f " B0 )
thus  ( f .: A0 c= B0 implies A0 c= f " B0 ) ::_thesis: ( A0 c= f " B0 implies f .: A0 c= B0 )
proof
assume  f .: A0 c= B0 ; ::_thesis: A0 c= f " B0
then A1: f " (f .: A0) c= f " B0 by RELAT_1:143;
 A0 c= f " (f .: A0) by Th42;
hence  A0 c= f " B0 by A1, XBOOLE_1:1; ::_thesis: verum
end;
thus  ( A0 c= f " B0 implies f .: A0 c= B0 ) ::_thesis: verum
proof
assume  A0 c= f " B0 ; ::_thesis: f .: A0 c= B0
then A2: f .: A0 c= f .: (f " B0) by RELAT_1:123;
 f .: (f " B0) c= B0 by FUNCT_1:75;
hence  f .: A0 c= B0 by A2, XBOOLE_1:1; ::_thesis: verum
end;
end;

theorem :: FUNCT_2:96
for A, B being non empty set
for f being Function of A,B
for A0 being non empty Subset of A
for f0 being Function of A0,B st ( for c being Element of A st c in A0 holds
f . c = f0 . c ) holds
f | A0 = f0
proof
let A, B be non empty set ; ::_thesis: for f being Function of A,B
for A0 being non empty Subset of A
for f0 being Function of A0,B st ( for c being Element of A st c in A0 holds
f . c = f0 . c ) holds
f | A0 = f0
let f be Function of A,B; ::_thesis: for A0 being non empty Subset of A
for f0 being Function of A0,B st ( for c being Element of A st c in A0 holds
f . c = f0 . c ) holds
f | A0 = f0
let A0 be non empty Subset of A; ::_thesis: for f0 being Function of A0,B st ( for c being Element of A st c in A0 holds
f . c = f0 . c ) holds
f | A0 = f0
let f0 be Function of A0,B; ::_thesis: ( ( for c being Element of A st c in A0 holds
f . c = f0 . c ) implies f | A0 = f0 )
assume A1: for c being Element of A st c in A0 holds
f . c = f0 . c ; ::_thesis: f | A0 = f0
reconsider g = f | A0 as Function of A0,B by Th32;
 for c being Element of A0 holds g . c = f0 . c
proof
let c be Element of A0; ::_thesis: g . c = f0 . c
thus g . c = f . c by FUNCT_1:49
.= f0 . c by A1 ; ::_thesis: verum
end;
hence  f | A0 = f0 by Th63; ::_thesis: verum
end;

theorem :: FUNCT_2:97
for f being Function
for A0, C being set st C c= A0 holds
f .: C = (f | A0) .: C
proof
let f be Function; ::_thesis: for A0, C being set st C c= A0 holds
f .: C = (f | A0) .: C
let A0, C be set ; ::_thesis: ( C c= A0 implies f .: C = (f | A0) .: C )
assume A1: C c= A0 ; ::_thesis: f .: C = (f | A0) .: C
thus (f | A0) .: C = (f * (id A0)) .: C by RELAT_1:65
.= f .: ((id A0) .: C) by RELAT_1:126
.= f .: C by A1, FUNCT_1:92 ; ::_thesis: verum
end;

theorem :: FUNCT_2:98
for f being Function
for A0, D being set st f " D c= A0 holds
f " D = (f | A0) " D
proof
let f be Function; ::_thesis: for A0, D being set st f " D c= A0 holds
f " D = (f | A0) " D
let A0, D be set ; ::_thesis: ( f " D c= A0 implies f " D = (f | A0) " D )
assume A1: f " D c= A0 ; ::_thesis: f " D = (f | A0) " D
thus (f | A0) " D = (f * (id A0)) " D by RELAT_1:65
.= (id A0) " (f " D) by RELAT_1:146
.= f " D by A1, Th94 ; ::_thesis: verum
end;

scheme :: FUNCT_2:sch 10
MChoice{ F1() ->  non empty set , F2() ->  non empty set , F3( set ) ->  set } :
 ex t being Function of F1(),F2() st
for a being Element of F1() holds t . a in F3(a)
provided
A1: for a being Element of F1() holds F2() meets F3(a)
proof
defpred S1[ set , set ] means $2 in F3($1);
A2: for e being set st e in F1() holds
ex u being set st
( u in F2() & S1[e,u] ) by A1, XBOOLE_0:3;
consider t being Function such that
A3: ( dom t = F1() & rng t c= F2() ) and
A4: for e being set st e in F1() holds
S1[e,t . e] from FUNCT_1:sch_5(A2);
reconsider t = t as Function of F1(),F2() by A3, Def1, RELSET_1:4;
take  t ; ::_thesis: for a being Element of F1() holds t . a in F3(a)
let a be Element of F1(); ::_thesis: t . a in F3(a)
thus  t . a in F3(a) by A4; ::_thesis: verum
end;

theorem Th99: :: FUNCT_2:99
for X, D being non empty set
for p being Function of X,D
for i being Element of X holds p /. i = p . i
proof
let X, D be non empty set ; ::_thesis: for p being Function of X,D
for i being Element of X holds p /. i = p . i
let p be Function of X,D; ::_thesis: for i being Element of X holds p /. i = p . i
let i be Element of X; ::_thesis: p /. i = p . i
 i in X ;
then  i in dom p by Def1;
hence  p /. i = p . i by PARTFUN1:def_6; ::_thesis: verum
end;

registration
let X, D be non empty set ;
let p be Function of X,D;
let i be Element of X;
identifyp /. i with p . i;
correctness
compatibility
p /. i = p . i;
by Th99;
end;

theorem :: FUNCT_2:100
for S, X being set
for f being Function of S,X
for A being Subset of X st ( X = {} implies S = {} ) holds
(f " A) ` = f " (A `)
proof
let S, X be set ; ::_thesis: for f being Function of S,X
for A being Subset of X st ( X = {} implies S = {} ) holds
(f " A) ` = f " (A `)
let f be Function of S,X; ::_thesis: for A being Subset of X st ( X = {} implies S = {} ) holds
(f " A) ` = f " (A `)
let A be Subset of X; ::_thesis: ( ( X = {} implies S = {} ) implies (f " A) ` = f " (A `) )
assume A1: ( X = {} implies S = {} ) ; ::_thesis: (f " A) ` = f " (A `)
 A /\ (A `) = {} by XBOOLE_0:def_7, XBOOLE_1:79;
then (f " A) /\ (f " (A `)) = f " ({} X) by FUNCT_1:68
.= {} ;
then A2: f " A misses f " (A `) by XBOOLE_0:def_7;
(f " A) \/ (f " (A `)) = f " (A \/ (A `)) by RELAT_1:140
.= f " ([#] X) by SUBSET_1:10
.= [#] S by A1, Th40 ;
then ((f " A) `) /\ ((f " (A `)) `) = ([#] S) ` by XBOOLE_1:53
.= {} S by XBOOLE_1:37 ;
then  (f " A) ` misses (f " (A `)) ` by XBOOLE_0:def_7;
hence  (f " A) ` = f " (A `) by A2, SUBSET_1:25; ::_thesis: verum
end;

theorem :: FUNCT_2:101
for X, Y, Z being set
for D being non empty set
for f being Function of X,D st Y c= X & f .: Y c= Z holds
f | Y is Function of Y,Z
proof
let X, Y, Z be set ; ::_thesis: for D being non empty set
for f being Function of X,D st Y c= X & f .: Y c= Z holds
f | Y is Function of Y,Z
let D be non empty set ; ::_thesis: for f being Function of X,D st Y c= X & f .: Y c= Z holds
f | Y is Function of Y,Z
let f be Function of X,D; ::_thesis: ( Y c= X & f .: Y c= Z implies f | Y is Function of Y,Z )
assume that
A1: Y c= X and
A2: f .: Y c= Z ; ::_thesis: f | Y is Function of Y,Z
 dom f = X by Def1;
then A3: dom (f | Y) = Y by A1, RELAT_1:62;
A4: now__::_thesis:_(_Z_=_{}_implies_Y_=_{}_)
assume  Z = {} ; ::_thesis: Y = {}
then  rng (f | Y) = {} by A2, RELAT_1:115;
hence  Y = {} by A3, RELAT_1:42; ::_thesis: verum
end;
 rng (f | Y) c= Z by A2, RELAT_1:115;
hence  f | Y is Function of Y,Z by A3, A4, Def1, RELSET_1:4; ::_thesis: verum
end;

definition
let T, S be non empty set ;
let f be Function of T,S;
let G be Subset-Family of S;
funcf " G ->  Subset-Family of T means :Def9: :: FUNCT_2:def 9
 for A being Subset of T holds
( A in it iff ex B being Subset of S st
( B in G & A = f " B ) );
existence
 ex b1 being Subset-Family of T st
for A being Subset of T holds
( A in b1 iff ex B being Subset of S st
( B in G & A = f " B ) )
proof
defpred S1[ Subset of T] means  ex B being Subset of S st
( B in G & $1 = f " B );
 ex R being Subset-Family of T st
for A being Subset of T holds
( A in R iff S1[A] ) from SUBSET_1:sch_3();
hence  ex b1 being Subset-Family of T st
for A being Subset of T holds
( A in b1 iff ex B being Subset of S st
( B in G & A = f " B ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset-Family of T st ( for A being Subset of T holds
( A in b1 iff ex B being Subset of S st
( B in G & A = f " B ) ) ) & ( for A being Subset of T holds
( A in b2 iff ex B being Subset of S st
( B in G & A = f " B ) ) ) holds
b1 = b2
proof
let R1, R2 be Subset-Family of T; ::_thesis: ( ( for A being Subset of T holds
( A in R1 iff ex B being Subset of S st
( B in G & A = f " B ) ) ) & ( for A being Subset of T holds
( A in R2 iff ex B being Subset of S st
( B in G & A = f " B ) ) ) implies R1 = R2 )
assume that
A1: for A being Subset of T holds
( A in R1 iff ex B being Subset of S st
( B in G & A = f " B ) ) and
A2: for A being Subset of T holds
( A in R2 iff ex B being Subset of S st
( B in G & A = f " B ) ) ; ::_thesis: R1 = R2
 for x being set holds
( x in R1 iff x in R2 )
proof
let x be set ; ::_thesis: ( x in R1 iff x in R2 )
thus  ( x in R1 implies x in R2 ) ::_thesis: ( x in R2 implies x in R1 )
proof
assume A3: x in R1 ; ::_thesis: x in R2
then reconsider x = x as Subset of T ;
 ex B being Subset of S st
( B in G & x = f " B ) by A1, A3;
hence  x in R2 by A2; ::_thesis: verum
end;
assume A4: x in R2 ; ::_thesis: x in R1
then reconsider x = x as Subset of T ;
 ex B being Subset of S st
( B in G & x = f " B ) by A2, A4;
hence  x in R1 by A1; ::_thesis: verum
end;
hence  R1 = R2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def9 defines " FUNCT_2:def_9_:_
 for T, S being non empty set
for f being Function of T,S
for G being Subset-Family of S
for b5 being Subset-Family of T holds
( b5 = f " G iff for A being Subset of T holds
( A in b5 iff ex B being Subset of S st
( B in G & A = f " B ) ) );

theorem :: FUNCT_2:102
for T, S being non empty set
for f being Function of T,S
for A, B being Subset-Family of S st A c= B holds
f " A c= f " B
proof
let T, S be non empty set ; ::_thesis: for f being Function of T,S
for A, B being Subset-Family of S st A c= B holds
f " A c= f " B
let f be Function of T,S; ::_thesis: for A, B being Subset-Family of S st A c= B holds
f " A c= f " B
let A, B be Subset-Family of S; ::_thesis: ( A c= B implies f " A c= f " B )
assume A1: A c= B ; ::_thesis: f " A c= f " B
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f " A or x in f " B )
assume A2: x in f " A ; ::_thesis: x in f " B
then reconsider x = x as Subset of T ;
 ex C being Subset of S st
( C in B & x = f " C )
proof
consider C being Subset of S such that
A3: ( C in A & x = f " C ) by A2, Def9;
take  C ; ::_thesis: ( C in B & x = f " C )
thus  ( C in B & x = f " C ) by A1, A3; ::_thesis: verum
end;
hence  x in f " B by Def9; ::_thesis: verum
end;

definition
let T, S be non empty set ;
let f be Function of T,S;
let G be Subset-Family of T;
funcf .: G ->  Subset-Family of S means :Def10: :: FUNCT_2:def 10
 for A being Subset of S holds
( A in it iff ex B being Subset of T st
( B in G & A = f .: B ) );
existence
 ex b1 being Subset-Family of S st
for A being Subset of S holds
( A in b1 iff ex B being Subset of T st
( B in G & A = f .: B ) )
proof
thus  ex R being Subset-Family of S st
for A being Subset of S holds
( A in R iff ex B being Subset of T st
( B in G & A = f .: B ) ) ::_thesis: verum
proof
defpred S1[ Subset of S] means  ex B being Subset of T st
( B in G & $1 = f .: B );
 ex R being Subset-Family of S st
for A being Subset of S holds
( A in R iff S1[A] ) from SUBSET_1:sch_3();
hence  ex R being Subset-Family of S st
for A being Subset of S holds
( A in R iff ex B being Subset of T st
( B in G & A = f .: B ) ) ; ::_thesis: verum
end;
end;
uniqueness
 for b1, b2 being Subset-Family of S st ( for A being Subset of S holds
( A in b1 iff ex B being Subset of T st
( B in G & A = f .: B ) ) ) & ( for A being Subset of S holds
( A in b2 iff ex B being Subset of T st
( B in G & A = f .: B ) ) ) holds
b1 = b2
proof
let R1, R2 be Subset-Family of S; ::_thesis: ( ( for A being Subset of S holds
( A in R1 iff ex B being Subset of T st
( B in G & A = f .: B ) ) ) & ( for A being Subset of S holds
( A in R2 iff ex B being Subset of T st
( B in G & A = f .: B ) ) ) implies R1 = R2 )
assume that
A1: for A being Subset of S holds
( A in R1 iff ex B being Subset of T st
( B in G & A = f .: B ) ) and
A2: for A being Subset of S holds
( A in R2 iff ex B being Subset of T st
( B in G & A = f .: B ) ) ; ::_thesis: R1 = R2
 for x being set holds
( x in R1 iff x in R2 )
proof
let x be set ; ::_thesis: ( x in R1 iff x in R2 )
thus  ( x in R1 implies x in R2 ) ::_thesis: ( x in R2 implies x in R1 )
proof
assume A3: x in R1 ; ::_thesis: x in R2
then reconsider x = x as Subset of S ;
 ex B being Subset of T st
( B in G & x = f .: B ) by A1, A3;
hence  x in R2 by A2; ::_thesis: verum
end;
assume A4: x in R2 ; ::_thesis: x in R1
then reconsider x = x as Subset of S ;
 ex B being Subset of T st
( B in G & x = f .: B ) by A2, A4;
hence  x in R1 by A1; ::_thesis: verum
end;
hence  R1 = R2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def10 defines .: FUNCT_2:def_10_:_
 for T, S being non empty set
for f being Function of T,S
for G being Subset-Family of T
for b5 being Subset-Family of S holds
( b5 = f .: G iff for A being Subset of S holds
( A in b5 iff ex B being Subset of T st
( B in G & A = f .: B ) ) );

theorem :: FUNCT_2:103
for T, S being non empty set
for f being Function of T,S
for A, B being Subset-Family of T st A c= B holds
f .: A c= f .: B
proof
let T, S be non empty set ; ::_thesis: for f being Function of T,S
for A, B being Subset-Family of T st A c= B holds
f .: A c= f .: B
let f be Function of T,S; ::_thesis: for A, B being Subset-Family of T st A c= B holds
f .: A c= f .: B
let A, B be Subset-Family of T; ::_thesis: ( A c= B implies f .: A c= f .: B )
assume A1: A c= B ; ::_thesis: f .: A c= f .: B
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f .: A or x in f .: B )
assume A2: x in f .: A ; ::_thesis: x in f .: B
then reconsider x = x as Subset of S ;
 ex C being Subset of T st
( C in B & x = f .: C )
proof
consider C being Subset of T such that
A3: ( C in A & x = f .: C ) by A2, Def10;
take  C ; ::_thesis: ( C in B & x = f .: C )
thus  ( C in B & x = f .: C ) by A1, A3; ::_thesis: verum
end;
hence  x in f .: B by Def10; ::_thesis: verum
end;

theorem :: FUNCT_2:104
for T, S being non empty set
for f being Function of T,S
for B being Subset-Family of S
for P being Subset of S st f .: (f " B) is Cover of P holds
B is Cover of P
proof
let T, S be non empty set ; ::_thesis: for f being Function of T,S
for B being Subset-Family of S
for P being Subset of S st f .: (f " B) is Cover of P holds
B is Cover of P
let f be Function of T,S; ::_thesis: for B being Subset-Family of S
for P being Subset of S st f .: (f " B) is Cover of P holds
B is Cover of P
let B be Subset-Family of S; ::_thesis: for P being Subset of S st f .: (f " B) is Cover of P holds
B is Cover of P
let P be Subset of S; ::_thesis: ( f .: (f " B) is Cover of P implies B is Cover of P )
assume  f .: (f " B) is Cover of P ; ::_thesis: B is Cover of P
then A1: P c= union (f .: (f " B)) by SETFAM_1:def_11;
 P c= union B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in union B )
assume  x in P ; ::_thesis: x in union B
then consider Y being set  such that
A2: x in Y and
A3: Y in f .: (f " B) by A1, TARSKI:def_4;
 ex Z being set st
( x in Z & Z in B )
proof
reconsider Y = Y as Subset of S by A3;
consider Y1 being Subset of T such that
A4: Y1 in f " B and
A5: Y = f .: Y1 by A3, Def10;
consider Y2 being Subset of S such that
A6: ( Y2 in B & Y1 = f " Y2 ) by A4, Def9;
A7: f .: (f " Y2) c= Y2 by FUNCT_1:75;
reconsider Y2 = Y2 as set ;
take  Y2 ; ::_thesis: ( x in Y2 & Y2 in B )
thus  ( x in Y2 & Y2 in B ) by A2, A5, A6, A7; ::_thesis: verum
end;
hence  x in union B by TARSKI:def_4; ::_thesis: verum
end;
hence  B is Cover of P by SETFAM_1:def_11; ::_thesis: verum
end;

theorem :: FUNCT_2:105
for T, S being non empty set
for f being Function of T,S
for B being Subset-Family of T
for P being Subset of T st B is Cover of P holds
f " (f .: B) is Cover of P
proof
let T, S be non empty set ; ::_thesis: for f being Function of T,S
for B being Subset-Family of T
for P being Subset of T st B is Cover of P holds
f " (f .: B) is Cover of P
let f be Function of T,S; ::_thesis: for B being Subset-Family of T
for P being Subset of T st B is Cover of P holds
f " (f .: B) is Cover of P
let B be Subset-Family of T; ::_thesis: for P being Subset of T st B is Cover of P holds
f " (f .: B) is Cover of P
let P be Subset of T; ::_thesis: ( B is Cover of P implies f " (f .: B) is Cover of P )
assume  B is Cover of P ; ::_thesis: f " (f .: B) is Cover of P
then A1: P c= union B by SETFAM_1:def_11;
 P c= union (f " (f .: B))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in union (f " (f .: B)) )
assume  x in P ; ::_thesis: x in union (f " (f .: B))
then consider Y being set  such that
A2: x in Y and
A3: Y in B by A1, TARSKI:def_4;
 ex Z being set st
( x in Z & Z in f " (f .: B) )
proof
reconsider Y = Y as Subset of T by A3;
set Z = f " (f .: Y);
take  f " (f .: Y) ; ::_thesis: ( x in f " (f .: Y) & f " (f .: Y) in f " (f .: B) )
 dom f = T by Def1;
then A4: Y c= f " (f .: Y) by FUNCT_1:76;
 f .: Y in f .: B by A3, Def10;
hence  ( x in f " (f .: Y) & f " (f .: Y) in f " (f .: B) ) by A2, A4, Def9; ::_thesis: verum
end;
hence  x in union (f " (f .: B)) by TARSKI:def_4; ::_thesis: verum
end;
hence  f " (f .: B) is Cover of P by SETFAM_1:def_11; ::_thesis: verum
end;

theorem :: FUNCT_2:106
for T, S being non empty set
for f being Function of T,S
for Q being Subset-Family of S holds union (f .: (f " Q)) c= union Q
proof
let T, S be non empty set ; ::_thesis: for f being Function of T,S
for Q being Subset-Family of S holds union (f .: (f " Q)) c= union Q
let f be Function of T,S; ::_thesis: for Q being Subset-Family of S holds union (f .: (f " Q)) c= union Q
let Q be Subset-Family of S; ::_thesis: union (f .: (f " Q)) c= union Q
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (f .: (f " Q)) or x in union Q )
thus  ( x in union (f .: (f " Q)) implies x in union Q ) ::_thesis: verum
proof
assume  x in union (f .: (f " Q)) ; ::_thesis: x in union Q
then consider A being set  such that
A1: x in A and
A2: A in f .: (f " Q) by TARSKI:def_4;
reconsider A = A as Subset of S by A2;
consider A1 being Subset of T such that
A3: A1 in f " Q and
A4: A = f .: A1 by A2, Def10;
consider A2 being Subset of S such that
A5: ( A2 in Q & A1 = f " A2 ) by A3, Def9;
 f .: (f " A2) c= A2 by FUNCT_1:75;
hence  x in union Q by A1, A4, A5, TARSKI:def_4; ::_thesis: verum
end;
end;

theorem :: FUNCT_2:107
for T, S being non empty set
for f being Function of T,S
for P being Subset-Family of T holds union P c= union (f " (f .: P))
proof
let T, S be non empty set ; ::_thesis: for f being Function of T,S
for P being Subset-Family of T holds union P c= union (f " (f .: P))
let f be Function of T,S; ::_thesis: for P being Subset-Family of T holds union P c= union (f " (f .: P))
let P be Subset-Family of T; ::_thesis: union P c= union (f " (f .: P))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union P or x in union (f " (f .: P)) )
assume  x in union P ; ::_thesis: x in union (f " (f .: P))
then consider A being set  such that
A1: x in A and
A2: A in P by TARSKI:def_4;
A3: A c= T by A2;
reconsider A = A as Subset of T by A2;
reconsider A1 = f .: A as Subset of S ;
reconsider A2 = f " A1 as Subset of T ;
 A c= dom f by A3, Def1;
then A4: A c= A2 by FUNCT_1:76;
 A1 in f .: P by A2, Def10;
then  A2 in f " (f .: P) by Def9;
hence  x in union (f " (f .: P)) by A1, A4, TARSKI:def_4; ::_thesis: verum
end;

definition
let X, Z be set ;
let Y be non empty set ;
let f be Function of X,Y;
let p be Z -valued Function;
assume A1: rng f c= dom p ;
funcp /* f ->  Function of X,Z equals :Def11: :: FUNCT_2:def 11
p * f;
coherence
 p * f is Function of X,Z
proof
 dom f = X by Def1;
then A2: dom (p * f) = X by A1, RELAT_1:27;
then A3: p * f is total by PARTFUN1:def_2;
 rng (p * f) c= Z ;
hence  p * f is Function of X,Z by A3, A2, RELSET_1:4; ::_thesis: verum
end;
end;

:: deftheorem Def11 defines /* FUNCT_2:def_11_:_
 for X, Z being set
for Y being non empty set
for f being Function of X,Y
for p being b2 -valued Function st rng f c= dom p holds
p /* f = p * f;


theorem Th108: :: FUNCT_2:108
for Z, X being set
for Y being non empty set
for f being Function of X,Y
for p being PartFunc of Y,Z
for x being Element of X st X <> {} & rng f c= dom p holds
(p /* f) . x = p . (f . x)
proof
let Z, X be set ; ::_thesis: for Y being non empty set
for f being Function of X,Y
for p being PartFunc of Y,Z
for x being Element of X st X <> {} & rng f c= dom p holds
(p /* f) . x = p . (f . x)
let Y be non empty set ; ::_thesis: for f being Function of X,Y
for p being PartFunc of Y,Z
for x being Element of X st X <> {} & rng f c= dom p holds
(p /* f) . x = p . (f . x)
let f be Function of X,Y; ::_thesis: for p being PartFunc of Y,Z
for x being Element of X st X <> {} & rng f c= dom p holds
(p /* f) . x = p . (f . x)
let p be PartFunc of Y,Z; ::_thesis: for x being Element of X st X <> {} & rng f c= dom p holds
(p /* f) . x = p . (f . x)
let x be Element of X; ::_thesis: ( X <> {} & rng f c= dom p implies (p /* f) . x = p . (f . x) )
assume that
A1: X <> {} and
A2: rng f c= dom p ; ::_thesis: (p /* f) . x = p . (f . x)
 p /* f = p * f by A2, Def11;
hence  (p /* f) . x = p . (f . x) by A1, Th15; ::_thesis: verum
end;

theorem Th109: :: FUNCT_2:109
for Z, X being set
for Y being non empty set
for f being Function of X,Y
for p being PartFunc of Y,Z
for x being Element of X st X <> {} & rng f c= dom p holds
(p /* f) . x = p /. (f . x)
proof
let Z, X be set ; ::_thesis: for Y being non empty set
for f being Function of X,Y
for p being PartFunc of Y,Z
for x being Element of X st X <> {} & rng f c= dom p holds
(p /* f) . x = p /. (f . x)
let Y be non empty set ; ::_thesis: for f being Function of X,Y
for p being PartFunc of Y,Z
for x being Element of X st X <> {} & rng f c= dom p holds
(p /* f) . x = p /. (f . x)
let f be Function of X,Y; ::_thesis: for p being PartFunc of Y,Z
for x being Element of X st X <> {} & rng f c= dom p holds
(p /* f) . x = p /. (f . x)
let p be PartFunc of Y,Z; ::_thesis: for x being Element of X st X <> {} & rng f c= dom p holds
(p /* f) . x = p /. (f . x)
let x be Element of X; ::_thesis: ( X <> {} & rng f c= dom p implies (p /* f) . x = p /. (f . x) )
assume that
A1: X <> {} and
A2: rng f c= dom p ; ::_thesis: (p /* f) . x = p /. (f . x)
A3: f . x in rng f by A1, Th4;
thus (p /* f) . x = p . (f . x) by A1, A2, Th108
.= p /. (f . x) by A2, A3, PARTFUN1:def_6 ; ::_thesis: verum
end;

theorem :: FUNCT_2:110
for Z, X being set
for Y being non empty set
for f being Function of X,Y
for p being PartFunc of Y,Z
for g being Function of X,X st rng f c= dom p holds
(p /* f) * g = p /* (f * g)
proof
let Z, X be set ; ::_thesis: for Y being non empty set
for f being Function of X,Y
for p being PartFunc of Y,Z
for g being Function of X,X st rng f c= dom p holds
(p /* f) * g = p /* (f * g)
let Y be non empty set ; ::_thesis: for f being Function of X,Y
for p being PartFunc of Y,Z
for g being Function of X,X st rng f c= dom p holds
(p /* f) * g = p /* (f * g)
let f be Function of X,Y; ::_thesis: for p being PartFunc of Y,Z
for g being Function of X,X st rng f c= dom p holds
(p /* f) * g = p /* (f * g)
let p be PartFunc of Y,Z; ::_thesis: for g being Function of X,X st rng f c= dom p holds
(p /* f) * g = p /* (f * g)
let g be Function of X,X; ::_thesis: ( rng f c= dom p implies (p /* f) * g = p /* (f * g) )
A1: rng (f * g) c= rng f by RELAT_1:26;
assume A2: rng f c= dom p ; ::_thesis: (p /* f) * g = p /* (f * g)
hence (p /* f) * g = (p * f) * g by Def11
.= p * (f * g) by RELAT_1:36
.= p /* (f * g) by A2, A1, Def11, XBOOLE_1:1 ;
::_thesis: verum
end;

theorem :: FUNCT_2:111
for X, Y being non empty set
for f being Function of X,Y holds
( f is constant iff ex y being Element of Y st rng f = {y} )
proof
let X, Y be non empty set ; ::_thesis: for f being Function of X,Y holds
( f is constant iff ex y being Element of Y st rng f = {y} )
let f be Function of X,Y; ::_thesis: ( f is constant iff ex y being Element of Y st rng f = {y} )
hereby  ::_thesis: ( ex y being Element of Y st rng f = {y} implies f is constant )
consider x being set  such that
A1: x in dom f by XBOOLE_0:def_1;
set y = f . x;
reconsider y = f . x as Element of Y by A1, Th5;
assume A2: f is constant ; ::_thesis: ex y being Element of Y st rng f = {y}
take y = y; ::_thesis: rng f = {y}
 for y9 being set holds
( y9 in rng f iff y9 = y )
proof
let y9 be set ; ::_thesis: ( y9 in rng f iff y9 = y )
hereby  ::_thesis: ( y9 = y implies y9 in rng f )
assume  y9 in rng f ; ::_thesis: y9 = y
then  ex x9 being set st
( x9 in dom f & y9 = f . x9 ) by FUNCT_1:def_3;
hence  y9 = y by A2, A1, FUNCT_1:def_10; ::_thesis: verum
end;
assume  y9 = y ; ::_thesis: y9 in rng f
hence  y9 in rng f by A1, Th4; ::_thesis: verum
end;
hence  rng f = {y} by TARSKI:def_1; ::_thesis: verum
end;
given y being Element of Y such that A3: rng f = {y} ; ::_thesis: f is constant
let x, x9 be set ; :: according to FUNCT_1:def_10 ::_thesis: ( not x in proj1 f or not x9 in proj1 f or f . x = f . x9 )
assume  x in dom f ; ::_thesis: ( not x9 in proj1 f or f . x = f . x9 )
then A4: f . x in rng f by Th4;
assume  x9 in dom f ; ::_thesis: f . x = f . x9
then A5: f . x9 in rng f by Th4;
thus f . x = y by A3, A4, TARSKI:def_1
.= f . x9 by A3, A5, TARSKI:def_1 ; ::_thesis: verum
end;

theorem :: FUNCT_2:112
for A, B being non empty set
for x being Element of A
for f being Function of A,B holds f . x in rng f
proof
let A, B be non empty set ; ::_thesis: for x being Element of A
for f being Function of A,B holds f . x in rng f
let x be Element of A; ::_thesis: for f being Function of A,B holds f . x in rng f
let f be Function of A,B; ::_thesis: f . x in rng f
 dom f = A by Def1;
hence  f . x in rng f by FUNCT_1:def_3; ::_thesis: verum
end;

theorem Th113: :: FUNCT_2:113
for y, A, B being set
for f being Function of A,B st y in rng f holds
ex x being Element of A st y = f . x
proof
let y be set ; ::_thesis: for A, B being set
for f being Function of A,B st y in rng f holds
ex x being Element of A st y = f . x
let A, B be set ; ::_thesis: for f being Function of A,B st y in rng f holds
ex x being Element of A st y = f . x
let f be Function of A,B; ::_thesis: ( y in rng f implies ex x being Element of A st y = f . x )
assume  y in rng f ; ::_thesis: ex x being Element of A st y = f . x
then consider x being set  such that
A1: x in A and
A2: f . x = y by Th11;
reconsider x = x as Element of A by A1;
take  x ; ::_thesis: y = f . x
thus  y = f . x by A2; ::_thesis: verum
end;

theorem :: FUNCT_2:114
for Z being set
for A, B being non empty set
for f being Function of A,B st ( for x being Element of A holds f . x in Z ) holds
rng f c= Z
proof
let Z be set ; ::_thesis: for A, B being non empty set
for f being Function of A,B st ( for x being Element of A holds f . x in Z ) holds
rng f c= Z
let A, B be non empty set ; ::_thesis: for f being Function of A,B st ( for x being Element of A holds f . x in Z ) holds
rng f c= Z
let f be Function of A,B; ::_thesis: ( ( for x being Element of A holds f . x in Z ) implies rng f c= Z )
assume A1: for x being Element of A holds f . x in Z ; ::_thesis: rng f c= Z
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in Z )
assume  y in rng f ; ::_thesis: y in Z
then  ex x being Element of A st f . x = y by Th113;
hence  y in Z by A1; ::_thesis: verum
end;


theorem :: FUNCT_2:115
for Y, X being non empty set
for Z being set
for f being Function of X,Y
for g being PartFunc of Y,Z
for x being Element of X st g is total holds
(g /* f) . x = g . (f . x)
proof
let Y, X be non empty set ; ::_thesis: for Z being set
for f being Function of X,Y
for g being PartFunc of Y,Z
for x being Element of X st g is total holds
(g /* f) . x = g . (f . x)
let Z be set ; ::_thesis: for f being Function of X,Y
for g being PartFunc of Y,Z
for x being Element of X st g is total holds
(g /* f) . x = g . (f . x)
let f be Function of X,Y; ::_thesis: for g being PartFunc of Y,Z
for x being Element of X st g is total holds
(g /* f) . x = g . (f . x)
let g be PartFunc of Y,Z; ::_thesis: for x being Element of X st g is total holds
(g /* f) . x = g . (f . x)
let x be Element of X; ::_thesis: ( g is total implies (g /* f) . x = g . (f . x) )
assume  g is total ; ::_thesis: (g /* f) . x = g . (f . x)
then  dom g = Y by PARTFUN1:def_2;
then  rng f c= dom g ;
hence  (g /* f) . x = g . (f . x) by Th108; ::_thesis: verum
end;

theorem :: FUNCT_2:116
for Y, X being non empty set
for Z being set
for f being Function of X,Y
for g being PartFunc of Y,Z
for x being Element of X st g is total holds
(g /* f) . x = g /. (f . x)
proof
let Y, X be non empty set ; ::_thesis: for Z being set
for f being Function of X,Y
for g being PartFunc of Y,Z
for x being Element of X st g is total holds
(g /* f) . x = g /. (f . x)
let Z be set ; ::_thesis: for f being Function of X,Y
for g being PartFunc of Y,Z
for x being Element of X st g is total holds
(g /* f) . x = g /. (f . x)
let f be Function of X,Y; ::_thesis: for g being PartFunc of Y,Z
for x being Element of X st g is total holds
(g /* f) . x = g /. (f . x)
let g be PartFunc of Y,Z; ::_thesis: for x being Element of X st g is total holds
(g /* f) . x = g /. (f . x)
let x be Element of X; ::_thesis: ( g is total implies (g /* f) . x = g /. (f . x) )
assume  g is total ; ::_thesis: (g /* f) . x = g /. (f . x)
then  dom g = Y by PARTFUN1:def_2;
then  rng f c= dom g ;
hence  (g /* f) . x = g /. (f . x) by Th109; ::_thesis: verum
end;

theorem Th117: :: FUNCT_2:117
for X, Y being non empty set
for Z, S being set
for f being Function of X,Y
for g being PartFunc of Y,Z st rng f c= dom (g | S) holds
(g | S) /* f = g /* f
proof
let X, Y be non empty set ; ::_thesis: for Z, S being set
for f being Function of X,Y
for g being PartFunc of Y,Z st rng f c= dom (g | S) holds
(g | S) /* f = g /* f
let Z, S be set ; ::_thesis: for f being Function of X,Y
for g being PartFunc of Y,Z st rng f c= dom (g | S) holds
(g | S) /* f = g /* f
let f be Function of X,Y; ::_thesis: for g being PartFunc of Y,Z st rng f c= dom (g | S) holds
(g | S) /* f = g /* f
let g be PartFunc of Y,Z; ::_thesis: ( rng f c= dom (g | S) implies (g | S) /* f = g /* f )
assume A1: rng f c= dom (g | S) ; ::_thesis: (g | S) /* f = g /* f
let x be Element of X; :: according to FUNCT_2:def_8 ::_thesis: ((g | S) /* f) . x = (g /* f) . x
A2: dom (g | S) c= dom g by RELAT_1:60;
A3: f . x in rng f by Th4;
thus ((g | S) /* f) . x = (g | S) . (f . x) by A1, Th108
.= g . (f . x) by A1, A3, FUNCT_1:47
.= (g /* f) . x by A1, A2, Th108, XBOOLE_1:1 ; ::_thesis: verum
end;

theorem :: FUNCT_2:118
for X, Y being non empty set
for Z, S, T being set
for f being Function of X,Y
for g being PartFunc of Y,Z st rng f c= dom (g | S) & S c= T holds
(g | S) /* f = (g | T) /* f
proof
let X, Y be non empty set ; ::_thesis: for Z, S, T being set
for f being Function of X,Y
for g being PartFunc of Y,Z st rng f c= dom (g | S) & S c= T holds
(g | S) /* f = (g | T) /* f
let Z, S, T be set ; ::_thesis: for f being Function of X,Y
for g being PartFunc of Y,Z st rng f c= dom (g | S) & S c= T holds
(g | S) /* f = (g | T) /* f
let f be Function of X,Y; ::_thesis: for g being PartFunc of Y,Z st rng f c= dom (g | S) & S c= T holds
(g | S) /* f = (g | T) /* f
let g be PartFunc of Y,Z; ::_thesis: ( rng f c= dom (g | S) & S c= T implies (g | S) /* f = (g | T) /* f )
assume A1: rng f c= dom (g | S) ; ::_thesis: ( not S c= T or (g | S) /* f = (g | T) /* f )
assume  S c= T ; ::_thesis: (g | S) /* f = (g | T) /* f
then  g | S c= g | T by RELAT_1:75;
then A2: dom (g | S) c= dom (g | T) by RELAT_1:11;
thus (g | S) /* f = g /* f by A1, Th117
.= (g | T) /* f by A1, A2, Th117, XBOOLE_1:1 ; ::_thesis: verum
end;

theorem :: FUNCT_2:119
for D, A, B being non empty set
for H being Function of D,[:A,B:]
for d being Element of D holds H . d = [((pr1 H) . d),((pr2 H) . d)]
proof
let D, A, B be non empty set ; ::_thesis: for H being Function of D,[:A,B:]
for d being Element of D holds H . d = [((pr1 H) . d),((pr2 H) . d)]
let H be Function of D,[:A,B:]; ::_thesis: for d being Element of D holds H . d = [((pr1 H) . d),((pr2 H) . d)]
let d be Element of D; ::_thesis: H . d = [((pr1 H) . d),((pr2 H) . d)]
thus H . d = [((H . d) `1),((H . d) `2)] by MCART_1:21
.= [((H . d) `1),((pr2 H) . d)] by Def6
.= [((pr1 H) . d),((pr2 H) . d)] by Def5 ; ::_thesis: verum
end;

theorem :: FUNCT_2:120
for A1, A2, B1, B2 being set
for f being Function of A1,A2
for g being Function of B1,B2 st f tolerates g holds
f /\ g is Function of (A1 /\ B1),(A2 /\ B2)
proof
let A1, A2, B1, B2 be set ; ::_thesis: for f being Function of A1,A2
for g being Function of B1,B2 st f tolerates g holds
f /\ g is Function of (A1 /\ B1),(A2 /\ B2)
let f be Function of A1,A2; ::_thesis: for g being Function of B1,B2 st f tolerates g holds
f /\ g is Function of (A1 /\ B1),(A2 /\ B2)
let g be Function of B1,B2; ::_thesis: ( f tolerates g implies f /\ g is Function of (A1 /\ B1),(A2 /\ B2) )
assume A1: f tolerates g ; ::_thesis: f /\ g is Function of (A1 /\ B1),(A2 /\ B2)
A2: ( dom (f /\ g) c= (dom f) /\ (dom g) & (dom f) /\ (dom g) c= A1 /\ B1 ) by RELAT_1:2, XBOOLE_1:27;
A3: now__::_thesis:_(_dom_f_=_A1_&_A1_<>_{}_&_dom_g_=_B1_&_B1_<>_{}_implies_(_(_A1_/\_B1_<>_{}_implies_A2_/\_B2_<>_{}_)_&_dom_(f_/\_g)_=_A1_/\_B1_)_)
set a = the Element of A1 /\ B1;
assume that
A4: dom f = A1 and
 A1 <> {} and
A5: dom g = B1 and
 B1 <> {} ; ::_thesis: ( ( A1 /\ B1 <> {} implies A2 /\ B2 <> {} ) & dom (f /\ g) = A1 /\ B1 )
hereby  ::_thesis: dom (f /\ g) = A1 /\ B1
assume A6: A1 /\ B1 <> {} ; ::_thesis: A2 /\ B2 <> {}
then  the Element of A1 /\ B1 in A1 by XBOOLE_0:def_4;
then A7: f . the Element of A1 /\ B1 in rng f by A4, FUNCT_1:def_3;
 ( f . the Element of A1 /\ B1 = g . the Element of A1 /\ B1 & the Element of A1 /\ B1 in B1 ) by A1, A4, A5, A6, PARTFUN1:def_4, XBOOLE_0:def_4;
then  f . the Element of A1 /\ B1 in rng g by A5, FUNCT_1:def_3;
hence  A2 /\ B2 <> {} by A7, XBOOLE_0:def_4; ::_thesis: verum
end;
thus  dom (f /\ g) = A1 /\ B1 ::_thesis: verum
proof
thus  dom (f /\ g) c= A1 /\ B1 by A2, XBOOLE_1:1; :: according to XBOOLE_0:def_10 ::_thesis: A1 /\ B1 c= dom (f /\ g)
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A1 /\ B1 or a in dom (f /\ g) )
assume A8: a in A1 /\ B1 ; ::_thesis: a in dom (f /\ g)
then  a in A1 by XBOOLE_0:def_4;
then A9: [a,(f . a)] in f by A4, FUNCT_1:def_2;
 ( f . a = g . a & a in B1 ) by A1, A4, A5, A8, PARTFUN1:def_4, XBOOLE_0:def_4;
then  [a,(f . a)] in g by A5, FUNCT_1:def_2;
then  [a,(f . a)] in f /\ g by A9, XBOOLE_0:def_4;
hence  a in dom (f /\ g) by XTUPLE_0:def_12; ::_thesis: verum
end;
end;
 ( rng (f /\ g) c= (rng f) /\ (rng g) & (rng f) /\ (rng g) c= A2 /\ B2 ) by RELAT_1:13, XBOOLE_1:27;
then A10: rng (f /\ g) c= A2 /\ B2 by XBOOLE_1:1;
A11: ( A2 = {} or A2 <> {} ) ;
A12: ( B2 = {} or B2 <> {} ) ;
A13: now__::_thesis:_(_(_A2_/\_B2_<>_{}_&_dom_(f_/\_g)_=_A1_/\_B1_)_or_(_A1_/\_B1_=_{}_&_dom_(f_/\_g)_=_A1_/\_B1_)_or_(_A2_/\_B2_=_{}_&_A1_/\_B1_<>_{}_&_f_/\_g_=_{}_)_)
percases ( A2 /\ B2 <> {} or A1 /\ B1 = {} or ( A2 /\ B2 = {} & A1 /\ B1 <> {} ) ) ;
case A2 /\ B2 <> {} ; ::_thesis: dom (f /\ g) = A1 /\ B1
hence  dom (f /\ g) = A1 /\ B1 by A12, A3, Def1, A11; ::_thesis: verum
end;
case A1 /\ B1 = {} ; ::_thesis: dom (f /\ g) = A1 /\ B1
hence  dom (f /\ g) = A1 /\ B1 by A2; ::_thesis: verum
end;
case ( A2 /\ B2 = {} & A1 /\ B1 <> {} ) ; ::_thesis: f /\ g = {}
hence  f /\ g = {} by A12, A3, Def1, A11; ::_thesis: verum
end;
end;
end;
 dom (f /\ g) c= A1 /\ B1 by A2, XBOOLE_1:1;
hence  f /\ g is Function of (A1 /\ B1),(A2 /\ B2) by A10, A13, Def1, RELSET_1:4; ::_thesis: verum
end;

registration
let A, B be set ;
cluster Funcs (A,B) ->  functional ;
coherence
 Funcs (A,B) is functional
proof
let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in Funcs (A,B) or x is set )
assume  x in Funcs (A,B) ; ::_thesis: x is set
then  ex f being Function st
( x = f & dom f = A & rng f c= B ) by Def2;
hence  x is set ; ::_thesis: verum
end;
end;

definition
let A, B be set ;
mode FUNCTION_DOMAIN of A,B ->  non empty set  means :Def12: :: FUNCT_2:def 12
 for x being Element of it holds x is Function of A,B;
existence
 ex b1 being non empty set st
for x being Element of b1 holds x is Function of A,B
proof
take IT = { the Function of A,B}; ::_thesis: for x being Element of IT holds x is Function of A,B
let g be Element of IT; ::_thesis: g is Function of A,B
thus  g is Function of A,B by TARSKI:def_1; ::_thesis: verum
end;
end;

:: deftheorem Def12 defines FUNCTION_DOMAIN FUNCT_2:def_12_:_
 for A, B being set
for b3 being non empty set holds
( b3 is FUNCTION_DOMAIN of A,B iff for x being Element of b3 holds x is Function of A,B );

registration
let A, B be set ;
cluster  ->  functional for FUNCTION_DOMAIN of A,B;
coherence
 for b1 being FUNCTION_DOMAIN of A,B holds b1 is functional
proof
let F be FUNCTION_DOMAIN of A,B; ::_thesis: F is functional
thus  for x being set st x in F holds
x is Function by Def12; :: according to FUNCT_1:def_13 ::_thesis: verum
end;
end;

theorem :: FUNCT_2:121
for P, Q being set
for f being Function of P,Q holds {f} is FUNCTION_DOMAIN of P,Q
proof
let P, Q be set ; ::_thesis: for f being Function of P,Q holds {f} is FUNCTION_DOMAIN of P,Q
let f be Function of P,Q; ::_thesis: {f} is FUNCTION_DOMAIN of P,Q
 for g being Element of {f} holds g is Function of P,Q by TARSKI:def_1;
hence  {f} is FUNCTION_DOMAIN of P,Q by Def12; ::_thesis: verum
end;

theorem Th122: :: FUNCT_2:122
for P being set
for B being non empty set holds Funcs (P,B) is FUNCTION_DOMAIN of P,B
proof
let P be set ; ::_thesis: for B being non empty set holds Funcs (P,B) is FUNCTION_DOMAIN of P,B
let B be non empty set ; ::_thesis: Funcs (P,B) is FUNCTION_DOMAIN of P,B
 for f being Element of Funcs (P,B) holds f is Function of P,B by Th66;
hence  Funcs (P,B) is FUNCTION_DOMAIN of P,B by Def12; ::_thesis: verum
end;

definition
let A be set ;
let B be non empty set ;
:: original: Funcs
redefine func Funcs (A,B) ->  FUNCTION_DOMAIN of A,B;
coherence
 Funcs (A,B) is FUNCTION_DOMAIN of A,B by Th122;
let F be FUNCTION_DOMAIN of A,B;
:: original: Element
redefine mode Element of F ->  Function of A,B;
coherence
 for b1 being Element of F holds b1 is Function of A,B by Def12;
end;

registration
let I be set ;
cluster id I -> I -defined total for I -defined Function;
coherence
 for b1 being I -defined Function st b1 = id I holds
b1 is total ;
end;

definition
let X, A be non empty set ;
let F be Function of X,A;
let x be set ;
assume A1: x in X ;
:: original: /.
redefine funcF /. x ->  Element of A equals :: FUNCT_2:def 13
F . x;
compatibility
 for b1 being Element of A holds
( b1 = F /. x iff b1 = F . x )
proof
let a be Element of A; ::_thesis: ( a = F /. x iff a = F . x )
 x in dom F by A1, Def1;
hence  ( a = F /. x iff a = F . x ) by PARTFUN1:def_6; ::_thesis: verum
end;
end;

:: deftheorem  defines /. FUNCT_2:def_13_:_
 for X, A being non empty set
for F being Function of X,A
for x being set st x in X holds
F /. x = F . x;

theorem :: FUNCT_2:123
for X being non empty set
for f being Function of X,X
for g being b1 -valued Function holds dom (f * g) = dom g
proof
let X be non empty set ; ::_thesis: for f being Function of X,X
for g being X -valued Function holds dom (f * g) = dom g
let f be Function of X,X; ::_thesis: for g being X -valued Function holds dom (f * g) = dom g
let g be X -valued Function; ::_thesis: dom (f * g) = dom g
 dom f = X by Def1;
then  rng g c= dom f ;
hence  dom (f * g) = dom g by RELAT_1:27; ::_thesis: verum
end;

theorem :: FUNCT_2:124
for X being non empty set
for f being Function of X,X st ( for x being Element of X holds f . x = x ) holds
f = id X
proof
let X be non empty set ; ::_thesis: for f being Function of X,X st ( for x being Element of X holds f . x = x ) holds
f = id X
let f be Function of X,X; ::_thesis: ( ( for x being Element of X holds f . x = x ) implies f = id X )
assume A1: for x being Element of X holds f . x = x ; ::_thesis: f = id X
let x be Element of X; :: according to FUNCT_2:def_8 ::_thesis: f . x = (id X) . x
 x = (id X) . x by FUNCT_1:18;
hence  f . x = (id X) . x by A1; ::_thesis: verum
end;

definition
let O, E be set ;
mode Action of O,E is Function of O,(Funcs (E,E));
end;

theorem :: FUNCT_2:125
for x, A being set
for f, g being Function of {x},A st f . x = g . x holds
f = g
proof
let x, A be set ; ::_thesis: for f, g being Function of {x},A st f . x = g . x holds
f = g
let f, g be Function of {x},A; ::_thesis: ( f . x = g . x implies f = g )
assume A1: f . x = g . x ; ::_thesis: f = g
now__::_thesis:_for_y_being_set_st_y_in_{x}_holds_
f_._y_=_g_._y
let y be set ; ::_thesis: ( y in {x} implies f . y = g . y )
assume  y in {x} ; ::_thesis: f . y = g . y
then  y = x by TARSKI:def_1;
hence  f . y = g . y by A1; ::_thesis: verum
end;
hence  f = g by Th12; ::_thesis: verum
end;