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