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
==>.-relation TS is Function-like
let F be Subset of (E ^omega); :: thesis: for TS being non empty transition-system over F st TS is deterministic holds
==>.-relation TS is Function-like
let TS be non empty transition-system over F; :: thesis: ( TS is deterministic implies ==>.-relation TS is Function-like )
assume TS is deterministic ; :: thesis: ==>.-relation TS is Function-like
then for x, y, z being object st [x,y] in ==>.-relation TS & [x,z] in ==>.-relation TS holds
y = z by Th44;
hence ==>.-relation TS is Function-like by FUNCT_1:def 1; :: thesis: verum