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 holds
for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 & len P = len Q holds
P = Q
let F be Subset of (E ^omega ); :: thesis: for TS being non empty transition-system of F st TS is deterministic holds
for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 & len P = len Q holds
P = Q
let TS be non empty transition-system of F; :: thesis: ( TS is deterministic implies for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 & len P = len Q holds
P = Q )
assume A: TS is deterministic ; :: thesis: for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 & len P = len Q holds
P = Q
let P, Q be RedSequence of ==>.-relation TS; :: thesis: ( P . 1 = Q . 1 & len P = len Q implies P = Q )
assume that
B1: P . 1 = Q . 1 and
B2: len P = len Q ; :: thesis: P = Q

now

let k be Nat; :: thesis: ( k in dom P implies P . k = Q . k )
assume C: k in dom P ; :: thesis: P . k = Q . k
then ( 1 <= k & k <= len P ) by FINSEQ_3:27;
then k in dom Q by B2, FINSEQ_3:27;
hence P . k = Q . k by A, B1, C, ThRedSeq130; :: thesis: verum

end;

hence P = Q by B2, FINSEQ_2:10; :: thesis: verum