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