let p be polyhedron; :: thesis: for k being Integer
for c, d being Element of (k -chain-space p) holds Boundary (c + d) = (Boundary c) + (Boundary d)
let k be Integer; :: thesis: for c, d being Element of (k -chain-space p) holds Boundary (c + d) = (Boundary c) + (Boundary d)
let c, d be Element of (k -chain-space p); :: thesis: Boundary (c + d) = (Boundary c) + (Boundary d)
set bc = Boundary c;
set bd = Boundary d;
set s = c + d;
set l = Boundary (c + d);
set r = (Boundary c) + (Boundary d);
for x being Element of (k - 1) -polytopes p holds (Boundary (c + d)) @ x = ((Boundary c) + (Boundary d)) @ x

proof

let x be Element of (k - 1) -polytopes p; :: thesis: (Boundary (c + d)) @ x = ((Boundary c) + (Boundary d)) @ x
set a = (Boundary c) @ x;
set b = (Boundary d) @ x;
A1: ( (Boundary c) @ x = Sum (incidence-sequence (x,c)) & (Boundary d) @ x = Sum (incidence-sequence (x,d)) ) by Th43;
( (Boundary (c + d)) @ x = Sum (incidence-sequence (x,(c + d))) & ((Boundary c) + (Boundary d)) @ x = ((Boundary c) @ x) + ((Boundary d) @ x) ) by Th35, Th43;
hence (Boundary (c + d)) @ x = ((Boundary c) + (Boundary d)) @ x by A1, Th38; :: thesis: verum

end;

hence Boundary (c + d) = (Boundary c) + (Boundary d) by Th41; :: thesis: verum