let d be non zero Nat; :: thesis: for G being Grating of d holds
( Omega G = (0_ (d,G)) ` & 0_ (d,G) = (Omega G) ` )
let G be Grating of d; :: thesis: ( Omega G = (0_ (d,G)) ` & 0_ (d,G) = (Omega G) ` )
Omega G = (0_ (d,G)) ` ;
hence ( Omega G = (0_ (d,G)) ` & 0_ (d,G) = (Omega G) ` ) ; :: thesis: verum