for N, i being Nat st i in dom (Sgm0 (N /\ EvenNAT)) holds
(Sgm0 (N /\ EvenNAT)) . i = 2 * i