let p be polyhedron; :: thesis: for k being Integer holds k -boundary p is linear-transformation of (k -chain-space p),((k - 1) -chain-space p)
let k be Integer; :: thesis: k -boundary p is linear-transformation of (k -chain-space p),((k - 1) -chain-space p)
set V = k -chain-space p;
set b = k -boundary p;
A1: for a being Element of Z_2
for x being Element of (k -chain-space p) holds (k -boundary p) . (a * x) = a * ((k -boundary p) . x)

proof

let a be Element of Z_2; :: thesis: for x being Element of (k -chain-space p) holds (k -boundary p) . (a * x) = a * ((k -boundary p) . x)
let x be Element of (k -chain-space p); :: thesis: (k -boundary p) . (a * x) = a * ((k -boundary p) . x)
(k -boundary p) . (a * x) = Boundary (a * x) by Def18
.= a * (Boundary x) by Th45
.= a * ((k -boundary p) . x) by Def18 ;
hence (k -boundary p) . (a * x) = a * ((k -boundary p) . x) ; :: thesis: verum

end;

for x, y being Element of (k -chain-space p) holds (k -boundary p) . (x + y) = ((k -boundary p) . x) + ((k -boundary p) . y)

proof

let x, y be Element of (k -chain-space p); :: thesis: (k -boundary p) . (x + y) = ((k -boundary p) . x) + ((k -boundary p) . y)
(k -boundary p) . (x + y) = Boundary (x + y) by Def18
.= (Boundary x) + (Boundary y) by Th44
.= ((k -boundary p) . x) + (Boundary y) by Def18
.= ((k -boundary p) . x) + ((k -boundary p) . y) by Def18 ;
hence (k -boundary p) . (x + y) = ((k -boundary p) . x) + ((k -boundary p) . y) ; :: thesis: verum

end;

then ( k -boundary p is additive & k -boundary p is homogeneous ) by A1, MOD_2:def 2, VECTSP_1:def 20;
hence k -boundary p is linear-transformation of (k -chain-space p),((k - 1) -chain-space p) ; :: thesis: verum