let E be non empty set ; :: thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over 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 over 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 over 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 A1: 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
A2: P . 1 = Q . 1 and
A3: len P = len Q ; :: thesis: P = Q

now :: thesis: for k being Nat st k in dom P holds
P . k = Q . k

let k be Nat; :: thesis: ( k in dom P implies P . k = Q . k )
assume A4: k in dom P ; :: thesis: P . k = Q . k
then ( 1 <= k & k <= len P ) by FINSEQ_3:25;
then k in dom Q by A3, FINSEQ_3:25;
hence P . k = Q . k by A1, A2, A4, Th67; :: thesis: verum

end;

hence P = Q by A3, FINSEQ_2:9; :: thesis: verum