let x, y1, y2 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] in ==>.-relation TS & [x,y2] in ==>.-relation TS holds
y1 = y2
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] in ==>.-relation TS & [x,y2] in ==>.-relation TS holds
y1 = y2
let F be Subset of (E ^omega); :: thesis: for TS being non empty transition-system over F st TS is deterministic & [x,y1] in ==>.-relation TS & [x,y2] in ==>.-relation TS holds
y1 = y2
let TS be non empty transition-system over F; :: thesis: ( TS is deterministic & [x,y1] in ==>.-relation TS & [x,y2] in ==>.-relation TS implies y1 = y2 )
assume A1: TS is deterministic ; :: thesis: ( not [x,y1] in ==>.-relation TS or not [x,y2] in ==>.-relation TS or y1 = y2 )
assume that
A2: [x,y1] in ==>.-relation TS and
A3: [x,y2] in ==>.-relation TS ; :: thesis: y1 = y2
consider s2 being Element of TS, v2 being Element of E ^omega , t2 being Element of TS, w2 being Element of E ^omega such that
x = [s2,v2] and
A4: y2 = [t2,w2] by A3, Th31;
consider s1 being Element of TS, v1 being Element of E ^omega , t1 being Element of TS, w1 being Element of E ^omega such that
A5: x = [s1,v1] and
A6: y1 = [t1,w1] by A2, Th31;
A7: s1,v1 ==>. t1,w1,TS by A2, A5, A6, Def4;
A8: s1,v1 ==>. t2,w2,TS by A3, A5, A4, Def4;
then t1 = t2 by A1, A7, Th30;
hence y1 = y2 by A1, A6, A4, A7, A8, Th30; :: thesis: verum