theorem Th3: :: PETRI_2:3

for A being non trivial set
for B, Bo1 being set
for yo1 being Function of Bo1,A
for Bo2 being set
for yo2 being Function of Bo2,A st Bo1 c= B & Bo2 c= B & cylinder0 (A,B,Bo1,yo1) = cylinder0 (A,B,Bo2,yo2) holds
( Bo1 = Bo2 & yo1 = yo2 )