:: deftheorem defines Ristcylinders PETRI_2:def 5 :
for A1 being non empty set
for A2 being non trivial set
for B1, B2 being set
for b₅ being Function of (thin_cylinders (A2,B2)),(thin_cylinders (A1,B1)) holds
( b₅ = Ristcylinders (A1,B1,A2,B2) iff 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) & b₅ . x = cylinder0 (A1,B1,Bo1,yo1) ) );