begin
:: deftheorem Def1 defines quasi_total FUNCT_2:def 1 :
theorem
canceled;
theorem
canceled;
theorem
theorem Th4:
theorem
theorem Th6:
theorem Th7:
theorem
theorem
scheme
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] )
scheme
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()
:: deftheorem Def2 defines Funcs FUNCT_2:def 2 :
theorem
canceled;
theorem Th11:
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
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
theorem Th17:
theorem Th18:
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
theorem Th19:
theorem
theorem Th21:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th31:
theorem
theorem
canceled;
theorem
theorem
theorem
theorem
theorem Th38:
theorem
canceled;
theorem
theorem
theorem
canceled;
theorem
theorem
theorem
theorem
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 ) )
theorem
theorem Th48:
theorem
theorem Th50:
theorem
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem Th62:
theorem
canceled;
theorem
theorem Th65:
theorem Th66:
theorem Th67:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th73:
theorem
canceled;
theorem
theorem
theorem Th77:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
:: deftheorem Def3 defines onto FUNCT_2:def 3 :
:: deftheorem Def4 defines bijective FUNCT_2:def 4 :
theorem Th83:
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th92:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th113:
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
theorem
canceled;
theorem Th115:
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 )
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
begin
theorem Th121:
scheme
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() ) )
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem Th133:
theorem
theorem
canceled;
theorem Th136:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th142:
theorem
theorem
canceled;
theorem Th145:
theorem
theorem
canceled;
theorem Th148:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem Th155:
theorem
theorem
canceled;
theorem Th158:
theorem
theorem
theorem Th161:
theorem
theorem
canceled;
theorem
theorem
theorem Th166:
theorem Th167:
theorem
begin
theorem
definition
let A,
B,
C be non
empty set ;
canceled;let f be
Function of
A,
[:B,C:];
pr1redefine func pr1 f -> Function of
A,
B means :
Def6:
for
x being
Element of
A holds
it . x = (f . x) `1 ;
coherence
pr1 f is Function of A,B
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 )
pr2redefine func pr2 f -> Function of
A,
C means :
Def7:
for
x being
Element of
A holds
it . x = (f . x) `2 ;
coherence
pr2 f is Function of A,C
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 )
end;
:: deftheorem FUNCT_2:def 5 :
canceled;
:: deftheorem Def6 defines pr1 FUNCT_2:def 6 :
:: deftheorem Def7 defines pr2 FUNCT_2:def 7 :
:: deftheorem defines = FUNCT_2:def 8 :
:: deftheorem defines = FUNCT_2:def 9 :
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
theorem Th171:
theorem
theorem
theorem
theorem
theorem Th176:
theorem
theorem
:: deftheorem Def10 defines " FUNCT_2:def 10 :
theorem
:: deftheorem Def11 defines .: FUNCT_2:def 11 :
theorem
theorem
theorem
theorem
theorem
:: deftheorem Def12 defines /* FUNCT_2:def 12 :
theorem Th185:
theorem Th186:
theorem
theorem
theorem
theorem Th190:
theorem
theorem
theorem
theorem Th194:
theorem
theorem
theorem
:: deftheorem Def13 defines FUNCTION_DOMAIN FUNCT_2:def 13 :
theorem
theorem Th199:
:: deftheorem defines /. FUNCT_2:def 14 :
theorem
theorem