let d be non zero Element of NAT ; :: thesis: for G being Grating of d
for C being Cycle of d,G holds C ` is Cycle of d,G
let G be Grating of d; :: thesis: for C being Cycle of d,G holds C ` is Cycle of d,G
let C be Cycle of d,G; :: thesis: C ` is Cycle of d,G
consider d' being Nat such that
A1: d = d' + 1 by NAT_1:6;
reconsider d' = d' as Element of NAT by ORDINAL1:def 13;
reconsider G = G as Grating of d' + 1 by A1;
reconsider C = C as Cycle of d' + 1,G by A1;
del C = 0_ d',G ;
then del (C ` ) = 0_ d',G by Th64;
hence C ` is Cycle of d,G by A1, Th66; :: thesis: verum