let p be polyhedron; :: thesis: for k being Integer
for c being Element of (k -chain-space p)
for x being Element of (k - 1) -polytopes p holds (Boundary c) @ x = Sum (incidence-sequence (x,c))
let k be Integer; :: thesis: for c being Element of (k -chain-space p)
for x being Element of (k - 1) -polytopes p holds (Boundary c) @ x = Sum (incidence-sequence (x,c))
let c be Element of (k -chain-space p); :: thesis: for x being Element of (k - 1) -polytopes p holds (Boundary c) @ x = Sum (incidence-sequence (x,c))
let x be Element of (k - 1) -polytopes p; :: thesis: (Boundary c) @ x = Sum (incidence-sequence (x,c))
set b = Boundary c;

per cases ( (k - 1) -polytopes p is empty or not (k - 1) -polytopes p is empty ) ;

suppose A1: (k - 1) -polytopes p is empty ; :: thesis: (Boundary c) @ x = Sum (incidence-sequence (x,c))

set iscx = incidence-sequence (x,c);
incidence-sequence (x,c) = <*> the carrier of Z_2 by A1, Def16;
then A2: Sum (incidence-sequence (x,c)) = 0. Z_2 by RLVECT_1:43;
Boundary c = 0. ((k - 1) -chain-space p) by A1;
hence (Boundary c) @ x = Sum (incidence-sequence (x,c)) by A2, BSPACE:14; :: thesis: verum

end;

suppose A3: not (k - 1) -polytopes p is empty ; :: thesis: (Boundary c) @ x = Sum (incidence-sequence (x,c))

then A4: ( x in Boundary c iff Sum (incidence-sequence (x,c)) = 1. Z_2 ) by Def17;

per cases ( x in Boundary c or not x in Boundary c ) ;

suppose x in Boundary c ; :: thesis: (Boundary c) @ x = Sum (incidence-sequence (x,c))

hence (Boundary c) @ x = Sum (incidence-sequence (x,c)) by A4, BSPACE:def 3; :: thesis: verum

end;

suppose A5: not x in Boundary c ; :: thesis: (Boundary c) @ x = Sum (incidence-sequence (x,c))

then Sum (incidence-sequence (x,c)) <> 1. Z_2 by A3, Def17;
then Sum (incidence-sequence (x,c)) = 0. Z_2 by BSPACE:8;
hence (Boundary c) @ x = Sum (incidence-sequence (x,c)) by A5, BSPACE:def 3; :: thesis: verum

end;

end;

end;

end;