let d9 be Nat; :: thesis: for G being Grating of d9 + 1
for C being Chain of (d9 + 1),G holds del (C `) = del C
let G be Grating of d9 + 1; :: thesis: for C being Chain of (d9 + 1),G holds del (C `) = del C
let C be Chain of (d9 + 1),G; :: thesis: del (C `) = del C
thus del (C `) = del (C + (Omega G)) by Th55
.= (del C) + (del (Omega G)) by Th58
.= (del C) + (0_ (d9,G)) by Th57
.= del C ; :: thesis: verum