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 Th39
.= (Sum (incidence-sequence x,c)) + (Sum (incidence-sequence x,d)) by Th40 ;
hence Sum (incidence-sequence x,(c + d)) = (Sum (incidence-sequence x,c)) + (Sum (incidence-sequence x,d)) ; :: thesis: verum