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