let x, X 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 holds
x -succ_of X,TS1 = x -succ_of X,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 holds
x -succ_of X,TS1 = x -succ_of X,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 holds
x -succ_of X,TS1 = x -succ_of X,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 holds
x -succ_of X,TS1 = x -succ_of X,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 implies x -succ_of X,TS1 = x -succ_of X,TS2 )
assume that
A1: the carrier of TS1 = the carrier of TS2 and
A2: the Tran of TS1 = the Tran of TS2 ; :: thesis: x -succ_of X,TS1 = x -succ_of X,TS2

A3: now

let y be set ; :: thesis: ( y in x -succ_of X,TS2 implies y in x -succ_of X,TS1 )
assume A4: y in x -succ_of X,TS2 ; :: thesis: y in x -succ_of X,TS1
then reconsider q = y as Element of TS2 ;
consider p being Element of TS2 such that
A5: p in X and
A6: p,x ==>* q,TS2 by A4, Th103;
reconsider q = q as Element of TS1 by A1;
reconsider p = p as Element of TS1 by A1;
p,x ==>* q,TS1 by A1, A2, A6, Th94;
hence y in x -succ_of X,TS1 by A5; :: thesis: verum

end;

now

let y be set ; :: thesis: ( y in x -succ_of X,TS1 implies y in x -succ_of X,TS2 )
assume A7: y in x -succ_of X,TS1 ; :: thesis: y in x -succ_of X,TS2
then reconsider q = y as Element of TS1 ;
consider p being Element of TS1 such that
A8: p in X and
A9: p,x ==>* q,TS1 by A7, Th103;
reconsider q = q as Element of TS2 by A1;
reconsider p = p as Element of TS2 by A1;
p,x ==>* q,TS2 by A1, A2, A9, Th94;
hence y in x -succ_of X,TS2 by A8; :: thesis: verum

end;

hence x -succ_of X,TS1 = x -succ_of X,TS2 by A3, TARSKI:2; :: thesis: verum