let p be polyhedron; for k being Integer
for c, d being Element of (k -chain-space p)
for x being Element of (k - 1) -polytopes p holds Sum (incidence-sequence (x,(c + d))) = (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d)))
let k be Integer; for c, d being Element of (k -chain-space p)
for x being Element of (k - 1) -polytopes p holds Sum (incidence-sequence (x,(c + d))) = (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d)))
let c, d be Element of (k -chain-space p); for x being Element of (k - 1) -polytopes p holds Sum (incidence-sequence (x,(c + d))) = (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d)))
let x be Element of (k - 1) -polytopes p; Sum (incidence-sequence (x,(c + d))) = (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d)))
Sum (incidence-sequence (x,(c + d))) =
Sum ((incidence-sequence (x,c)) + (incidence-sequence (x,d)))
by Th36
.=
(Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d)))
by Th37
;
hence
Sum (incidence-sequence (x,(c + d))) = (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d)))
; verum