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) by VECTSP_1:def 17; :: thesis: verum
end;
end;