for A, B being Nat holds B = (A * (Fusc 0)) + (B * (Fusc 1)) by Th15;