let x, y1, z, 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 the Tran of TS is Function & [x,[y1,z]] in ==>.-relation TS & [x,[y2,z]] 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 the Tran of TS is Function & [x,[y1,z]] in ==>.-relation TS & [x,[y2,z]] in ==>.-relation TS holds
y1 = y2
let F be Subset of (E ^omega ); :: thesis: for TS being non empty transition-system of F st the Tran of TS is Function & [x,[y1,z]] in ==>.-relation TS & [x,[y2,z]] in ==>.-relation TS holds
y1 = y2
let TS be non empty transition-system of F; :: thesis: ( the Tran of TS is Function & [x,[y1,z]] in ==>.-relation TS & [x,[y2,z]] in ==>.-relation TS implies y1 = y2 )
assume A: the Tran of TS is Function ; :: thesis: ( not [x,[y1,z]] in ==>.-relation TS or not [x,[y2,z]] in ==>.-relation TS or y1 = y2 )
assume B: ( [x,[y1,z]] in ==>.-relation TS & [x,[y2,z]] in ==>.-relation TS ) ; :: thesis: y1 = y2
then consider s being Element of TS, v being Element of E ^omega , t being Element of TS, w being Element of E ^omega such that
C: ( x = [s,v] & [y1,z] = [t,w] ) by ThRel10;
( s,v ==>. y1,z,TS & s,v ==>. y2,z,TS ) by B, C, DefRel;
hence y1 = y2 by A, ThDir40; :: thesis: verum