theorem Th4:
for
A1,
A2 being non
empty set for
B1,
B2 being
set st
A1 c= A2 &
B1 c= B2 holds
ex
F being
Function of
(thin_cylinders (A1,B1)),
(thin_cylinders (A2,B2)) st
for
x being
set st
x in thin_cylinders (
A1,
B1) holds
ex
Bo being
Subset of
B1 ex
yo1 being
Function of
Bo,
A1 ex
yo2 being
Function of
Bo,
A2 st
(
Bo is
finite &
yo1 = yo2 &
x = cylinder0 (
A1,
B1,
Bo,
yo1) &
F . x = cylinder0 (
A2,
B2,
Bo,
yo2) )