begin
theorem
theorem
theorem Th3:
theorem Th4:
theorem
theorem Th6:
theorem Th7:
theorem
theorem
canceled;
theorem Th10:
theorem Th11:
theorem
theorem Th13:
theorem
theorem
theorem
theorem
canceled;
theorem
theorem
theorem Th20:
theorem
for
A,
B being
set st
A * c= B * holds
A c= B
theorem
theorem
theorem Th24:
theorem Th25:
begin
scheme
CardMono{
F1()
-> set ,
F2()
-> non
empty set ,
F3(
set )
-> set } :
provided
A1:
for
x being
set st
x in F1() holds
ex
d being
Element of
F2() st
x = F3(
d)
and A2:
for
d1,
d2 being
Element of
F2() st
F3(
d1)
= F3(
d2) holds
d1 = d2
scheme
CardMono9{
F1()
-> set ,
F2()
-> non
empty set ,
F3(
set )
-> set } :
provided
A1:
F1()
c= F2()
and A2:
for
d1,
d2 being
Element of
F2() st
F3(
d1)
= F3(
d2) holds
d1 = d2
begin
:: deftheorem Def1 defines In FUNCT_7:def 1 :
for
x,
y being
set st
x in y holds
In x,
y = x;
theorem
:: deftheorem Def2 defines equal_outside FUNCT_7:def 2 :
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
:: deftheorem Def3 defines +* FUNCT_7:def 3 :
theorem Th32:
theorem Th33:
theorem Th34:
theorem
theorem
theorem Th37:
theorem
theorem
theorem
begin
:: deftheorem Def4 defines compose FUNCT_7:def 4 :
:: deftheorem Def5 defines apply FUNCT_7:def 5 :
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem
theorem
theorem Th47:
theorem
theorem Th49:
theorem
theorem Th51:
theorem
theorem Th53:
theorem
theorem Th55:
theorem Th56:
theorem
theorem
:: deftheorem Def6 defines firstdom FUNCT_7:def 6 :
:: deftheorem Def7 defines lastrng FUNCT_7:def 7 :
theorem Th59:
theorem Th60:
theorem Th61:
:: deftheorem Def8 defines FuncSeq-like FUNCT_7:def 8 :
theorem Th62:
theorem Th63:
theorem Th64:
theorem
theorem
theorem
:: deftheorem Def9 defines FuncSequence FUNCT_7:def 9 :
:: deftheorem Def10 defines FuncSequence FUNCT_7:def 10 :
theorem Th68:
theorem
Lm1:
for X being set
for f being Function of X,X holds rng f c= dom f
Lm2:
for f being Function
for n being Element of NAT
for p1, p2 being Function of NAT ,(PFuncs ((dom f) \/ (rng f)),((dom f) \/ (rng f))) st p1 . 0 = id ((dom f) \/ (rng f)) & ( for k being Nat ex g being Function st
( g = p1 . k & p1 . (k + 1) = g * f ) ) & p2 . 0 = id ((dom f) \/ (rng f)) & ( for k being Nat ex g being Function st
( g = p2 . k & p2 . (k + 1) = g * f ) ) holds
p1 = p2
definition
let f be
Function;
let n be
Nat;
func iter f,
n -> Function means :
Def11:
ex
p being
Function of
NAT ,
(PFuncs ((dom f) \/ (rng f)),((dom f) \/ (rng f))) st
(
it = p . n &
p . 0 = id ((dom f) \/ (rng f)) & ( for
k being
Nat ex
g being
Function st
(
g = p . k &
p . (k + 1) = g * f ) ) );
existence
ex b1 being Function ex p being Function of NAT ,(PFuncs ((dom f) \/ (rng f)),((dom f) \/ (rng f))) st
( b1 = p . n & p . 0 = id ((dom f) \/ (rng f)) & ( for k being Nat ex g being Function st
( g = p . k & p . (k + 1) = g * f ) ) )
uniqueness
for b1, b2 being Function st ex p being Function of NAT ,(PFuncs ((dom f) \/ (rng f)),((dom f) \/ (rng f))) st
( b1 = p . n & p . 0 = id ((dom f) \/ (rng f)) & ( for k being Nat ex g being Function st
( g = p . k & p . (k + 1) = g * f ) ) ) & ex p being Function of NAT ,(PFuncs ((dom f) \/ (rng f)),((dom f) \/ (rng f))) st
( b2 = p . n & p . 0 = id ((dom f) \/ (rng f)) & ( for k being Nat ex g being Function st
( g = p . k & p . (k + 1) = g * f ) ) ) holds
b1 = b2
by Lm2;
end;
:: deftheorem Def11 defines iter FUNCT_7:def 11 :
Lm3:
for f being Function holds
( (id ((dom f) \/ (rng f))) * f = f & f * (id ((dom f) \/ (rng f))) = f )
theorem Th70:
Lm4:
for f being Function st rng f c= dom f holds
iter f,0 = id (dom f)
theorem Th71:
theorem Th72:
theorem Th73:
theorem Th74:
theorem
theorem Th76:
theorem Th77:
theorem
theorem Th79:
Lm5:
for f being Function
for m, k being Element of NAT st iter (iter f,m),k = iter f,(m * k) holds
iter (iter f,m),(k + 1) = iter f,(m * (k + 1))
theorem
theorem Th81:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
begin
theorem
theorem
theorem
theorem Th94:
theorem
theorem Th96:
theorem
theorem
theorem Th99:
theorem
:: deftheorem Def12 defines Swap FUNCT_7:def 12 :
theorem Th101:
theorem Th102:
theorem Th103:
theorem Th104:
theorem
scheme
Sch6{
F1()
-> set ,
F2()
-> non
empty set ,
F3(
set )
-> set } :
provided
A1:
F1()
c= F2()
and A2:
for
d1,
d2 being
Element of
F2() st
d1 in F1() &
d2 in F1() &
F3(
d1)
= F3(
d2) holds
d1 = d2
theorem
theorem
theorem
theorem Th109:
theorem
theorem
theorem Th112:
theorem
theorem
theorem
theorem
theorem Th117:
theorem Th118:
theorem
:: deftheorem defines followed_by FUNCT_7:def 13 :
theorem Th120:
theorem Th121:
theorem Th122:
:: deftheorem defines followed_by FUNCT_7:def 14 :
theorem Th123:
theorem Th124:
theorem Th125:
theorem Th126:
theorem Th127:
theorem Th128:
theorem
theorem
theorem
theorem