let x, y1, y2, z1, z2 be object ; 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 ; 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); 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; ( 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
; ( 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 )
; ( y1 = y2 & z1 = z2 )
then
[y1,z1] = [y2,z2]
by A1, Th44;
hence
( y1 = y2 & z1 = z2 )
by XTUPLE_0:1; verum