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