let x, y, z be object ; :: thesis: for X being set
for TS being transition-system over X st x,y -->. z,TS holds
( x in TS & y in X & z in TS & x in dom (dom the Tran of TS) & y in rng (dom the Tran of TS) & z in rng the Tran of TS )
let X be set ; :: thesis: for TS being transition-system over X st x,y -->. z,TS holds
( x in TS & y in X & z in TS & x in dom (dom the Tran of TS) & y in rng (dom the Tran of TS) & z in rng the Tran of TS )
let TS be transition-system over X; :: thesis: ( x,y -->. z,TS implies ( x in TS & y in X & z in TS & x in dom (dom the Tran of TS) & y in rng (dom the Tran of TS) & z in rng the Tran of TS ) )
assume x,y -->. z,TS ; :: thesis: ( x in TS & y in X & z in TS & x in dom (dom the Tran of TS) & y in rng (dom the Tran of TS) & z in rng the Tran of TS )
then A1: [[x,y],z] in the Tran of TS ;
then [x,y] in [: the carrier of TS,X:] by ZFMISC_1:87;
hence ( x in the carrier of TS & y in X & z in the carrier of TS ) by A1, ZFMISC_1:87; :: according to STRUCT_0:def 5 :: thesis: ( x in dom (dom the Tran of TS) & y in rng (dom the Tran of TS) & z in rng the Tran of TS )
[x,y] in dom the Tran of TS by A1, XTUPLE_0:def 12;
hence ( x in dom (dom the Tran of TS) & y in rng (dom the Tran of TS) ) by XTUPLE_0:def 12, XTUPLE_0:def 13; :: thesis: z in rng the Tran of TS
thus z in rng the Tran of TS by A1, XTUPLE_0:def 13; :: thesis: verum