let S be non empty set ; :: thesis: for R being total Relation of ,
for BASSIGN being non empty Subset of
for f being Assign of (CTLModel R,BASSIGN)
for X being Subset of holds (TransEG f) . X = (SIGMA f) /\ (Pred X,R)
let R be total Relation of ,; :: thesis: for BASSIGN being non empty Subset of
for f being Assign of (CTLModel R,BASSIGN)
for X being Subset of holds (TransEG f) . X = (SIGMA f) /\ (Pred X,R)
let BASSIGN be non empty Subset of ; :: thesis: for f being Assign of (CTLModel R,BASSIGN)
for X being Subset of holds (TransEG f) . X = (SIGMA f) /\ (Pred X,R)
let f be Assign of (CTLModel R,BASSIGN); :: thesis: for X being Subset of holds (TransEG f) . X = (SIGMA f) /\ (Pred X,R)
let X be Subset of ; :: thesis: (TransEG f) . X = (SIGMA f) /\ (Pred X,R)
set g = Tau X,R,BASSIGN;
(TransEG f) . X = SigFaxTau f,X,R,BASSIGN by Def70
.= (SIGMA f) /\ (SIGMA (EX (Tau X,R,BASSIGN))) by Th33
.= (SIGMA f) /\ (Pred (SIGMA (Tau X,R,BASSIGN)),R) by Th50 ;
hence (TransEG f) . X = (SIGMA f) /\ (Pred X,R) by Th32; :: thesis: verum