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
B:
now let y be
set ;
:: thesis: ( y in x -succ_of X,TS1 implies y in x -succ_of X,TS2 )assume C0:
y in x -succ_of X,
TS1
;
:: thesis: y in x -succ_of X,TS2then reconsider q =
y as
Element of
TS1 ;
consider p being
Element of
TS1 such that C:
(
p in X &
p,
x ==>* q,
TS1 )
by C0, ThSucc10;
reconsider p =
p as
Element of
TS2 by A1;
reconsider q =
q as
Element of
TS2 by A1;
p,
x ==>* q,
TS2
by C, A1, A2, ThAcc5;
hence
y in x -succ_of X,
TS2
by C;
:: thesis: verum end;
now let y be
set ;
:: thesis: ( y in x -succ_of X,TS2 implies y in x -succ_of X,TS1 )assume C0:
y in x -succ_of X,
TS2
;
:: thesis: y in x -succ_of X,TS1then reconsider q =
y as
Element of
TS2 ;
consider p being
Element of
TS2 such that C:
(
p in X &
p,
x ==>* q,
TS2 )
by C0, ThSucc10;
reconsider p =
p as
Element of
TS1 by A1;
reconsider q =
q as
Element of
TS1 by A1;
p,
x ==>* q,
TS1
by C, A1, A2, ThAcc5;
hence
y in x -succ_of X,
TS1
by C;
:: thesis: verum end;
hence
x -succ_of X,TS1 = x -succ_of X,TS2
by B, TARSKI:2; :: thesis: verum