for n being Nat
for R being commutative Ring holds
( (<%(0. R),(0. R),(1_ R)%> `^ n) . (2 * n) = 1_ R & ( for k being Nat st k <> 2 * n holds
(<%(0. R),(0. R),(1_ R)%> `^ n) . k = 0. R ) )