let x, y1, y2, z 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 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 over 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 over 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 over F; :: thesis: ( the Tran of TS is Function & [x,[y1,z]] in ==>.-relation TS & [x,[y2,z]] in ==>.-relation TS implies y1 = y2 )
assume A1: 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 that
A2: [x,[y1,z]] in ==>.-relation TS and
A3: [x,[y2,z]] in ==>.-relation TS ; :: thesis: y1 = y2
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
A4: x = [s,v] and
[y1,z] = [t,w] by A2, Th31;
( s,v ==>. y1,z,TS & s,v ==>. y2,z,TS ) by A2, A3, A4, Def4;
hence y1 = y2 by A1, Th27; :: thesis: verum