theorem Th21:
for
x1,
x2,
y1,
y2 being
object for
E being non
empty set for
F1,
F2 being
Subset of
(E ^omega) for
TS1 being
transition-system over
F1 for
TS2 being
transition-system over
F2 st the
Tran of
TS1 = the
Tran of
TS2 &
x1,
x2 ==>. y1,
y2,
TS1 holds
x1,
x2 ==>. y1,
y2,
TS2