:: deftheorem defines CylinderFunc PETRI_2:def 7 :
for A1, A2 being non trivial set
for B1, B2 being set
for C1, C2 being non trivial set
for D1, D2 being set
for F being Function of (thin_cylinders (A1,B1)),(thin_cylinders (C1,D1)) holds CylinderFunc (A1,B1,A2,B2,C1,D1,C2,D2,F) = ((Extcylinders (C1,D1,C2,D2)) * F) * (Ristcylinders (A1,B1,A2,B2));