a,c,b:
, e:({a..b
}
).
Thm* a
c
Thm*
Thm* c<b
Thm*
Thm* (
i:{a..b}. e(i)) = ( i:{a..c}. e(i))+e(c)+( i:{c+1..b}. e(i))f:(AAA), u:A.
Thm* is_ident(A; f; u)
Thm*
Thm* is_assoc_sep(A; f)
Thm*
Thm* (
a,c,b:, e:({a..b}A).
Thm* (a
c
Thm* (
Thm* (c<b
Thm* (
Thm* ((Iter(f;u) i:{a..b
}. e(i))
Thm* (=
Thm* (f((Iter(f;u) i:{a..c
}. e(i)),f(e(c),Iter(f;u) i:{c+1..b}. e(i))))