for l being Nat holds
( 0 in dom (Goto l) & (Goto l) . 0 = goto l ) by Lm1;