theorem :: CHAIN_1:56

for d being non zero Nat
for G being Grating of d holds
( Omega G = (0_ (d,G)) ` & 0_ (d,G) = (Omega G) ` )