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, g being Assign of (BASSModel (R,BASSIGN))
for X being Subset of S holds (TransEU (f,g)) . X = (SIGMA g) \/ ((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, g being Assign of (BASSModel (R,BASSIGN))
for X being Subset of S holds (TransEU (f,g)) . X = (SIGMA g) \/ ((SIGMA f) /\ (Pred (X,R)))
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f, g being Assign of (BASSModel (R,BASSIGN))
for X being Subset of S holds (TransEU (f,g)) . X = (SIGMA g) \/ ((SIGMA f) /\ (Pred (X,R)))
let f, g be Assign of (BASSModel (R,BASSIGN)); :: thesis: for X being Subset of S holds (TransEU (f,g)) . X = (SIGMA g) \/ ((SIGMA f) /\ (Pred (X,R)))
let X be Subset of S; :: thesis: (TransEU (f,g)) . X = (SIGMA g) \/ ((SIGMA f) /\ (Pred (X,R)))
set h = Tau (X,R,BASSIGN);
(TransEU (f,g)) . X = SigFoaxTau (g,f,X,R,BASSIGN) by Def73
.= (SIGMA g) \/ (SIGMA (Fax (f,(Tau (X,R,BASSIGN))))) by Th33
.= (SIGMA g) \/ ((SIGMA f) /\ (SIGMA (EX (Tau (X,R,BASSIGN))))) by Th33
.= (SIGMA g) \/ ((SIGMA f) /\ (Pred ((SIGMA (Tau (X,R,BASSIGN))),R))) by Th50 ;
hence (TransEU (f,g)) . X = (SIGMA g) \/ ((SIGMA f) /\ (Pred (X,R))) by Th32; :: thesis: verum