begin
theorem
for
A,
B being
set st
A * c= B * holds
A c= B
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
theorem
for
x,
A,
B being
set st
x in A /\ B holds
In (
x,
A)
= In (
x,
B)
begin
Lm1:
for X being set
for f being Function of X,X holds rng f c= dom f
Lm2:
for f being Relation
for n being Element of NAT
for p1, p2 being Function of NAT,(bool [:(field f),(field f):]) st p1 . 0 = id (field f) & ( for k being Nat holds p1 . (k + 1) = f * (p1 . k) ) & p2 . 0 = id (field f) & ( for k being Nat holds p2 . (k + 1) = f * (p2 . k) ) holds
p1 = p2
Lm3:
for R being Relation holds
( (id (field R)) * R = R & R * (id (field R)) = R )
Lm4:
for R being Relation st rng R c= dom R holds
iter (R,0) = id (dom R)
Lm5:
for m, k being Element of NAT
for R being Relation st iter ((iter (R,m)),k) = iter (R,(m * k)) holds
iter ((iter (R,m)),(k + 1)) = iter (R,(m * (k + 1)))
begin
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