let S be non empty set ; :: thesis: for R being total Relation of S,S ex o being UnOp of (ModelSP S) st
for f being set st f in ModelSP S holds
o . f = EneXt_0 f,R
let R be total Relation of S,S; :: thesis: ex o being UnOp of (ModelSP S) st
for f being set st f in ModelSP S holds
o . f = EneXt_0 f,R
set M = ModelSP S;
deffunc H₁( set ) -> Element of ModelSP S = EneXt_0 $1,R;
ex o being UnOp of (ModelSP S) st
for f being set st f in ModelSP S holds
o . f = H₁(f) from MODELC_1:sch 4();
hence ex o being UnOp of (ModelSP S) st
for f being set st f in ModelSP S holds
o . f = EneXt_0 f,R ; :: thesis: verum