let x1, x2, y1, y2, z be object ; for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F st the Tran of TS is Function & x1,x2 ==>. y1,z,TS & x1,x2 ==>. y2,z,TS holds
y1 = y2
let E be non empty set ; for F being Subset of (E ^omega)
for TS being transition-system over F st the Tran of TS is Function & x1,x2 ==>. y1,z,TS & x1,x2 ==>. y2,z,TS holds
y1 = y2
let F be Subset of (E ^omega); for TS being transition-system over F st the Tran of TS is Function & x1,x2 ==>. y1,z,TS & x1,x2 ==>. y2,z,TS holds
y1 = y2
let TS be transition-system over F; ( the Tran of TS is Function & x1,x2 ==>. y1,z,TS & x1,x2 ==>. y2,z,TS implies y1 = y2 )
assume A1:
the Tran of TS is Function
; ( not x1,x2 ==>. y1,z,TS or not x1,x2 ==>. y2,z,TS or y1 = y2 )
assume that
A2:
x1,x2 ==>. y1,z,TS
and
A3:
x1,x2 ==>. y2,z,TS
; y1 = y2
consider v1, w1 being Element of E ^omega such that
A4:
v1 = z
and
A5:
x1,w1 -->. y1,TS
and
A6:
x2 = w1 ^ v1
by A2;
consider v2, w2 being Element of E ^omega such that
A7:
v2 = z
and
A8:
x1,w2 -->. y2,TS
and
A9:
x2 = w2 ^ v2
by A3;
w1 = w2
by A4, A6, A7, A9, AFINSQ_1:28;
hence
y1 = y2
by A1, A5, A8, Th17; verum