let S be non empty set ; :: thesis: for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (BASSModel (R,BASSIGN))
for X being Subset of S holds (TransEG f) . X = (SIGMA f) /\ (Pred (X,R))
let R be total Relation of S,S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (BASSModel (R,BASSIGN))
for X being Subset of S holds (TransEG f) . X = (SIGMA f) /\ (Pred (X,R))
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f being Assign of (BASSModel (R,BASSIGN))
for X being Subset of S holds (TransEG f) . X = (SIGMA f) /\ (Pred (X,R))
let f be Assign of (BASSModel (R,BASSIGN)); :: thesis: for X being Subset of S holds (TransEG f) . X = (SIGMA f) /\ (Pred (X,R))
let X be Subset of S; :: 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