begin
:: deftheorem Def1 defines Function-like FUNCT_1:def 1 :
theorem
canceled;
theorem
canceled;
scheme
GraphFunc{
F1()
-> set ,
P1[
set ,
set ] } :
ex
f being
Function st
for
x,
y being
set holds
(
[x,y] in f iff (
x in F1() &
P1[
x,
y] ) )
provided
A1:
for
x,
y1,
y2 being
set st
P1[
x,
y1] &
P1[
x,
y2] holds
y1 = y2
:: deftheorem FUNCT_1:def 2 :
canceled;
:: deftheorem FUNCT_1:def 3 :
canceled;
:: deftheorem Def4 defines . FUNCT_1:def 4 :
for
f being
Function for
x,
b3 being
set holds
( (
x in dom f implies (
b3 = f . x iff
[x,b3] in f ) ) & ( not
x in dom f implies (
b3 = f . x iff
b3 = {} ) ) );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th8:
theorem Th9:
:: deftheorem Def5 defines rng FUNCT_1:def 5 :
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem Th14:
scheme
FuncEx{
F1()
-> set ,
P1[
set ,
set ] } :
ex
f being
Function st
(
dom f = F1() & ( for
x being
set st
x in F1() holds
P1[
x,
f . x] ) )
provided
A1:
for
x,
y1,
y2 being
set st
x in F1() &
P1[
x,
y1] &
P1[
x,
y2] holds
y1 = y2
and A2:
for
x being
set st
x in F1() holds
ex
y being
set st
P1[
x,
y]
theorem Th15:
theorem
theorem
theorem
theorem
theorem
theorem Th21:
theorem Th22:
theorem Th23:
theorem
canceled;
theorem
theorem
canceled;
theorem Th27:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th34:
theorem
theorem
canceled;
theorem Th37:
theorem
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem Th44:
:: deftheorem FUNCT_1:def 6 :
canceled;
:: deftheorem FUNCT_1:def 7 :
canceled;
:: deftheorem Def8 defines one-to-one FUNCT_1:def 8 :
theorem
canceled;
theorem Th46:
theorem Th47:
theorem
theorem
theorem
theorem
theorem Th52:
theorem
:: deftheorem Def9 defines " FUNCT_1:def 9 :
theorem Th54:
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
theorem Th59:
theorem
theorem Th61:
theorem Th62:
Lm1:
for X being set
for g2, f, g1 being Function st rng g2 = X & f * g2 = id (dom g1) & g1 * f = id X holds
g1 = g2
theorem Th63:
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
theorem Th70:
theorem Th71:
theorem Th72:
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem Th85:
theorem
theorem
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
:: deftheorem FUNCT_1:def 10 :
canceled;
:: deftheorem FUNCT_1:def 11 :
canceled;
:: deftheorem Def12 defines .: FUNCT_1:def 12 :
for
f being
Function for
X being
set for
b3 being
set holds
(
b3 = f .: X iff for
y being
set holds
(
y in b3 iff ex
x being
set st
(
x in dom f &
x in X &
y = f . x ) ) );
theorem
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 Th117:
theorem
theorem
canceled;
theorem
theorem Th121:
theorem
theorem
theorem
theorem
theorem
:: deftheorem Def13 defines " FUNCT_1:def 13 :
for
f being
Function for
Y being
set for
b3 being
set holds
(
b3 = f " Y iff for
x being
set holds
(
x in b3 iff (
x in dom f &
f . x in Y ) ) );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th137:
theorem
theorem
theorem
canceled;
theorem
theorem Th142:
theorem
theorem Th144:
theorem Th145:
theorem Th146:
theorem
theorem
theorem Th149:
theorem
theorem
theorem Th152:
theorem
theorem
theorem
theorem
theorem
theorem Th158:
theorem
theorem
theorem
begin
theorem
:: deftheorem Def15 defines empty-yielding FUNCT_1:def 14 :
:: deftheorem Def15 defines non-empty FUNCT_1:def 15 :
:: deftheorem Def16 defines constant FUNCT_1:def 16 :
theorem
theorem
:: deftheorem defines = FUNCT_1:def 17 :
theorem
theorem
theorem Th167:
theorem
theorem
theorem
theorem
:: deftheorem defines the_value_of FUNCT_1:def 18 :
theorem
:: deftheorem Def19 defines functional FUNCT_1:def 19 :
:: deftheorem Def20 defines -compatible FUNCT_1:def 20 :
theorem
theorem Th174:
theorem