let x, y, z be set ; :: thesis: for E being non empty set
for F1, F2 being Subset of (E ^omega)
for TS1 being non empty transition-system of F1
for TS2 being non empty transition-system of F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 & x,y ==>* z,TS1 holds
x,y ==>* z,TS2
let E be non empty set ; :: thesis: for F1, F2 being Subset of (E ^omega)
for TS1 being non empty transition-system of F1
for TS2 being non empty transition-system of F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 & x,y ==>* z,TS1 holds
x,y ==>* z,TS2
let F1, F2 be Subset of (E ^omega); :: thesis: for TS1 being non empty transition-system of F1
for TS2 being non empty transition-system of F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 & x,y ==>* z,TS1 holds
x,y ==>* z,TS2
let TS1 be non empty transition-system of F1; :: thesis: for TS2 being non empty transition-system of F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 & x,y ==>* z,TS1 holds
x,y ==>* z,TS2
let TS2 be non empty transition-system of F2; :: thesis: ( the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 & x,y ==>* z,TS1 implies x,y ==>* z,TS2 )
assume A1: ( the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 ) ; :: thesis: ( not x,y ==>* z,TS1 or x,y ==>* z,TS2 )
assume x,y ==>* z,TS1 ; :: thesis: x,y ==>* z,TS2
then x,y ==>* z, <%> E,TS1 by Def7;
then x,y ==>* z, <%> E,TS2 by A1, Th81;
hence x,y ==>* z,TS2 by Def7; :: thesis: verum