let E be non empty set ; :: thesis: for TS being transition-system over Lex E st the Tran of TS is Function holds
TS is deterministic

let TS be transition-system over Lex E; :: thesis: ( the Tran of TS is Function implies TS is deterministic )
assume A1: the Tran of TS is Function ; :: thesis: TS is deterministic
A2: now :: thesis: for p being Element of TS
for u, v being Element of E ^omega st u <> v & [p,u] in dom the Tran of TS & [p,v] in dom the Tran of TS holds
for w being Element of E ^omega holds
( not u ^ w = v & not v ^ w = u )
let p be Element of TS; :: thesis: for u, v being Element of E ^omega st u <> v & [p,u] in dom the Tran of TS & [p,v] in dom the Tran of TS holds
for w being Element of E ^omega holds
( not u ^ w = v & not v ^ w = u )

let u, v be Element of E ^omega ; :: thesis: ( u <> v & [p,u] in dom the Tran of TS & [p,v] in dom the Tran of TS implies for w being Element of E ^omega holds
( not u ^ w = v & not v ^ w = u ) )

assume that
A3: u <> v and
A4: ( [p,u] in dom the Tran of TS & [p,v] in dom the Tran of TS ) ; :: thesis: for w being Element of E ^omega holds
( not u ^ w = v & not v ^ w = u )

( u in Lex E & v in Lex E ) by ;
hence for w being Element of E ^omega holds
( not u ^ w = v & not v ^ w = u ) by ; :: thesis: verum
end;
not <%> E in rng (dom the Tran of TS) by Th8;
hence TS is deterministic by ; :: thesis: verum