theorem Th5:
for
A1,
A2 being non
empty set for
B1,
B2 being
set ex
G being
Function of
(thin_cylinders (A2,B2)),
(thin_cylinders (A1,B1)) st
for
x being
set st
x in thin_cylinders (
A2,
B2) holds
ex
Bo2 being
Subset of
B2 ex
Bo1 being
Subset of
B1 ex
yo1 being
Function of
Bo1,
A1 ex
yo2 being
Function of
Bo2,
A2 st
(
Bo1 is
finite &
Bo2 is
finite &
Bo1 = (B1 /\ Bo2) /\ (yo2 " A1) &
yo1 = yo2 | Bo1 &
x = cylinder0 (
A2,
B2,
Bo2,
yo2) &
G . x = cylinder0 (
A1,
B1,
Bo1,
yo1) )