let k be Nat; :: thesis: for d being non zero 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 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)

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 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 :: thesis: for A being Cell of k,G holds

( A in del (C1 + C2) iff A in (del C1) + (del C2) )

hence
del (C1 + C2) = (del C1) + (del C2)
by SUBSET_1:3; :: thesis: verum( A in del (C1 + C2) iff A in (del C1) + (del C2) )

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;

A2: ( A in del (C1 + C2) iff ( k + 1 <= d & card ((star A) /\ (C1 \+\ C2)) is odd ) ) by Th48;

A3: ( A in del C1 iff ( k + 1 <= d & card ((star A) /\ C1) is odd ) ) by Th48;

( A in del C2 iff ( k + 1 <= d & card ((star A) /\ C2) is odd ) ) by Th48;

hence ( A in del (C1 + C2) iff A in (del C1) + (del C2) ) by A1, A2, A3, Th7, XBOOLE_0:1; :: thesis: verum

end;A1: (star A) /\ (C1 \+\ C2) = ((star A) /\ C1) \+\ ((star A) /\ C2) by XBOOLE_1:112;

A2: ( A in del (C1 + C2) iff ( k + 1 <= d & card ((star A) /\ (C1 \+\ C2)) is odd ) ) by Th48;

A3: ( A in del C1 iff ( k + 1 <= d & card ((star A) /\ C1) is odd ) ) by Th48;

( A in del C2 iff ( k + 1 <= d & card ((star A) /\ C2) is odd ) ) by Th48;

hence ( A in del (C1 + C2) iff A in (del C1) + (del C2) ) by A1, A2, A3, Th7, XBOOLE_0:1; :: thesis: verum