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 holds
for k being Nat st k in dom P & k in dom Q holds
P . k = Q . k
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 holds
for k being Nat st k in dom P & k in dom Q holds
P . k = Q . k
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 holds
for k being Nat st k in dom P & k in dom Q holds
P . k = Q . k )
assume A: TS is deterministic ; :: thesis: for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 holds
for k being Nat st k in dom P & k in dom Q holds
P . k = Q . k
let P, Q be RedSequence of ==>.-relation TS; :: thesis: ( P . 1 = Q . 1 implies for k being Nat st k in dom P & k in dom Q holds
P . k = Q . k )
assume B: P . 1 = Q . 1 ; :: thesis: for k being Nat st k in dom P & k in dom Q holds
P . k = Q . k
defpred S₁[ Nat] means ( $1 in dom P & $1 in dom Q implies P . $1 = Q . $1 );
D: S₁[ 0 ] by FINSEQ_3:27;

E: now

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume E1: S₁[k] ; :: thesis: S₁[k + 1]

now

assume F0: ( k + 1 in dom P & k + 1 in dom Q ) ; :: thesis: P . (k + 1) = Q . (k + 1)

per cases ( ( k in dom P & k in dom Q ) or not k in dom P or not k in dom Q ) ;

suppose F1: ( k in dom P & k in dom Q ) ; :: thesis: P . (k + 1) = Q . (k + 1)

G1: [(P . k),(P . (k + 1))] in ==>.-relation TS by F0, F1, REWRITE1:def 2;
G2: [(Q . k),(Q . (k + 1))] in ==>.-relation TS by F0, F1, REWRITE1:def 2;
thus P . (k + 1) = Q . (k + 1) by A, E1, F1, G1, G2, ThRel120'; :: thesis: verum

end;

suppose ( not k in dom P or not k in dom Q ) ; :: thesis: P . (k + 1) = Q . (k + 1)

then k = 0 by F0, REWRITE2:1;
hence P . (k + 1) = Q . (k + 1) by B; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(D, E);
hence for k being Nat st k in dom P & k in dom Q holds
P . k = Q . k ; :: thesis: verum