let x, y, z1, z2 be set ; :: thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system of F st the Tran of TS is Function & x,y -->. z1,TS & x,y -->. z2,TS holds
z1 = z2
let E be non empty set ; :: thesis: for F being Subset of (E ^omega)
for TS being transition-system of F st the Tran of TS is Function & x,y -->. z1,TS & x,y -->. z2,TS holds
z1 = z2
let F be Subset of (E ^omega); :: thesis: for TS being transition-system of F st the Tran of TS is Function & x,y -->. z1,TS & x,y -->. z2,TS holds
z1 = z2
let TS be transition-system of F; :: thesis: ( the Tran of TS is Function & x,y -->. z1,TS & x,y -->. z2,TS implies z1 = z2 )
assume A1: the Tran of TS is Function ; :: thesis: ( not x,y -->. z1,TS or not x,y -->. z2,TS or z1 = z2 )
assume ( x,y -->. z1,TS & x,y -->. z2,TS ) ; :: thesis: z1 = z2
then ( [[x,y],z1] in the Tran of TS & [[x,y],z2] in the Tran of TS ) by Def2;
hence z1 = z2 by A1, FUNCT_1:def 1; :: thesis: verum