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 TS is deterministic & ==>.-relation TS reduces x,[y1,z] & ==>.-relation TS reduces x,[y2,z] 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 & ==>.-relation TS reduces x,[y1,z] & ==>.-relation TS reduces x,[y2,z] holds
y1 = y2
let F be Subset of (E ^omega ); :: thesis: for TS being non empty transition-system of F st TS is deterministic & ==>.-relation TS reduces x,[y1,z] & ==>.-relation TS reduces x,[y2,z] holds
y1 = y2
let TS be non empty transition-system of F; :: thesis: ( TS is deterministic & ==>.-relation TS reduces x,[y1,z] & ==>.-relation TS reduces x,[y2,z] implies y1 = y2 )
assume A: TS is deterministic ; :: thesis: ( not ==>.-relation TS reduces x,[y1,z] or not ==>.-relation TS reduces x,[y2,z] or y1 = y2 )
assume that
B1: ==>.-relation TS reduces x,[y1,z] and
B2: ==>.-relation TS reduces x,[y2,z] ; :: thesis: y1 = y2
consider P being RedSequence of ==>.-relation TS such that
C1: ( P . 1 = x & P . (len P) = [y1,z] ) by B1, REWRITE1:def 3;
consider Q being RedSequence of ==>.-relation TS such that
C2: ( Q . 1 = x & Q . (len Q) = [y2,z] ) by B2, REWRITE1:def 3;
( (P . (len P)) `2 = z & (Q . (len Q)) `2 = z ) by C1, C2, MCART_1:7;
then P = Q by A, C1, C2, ThRedSeq140;
hence y1 = y2 by C1, C2, ZFMISC_1:33; :: thesis: verum