let x be object ; :: thesis: for X being set
for E being non empty set
for F1, F2 being Subset of (E ^omega)
for TS1 being non empty transition-system over F1
for TS2 being non empty transition-system over 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 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 over F1
for TS2 being non empty transition-system over 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 over F1
for TS2 being non empty transition-system over 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 over F1
for TS2 being non empty transition-system over 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 over F1; :: thesis: for TS2 being non empty transition-system over 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 over 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 :: thesis: for y being object st y in x -succ_of (X,TS2) holds
y in x -succ_of (X,TS1)

let y be object ; :: 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 :: thesis: for y being object st y in x -succ_of (X,TS1) holds
y in x -succ_of (X,TS2)

let y be object ; :: 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