let x be object ; :: thesis:
let X be set ; :: thesis:
let E be non empty set ; :: thesis:
let F1, F2 be Subset of (E ^omega); :: thesis:
let TS1 be non empty transition-system over F1; :: thesis:
let TS2 be non empty transition-system over F2; :: thesis:
assume that
A1: the carrier of TS1 = the carrier of TS2 and
A2: the Tran of TS1 = the Tran of TS2 ; :: thesis:

A3: now :: thesis:

let y be object ; :: thesis:
assume A4: y in x -succ_of (X,TS2) ; :: thesis:
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:

end;

now :: thesis:

let y be object ; :: thesis:
assume A7: y in x -succ_of (X,TS1) ; :: thesis:
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:

end;

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