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 -polytopes p holds (c + d) @ x = (c @ x) + (d @ x)
let k be Integer; :: thesis: for c, d being Element of (k -chain-space p)
for x being Element of k -polytopes p holds (c + d) @ x = (c @ x) + (d @ x)
let c, d be Element of (k -chain-space p); :: thesis: for x being Element of k -polytopes p holds (c + d) @ x = (c @ x) + (d @ x)
let x be Element of k -polytopes p; :: thesis: (c + d) @ x = (c @ x) + (d @ x)
c + d = c \+\ d by BSPACE:def 5;
hence (c + d) @ x = (c @ x) + (d @ x) by BSPACE:15; :: thesis: verum