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 that
A1: the carrier of TS1 = the carrier of TS2 and
A2: 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 DefAcc;
then x,y ==>* z, <%> E,TS2 by A1, A2, ThTran5;
hence x,y ==>* z,TS2 by DefAcc; :: thesis: verum