let x, y1, y2 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] 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 of 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 of 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 of F; :: thesis: ( TS is deterministic & [x,y1] in ==>.-relation TS & [x,y2] in ==>.-relation TS implies y1 = y2 )
assume A: TS is deterministic ; :: thesis: ( not [x,y1] in ==>.-relation TS or not [x,y2] in ==>.-relation TS or y1 = y2 )
assume B: ( [x,y1] in ==>.-relation TS & [x,y2] in ==>.-relation TS ) ; :: thesis: y1 = y2
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
C1: ( x = [s1,v1] & y1 = [t1,w1] ) by B, ThRel10;
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
C2: ( x = [s2,v2] & y2 = [t2,w2] ) by B, ThRel10;
( s1,v1 ==>. t1,w1,TS & s1,v1 ==>. t2,w2,TS ) by B, C1, C2, DefRel;
then ( t1 = t2 & w1 = w2 ) by A, ThDir70;
hence y1 = y2 by C1, C2; :: thesis: verum