let p be polyhedron; :: thesis: for k being Integer
for c being Element of (k -chain-space p)
for a being Element of Z_2
for x being Element of k -polytopes p holds (a * c) @ x = a * (c @ x)
let k be Integer; :: thesis: for c being Element of (k -chain-space p)
for a being Element of Z_2
for x being Element of k -polytopes p holds (a * c) @ x = a * (c @ x)
let c be Element of (k -chain-space p); :: thesis: for a being Element of Z_2
for x being Element of k -polytopes p holds (a * c) @ x = a * (c @ x)
let a be Element of Z_2; :: thesis: for x being Element of k -polytopes p holds (a * c) @ x = a * (c @ x)
let x be Element of k -polytopes p; :: thesis: (a * c) @ x = a * (c @ x)

per cases ( a = 0. Z_2 or a = 1. Z_2 ) by BSPACE:8;

suppose a = 0. Z_2 ; :: thesis: (a * c) @ x = a * (c @ x)

then ( a * (c @ x) = 0. Z_2 & a * c = 0. (k -chain-space p) ) by VECTSP_1:14;
hence (a * c) @ x = a * (c @ x) by BSPACE:14; :: thesis: verum

end;

suppose a = 1. Z_2 ; :: thesis: (a * c) @ x = a * (c @ x)

hence (a * c) @ x = a * (c @ x) ; :: thesis: verum

end;

end;