let x, y1, z1, y2, z2 be set ; :: thesis: for E being non empty set
for F being Subset of (E ^omega )
for TS being non empty transition-system of F st TS is deterministic & [x,[y1,z1]] in ==>.-relation TS & [x,[y2,z2]] in ==>.-relation TS holds
( y1 = y2 & z1 = z2 )
let E be non empty set ; :: thesis: for F being Subset of (E ^omega )
for TS being non empty transition-system of F st TS is deterministic & [x,[y1,z1]] in ==>.-relation TS & [x,[y2,z2]] in ==>.-relation TS holds
( y1 = y2 & z1 = z2 )
let F be Subset of (E ^omega ); :: thesis: for TS being non empty transition-system of F st TS is deterministic & [x,[y1,z1]] in ==>.-relation TS & [x,[y2,z2]] in ==>.-relation TS holds
( y1 = y2 & z1 = z2 )
let TS be non empty transition-system of F; :: thesis: ( TS is deterministic & [x,[y1,z1]] in ==>.-relation TS & [x,[y2,z2]] in ==>.-relation TS implies ( y1 = y2 & z1 = z2 ) )
assume A: TS is deterministic ; :: thesis: ( not [x,[y1,z1]] in ==>.-relation TS or not [x,[y2,z2]] in ==>.-relation TS or ( y1 = y2 & z1 = z2 ) )
assume B: ( [x,[y1,z1]] in ==>.-relation TS & [x,[y2,z2]] in ==>.-relation TS ) ; :: thesis: ( y1 = y2 & z1 = z2 )
[y1,z1] = [y2,z2] by A, B, ThRel120';
hence ( y1 = y2 & z1 = z2 ) by ZFMISC_1:33; :: thesis: verum