let E be non empty set ; :: thesis: for F being Subset of (E ^omega )
for TS being transition-system of F st dom the Tran of TS = {} holds
TS is deterministic
let F be Subset of (E ^omega ); :: thesis: for TS being transition-system of F st dom the Tran of TS = {} holds
TS is deterministic
let TS be transition-system of F; :: thesis: ( dom the Tran of TS = {} implies TS is deterministic )
assume A: dom the Tran of TS = {} ; :: thesis: TS is deterministic
then B: the Tran of TS = {} ;
for s being Element of TS
for u, v being Element of E ^omega st u <> v & [s,u] in dom the Tran of TS & [s,v] in dom the Tran of TS holds
for w being Element of E ^omega holds
( not u ^ w = v & not v ^ w = u ) by A;
hence TS is deterministic by DefDetTS, B, RELAT_1:60; :: thesis: verum