begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem
theorem Th5:
theorem
theorem Th7:
theorem
theorem
theorem Th10:
begin
theorem Th11:
theorem Th12:
theorem Th13:
theorem
theorem
theorem Th16:
theorem Th17:
theorem
theorem Th19:
theorem Th20:
theorem
for
X,
Y,
Z,
V1,
V2 being
set for
f being
Function st (
curry f in Funcs X,
(Funcs Y,Z) or
curry' f in Funcs Y,
(Funcs X,Z) ) &
dom f c= [:V1,V2:] holds
f in Funcs [:X,Y:],
Z
theorem
for
X,
Y,
Z,
V1,
V2 being
set for
f being
Function st (
uncurry f in Funcs [:X,Y:],
Z or
uncurry' f in Funcs [:Y,X:],
Z ) &
rng f c= PFuncs V1,
V2 &
dom f = X holds
f in Funcs X,
(Funcs Y,Z)
theorem
theorem Th24:
theorem
for
X,
Y,
Z,
V1,
V2 being
set for
f being
Function st (
curry f in PFuncs X,
(PFuncs Y,Z) or
curry' f in PFuncs Y,
(PFuncs X,Z) ) &
dom f c= [:V1,V2:] holds
f in PFuncs [:X,Y:],
Z
theorem
for
X,
Y,
Z,
V1,
V2 being
set for
f being
Function st (
uncurry f in PFuncs [:X,Y:],
Z or
uncurry' f in PFuncs [:Y,X:],
Z ) &
rng f c= PFuncs V1,
V2 &
dom f c= X holds
f in PFuncs X,
(PFuncs Y,Z)
begin
:: deftheorem Def1 defines SubFuncs FUNCT_6:def 1 :
theorem Th27:
theorem Th28:
Lm1:
for X being set st ( for x being set st x in X holds
x is Function ) holds
SubFuncs X = X
theorem Th29:
theorem
:: deftheorem Def2 defines doms FUNCT_6:def 2 :
:: deftheorem Def3 defines rngs FUNCT_6:def 3 :
:: deftheorem defines meet FUNCT_6:def 4 :
theorem Th31:
theorem
theorem Th33:
theorem Th34:
theorem
for
f,
g,
h being
Function holds
(
doms <*f,g,h*> = <*(dom f),(dom g),(dom h)*> &
rngs <*f,g,h*> = <*(rng f),(rng g),(rng h)*> )
theorem Th36:
theorem Th37:
theorem
canceled;
theorem Th39:
theorem Th40:
theorem
theorem
theorem Th43:
:: deftheorem defines .. FUNCT_6:def 5 :
theorem
canceled;
theorem
theorem
theorem
theorem
begin
:: deftheorem defines <: FUNCT_6:def 6 :
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem
theorem Th54:
theorem
:: deftheorem Def7 defines Frege FUNCT_6:def 7 :
theorem
Lm2:
for f being Function holds rng (Frege f) c= product (rngs f)
theorem Th57:
Lm3:
for f being Function holds product (rngs f) c= rng (Frege f)
theorem Th58:
theorem Th59:
begin
theorem
theorem
theorem Th62:
theorem
theorem
theorem Th65:
theorem
theorem
theorem
theorem Th69:
theorem Th70:
theorem
begin
:: deftheorem Def8 defines Funcs FUNCT_6:def 8 :
theorem
theorem
theorem
theorem
theorem
Lm4:
for x, y, z being set
for f, g being Function st [x,y] in dom f & g = (curry f) . x & z in dom g holds
[x,z] in dom f
theorem
:: deftheorem Def9 defines Funcs FUNCT_6:def 9 :
Lm5:
for X being set
for f being Function st f <> {} & X <> {} holds
product (Funcs X,f), Funcs X,(product f) are_equipotent
theorem Th78:
theorem Th79:
theorem
theorem
theorem
theorem
begin
:: deftheorem FUNCT_6:def 10 :
canceled;
:: deftheorem FUNCT_6:def 11 :
canceled;
:: deftheorem defines commute FUNCT_6:def 12 :
theorem
theorem Th85:
theorem
theorem
theorem
theorem
theorem