let a be non zero Nat; :: thesis: for b being odd Nat holds 2 |-count (a * b) = 2 |-count a
let b be odd Nat; :: thesis: 2 |-count (a * b) = 2 |-count a
2 |-count (a * b) = (2 |-count a) + (2 |-count b) by INT_2:28, NAT_3:28
.= (2 |-count a) + 0 ;
hence 2 |-count (a * b) = 2 |-count a ; :: thesis: verum