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 :
for X being set
for b2 being set holds
( b2 = SubFuncs X iff for x being set holds
( x in b2 iff ( x in X & x is Function ) ) );
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 :
for f, b2 being Function holds
( b2 = doms f iff ( dom b2 = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds
b2 . x = proj1 (f . x) ) ) );
:: deftheorem Def3 defines rngs FUNCT_6:def 3 :
for f, b2 being Function holds
( b2 = rngs f iff ( dom b2 = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds
b2 . x = proj2 (f . x) ) ) );
:: deftheorem defines meet FUNCT_6:def 4 :
for f being Function holds meet f = meet (rng f);
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 :
for f being Function
for x, y being set holds f .. x,y = (uncurry f) . x,y;
theorem
canceled;
theorem
theorem
theorem
theorem
begin
:: deftheorem defines <: FUNCT_6:def 6 :
for f being Function holds <:f:> = curry ((uncurry' f) | [:(meet (doms f)),(dom f):]);
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem
theorem Th54:
theorem
:: deftheorem Def7 defines Frege FUNCT_6:def 7 :
for f, b2 being Function holds
( b2 = Frege f iff ( dom b2 = product (doms f) & ( for g being Function st g in product (doms f) holds
ex h being Function st
( b2 . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds
h . x = (uncurry f) . x,(g . x) ) ) ) ) );
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 :
for f being Function
for X being set
for b3 being Function holds
( b3 = Funcs f,X iff ( dom b3 = dom f & ( for x being set st x in dom f holds
b3 . x = Funcs (f . x),X ) ) );
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 :
for X being set
for f, b3 being Function holds
( b3 = Funcs X,f iff ( dom b3 = dom f & ( for x being set st x in dom f holds
b3 . x = Funcs X,(f . x) ) ) );
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 :
for f being Function holds commute f = curry' (uncurry f);
theorem
theorem Th85:
theorem
theorem
theorem
theorem
theorem