let x1, x2, y1, z, y2 be set ; :: thesis: for E being non empty set
for F being Subset of (E ^omega )
for TS being transition-system of F st the Tran of TS is Function & x1,x2 ==>. y1,z,TS & x1,x2 ==>. y2,z,TS holds
y1 = y2
let E be non empty set ; :: thesis: for F being Subset of (E ^omega )
for TS being transition-system of F st the Tran of TS is Function & x1,x2 ==>. y1,z,TS & x1,x2 ==>. y2,z,TS holds
y1 = y2
let F be Subset of (E ^omega ); :: thesis: for TS being transition-system of F st the Tran of TS is Function & x1,x2 ==>. y1,z,TS & x1,x2 ==>. y2,z,TS holds
y1 = y2
let TS be transition-system of F; :: thesis: ( the Tran of TS is Function & x1,x2 ==>. y1,z,TS & x1,x2 ==>. y2,z,TS implies y1 = y2 )
assume A: the Tran of TS is Function ; :: thesis: ( not x1,x2 ==>. y1,z,TS or not x1,x2 ==>. y2,z,TS or y1 = y2 )
assume B: ( x1,x2 ==>. y1,z,TS & x1,x2 ==>. y2,z,TS ) ; :: thesis: y1 = y2
consider v1, w1 being Element of E ^omega such that
C1: ( v1 = z & x1,w1 -->. y1,TS & x2 = w1 ^ v1 ) by B, DefDir;
consider v2, w2 being Element of E ^omega such that
C2: ( v2 = z & x1,w2 -->. y2,TS & x2 = w2 ^ v2 ) by B, DefDir;
w1 = w2 by C1, C2, AFINSQ_1:31;
hence y1 = y2 by A, C1, C2, ThProd50; :: thesis: verum