let x, y1, y2, z1, z2 be object ; :: thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over 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 over 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 over 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 over F; :: thesis: ( TS is deterministic & [x,[y1,z1]] in ==>.-relation TS & [x,[y2,z2]] in ==>.-relation TS implies ( y1 = y2 & z1 = z2 ) )
assume A1: 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 ( [x,[y1,z1]] in ==>.-relation TS & [x,[y2,z2]] in ==>.-relation TS ) ; :: thesis: ( y1 = y2 & z1 = z2 )
then [y1,z1] = [y2,z2] by A1, Th44;
hence ( y1 = y2 & z1 = z2 ) by XTUPLE_0:1; :: thesis: verum