let d' be Element of NAT ; :: thesis: for G being Grating of d' + 1
for C being Chain of (d' + 1),G holds del (C ` ) = del C
let G be Grating of d' + 1; :: thesis: for C being Chain of (d' + 1),G holds del (C ` ) = del C
let C be Chain of (d' + 1),G; :: thesis: del (C ` ) = del C
thus del (C ` ) = del (C + (Omega G)) by Th60
.= (del C) + (del (Omega G)) by Th63
.= (del C) + (0_ d',G) by Th62
.= del C ; :: thesis: verum