let X1, X2, x, y, z be set ; :: thesis: for TS1 being transition-system of X1
for TS2 being transition-system of X2 st the Tran of TS1 = the Tran of TS2 & x,y -->. z,TS1 holds
x,y -->. z,TS2
let TS1 be transition-system of X1; :: thesis: for TS2 being transition-system of X2 st the Tran of TS1 = the Tran of TS2 & x,y -->. z,TS1 holds
x,y -->. z,TS2
let TS2 be transition-system of X2; :: thesis: ( the Tran of TS1 = the Tran of TS2 & x,y -->. z,TS1 implies x,y -->. z,TS2 )
assume A1: the Tran of TS1 = the Tran of TS2 ; :: thesis: ( not x,y -->. z,TS1 or x,y -->. z,TS2 )
assume A2: x,y -->. z,TS1 ; :: thesis: x,y -->. z,TS2
[[x,y],z] in the Tran of TS1 by A2, DefProd;
hence x,y -->. z,TS2 by A1, DefProd; :: thesis: verum