:: deftheorem Def1 defines cylinder0 PETRI_2:def 1 :
for A being non empty set
for B, Bo being set
for yo being Function of Bo,A st Bo c= B holds
cylinder0 (A,B,Bo,yo) = { y where y is Function of B,A : y | Bo = yo } ;