By: |
Thm* ![]() ![]() ![]() ![]() ![]() Thm* is_commutative_sep(A; f) Thm* ![]() ![]() Thm* is_ident(A; f; u) Thm* ![]() ![]() Thm* is_assoc_sep(A; f) Thm* ![]() ![]() Thm* ( ![]() ![]() ![]() ![]() ![]() Thm* (f((Iter(f;u) i:{a..b ![]() ![]() Thm* (= Thm* ((Iter(f;u) i:{a..b ![]() Thm* ( ![]() Using:[ ![]() ![]() |
1 |
![]() ![]() ![]() ![]() | 1 step |
2 |
![]() ![]() ![]() ![]() | 1 step |
3 |
![]() ![]() ![]() ![]() | 1 step |
4 |
![]() ![]() ![]() ![]() ![]() ![]() 1. ( ![]() ![]() ![]() ![]() ![]() 1. = 1. ( ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | 1 step |
About:
![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() |