theorem Th17: :: REWRITE3:17

for x, y, z1, z2 being object
for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F st the Tran of TS is Function & x,y -->. z1,TS & x,y -->. z2,TS holds
z1 = z2 by FUNCT_1:def 1;