let k be Element of NAT ; :: thesis: for d being non zero Element of NAT
for G being Grating of d
for C1, C2 being Chain of (k + 1),G holds del (C1 + C2) = (del C1) + (del C2)
let d be non zero Element of NAT ; :: thesis: for G being Grating of d
for C1, C2 being Chain of (k + 1),G holds del (C1 + C2) = (del C1) + (del C2)
let G be Grating of d; :: thesis: for C1, C2 being Chain of (k + 1),G holds del (C1 + C2) = (del C1) + (del C2)
let C1, C2 be Chain of (k + 1),G; :: thesis: del (C1 + C2) = (del C1) + (del C2)

now

let A be Cell of k,G; :: thesis: ( A in del (C1 + C2) iff A in (del C1) + (del C2) )
A1: (star A) /\ (C1 \+\ C2) = ((star A) /\ C1) \+\ ((star A) /\ C2) by XBOOLE_1:112;
( ( A in del (C1 + C2) implies ( k + 1 <= d & not card ((star A) /\ (C1 \+\ C2)) is even ) ) & ( k + 1 <= d & not card ((star A) /\ (C1 \+\ C2)) is even implies A in del (C1 + C2) ) & ( A in del C1 implies ( k + 1 <= d & not card ((star A) /\ C1) is even ) ) & ( k + 1 <= d & not card ((star A) /\ C1) is even implies A in del C1 ) & ( A in del C2 implies ( k + 1 <= d & not card ((star A) /\ C2) is even ) ) & ( k + 1 <= d & not card ((star A) /\ C2) is even implies A in del C2 ) ) by Th52;
hence ( A in del (C1 + C2) iff A in (del C1) + (del C2) ) by A1, Th9, XBOOLE_0:1; :: thesis: verum

end;

hence del (C1 + C2) = (del C1) + (del C2) by SUBSET_1:8; :: thesis: verum