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 Th46;
( (Boundary (c + d)) @ x = Sum (incidence-sequence x,(c + d)) & ((Boundary c) + (Boundary d)) @ x = ((Boundary c) @ x) + ((Boundary d) @ x) ) by Th38, Th46;
hence (Boundary (c + d)) @ x = ((Boundary c) + (Boundary d)) @ x by A1, Th41; :: thesis: verum

end;

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