let p be polyhedron; :: thesis: 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; :: thesis: 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); :: thesis: 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; :: thesis: 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))) ; :: thesis: verum