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 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 over 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 over 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 A1: 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 A2: 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 );

A3: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

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

now :: thesis: ( k + 1 in dom P & k + 1 in dom Q implies P . (k + 1) = Q . (k + 1) )

assume A5: ( 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 A6: ( k in dom P & k in dom Q ) ; :: thesis: P . (k + 1) = Q . (k + 1)

then ( [(P . k),(P . (k + 1))] in ==>.-relation TS & [(Q . k),(Q . (k + 1))] in ==>.-relation TS ) by A5, REWRITE1:def 2;
hence P . (k + 1) = Q . (k + 1) by A1, A4, A6, Th44; :: 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 A5, REWRITE2:1;
hence P . (k + 1) = Q . (k + 1) by A2; :: thesis: verum

end;

end;

end;

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

end;

A7: S₁[ 0 ] by FINSEQ_3:25;
for k being Nat holds S₁[k] from NAT_1:sch 2(A7, A3);
hence for k being Nat st k in dom P & k in dom Q holds
P . k = Q . k ; :: thesis: verum