let a, b be non zero Nat; :: thesis: for n being non trivial Nat holds (a + b) |-count ((a |^ n) + (b |^ n)) < n
let n be non trivial Nat; :: thesis: (a + b) |-count ((a |^ n) + (b |^ n)) < n
reconsider m = n - 1 as non zero Nat ;
(a + b) |^ 1 = (a |^ 1) + (b |^ 1) ;
then (a + b) |^ (1 + m) > (a |^ (1 + m)) + (b |^ (1 + m)) by NEWTON01:18;
hence (a + b) |-count ((a |^ n) + (b |^ n)) < n by Count4; :: thesis: verum