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