a,b:
, e:({a..b
}
). b
a 
(
i:{a..b}. e(i)) = 1 a,b:, e:({a..b}). ba ( i:{a..b}. e(i)) = 1| By: |
Thm* f:(AAA), u:A, a,b:, e:({a..b}A).
Thm* b a (Iter(f;u) i:{a..b}. e(i)) = u
Using:[A:= | f:=  x,y. x y | 1]
THEN Reduce Hyp:-1 |
None
About:
 |  |  |  |  |  |  |  |  |