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 - 1) -polytopes p holds Sum ((incidence-sequence x,c) + (incidence-sequence x,d)) = (Sum (incidence-sequence x,c)) + (Sum (incidence-sequence x,d))
let k be Integer; :: thesis: for c, d being Element of (k -chain-space p)
for x being Element of (k - 1) -polytopes p holds Sum ((incidence-sequence x,c) + (incidence-sequence x,d)) = (Sum (incidence-sequence x,c)) + (Sum (incidence-sequence x,d))
let c, d be Element of (k -chain-space p); :: thesis: for x being Element of (k - 1) -polytopes p holds Sum ((incidence-sequence x,c) + (incidence-sequence x,d)) = (Sum (incidence-sequence x,c)) + (Sum (incidence-sequence x,d))
let x be Element of (k - 1) -polytopes p; :: thesis: Sum ((incidence-sequence x,c) + (incidence-sequence x,d)) = (Sum (incidence-sequence x,c)) + (Sum (incidence-sequence x,d))
set isc = incidence-sequence x,c;
set isd = incidence-sequence x,d;

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: Sum ((incidence-sequence x,c) + (incidence-sequence x,d)) = (Sum (incidence-sequence x,c)) + (Sum (incidence-sequence x,d))

then incidence-sequence x,d = <*> the carrier of Z_2 by Def16;
then reconsider isd = incidence-sequence x,d as Element of 0 -tuples_on the carrier of Z_2 by FINSEQ_2:151;
incidence-sequence x,c = <*> the carrier of Z_2 by A1, Def16;
then reconsider isc = incidence-sequence x,c as Element of 0 -tuples_on the carrier of Z_2 by FINSEQ_2:151;
reconsider s = isc + isd as Element of 0 -tuples_on the carrier of Z_2 ;
Sum s = 0. Z_2 by FVSUM_1:93;
hence Sum ((incidence-sequence x,c) + (incidence-sequence x,d)) = (Sum (incidence-sequence x,c)) + (Sum (incidence-sequence x,d)) by RLVECT_1:def 7; :: thesis: verum

end;

suppose A2: not (k - 1) -polytopes p is empty ; :: thesis: Sum ((incidence-sequence x,c) + (incidence-sequence x,d)) = (Sum (incidence-sequence x,c)) + (Sum (incidence-sequence x,d))

reconsider n = num-polytopes p,k as Element of NAT ;
len (incidence-sequence x,d) = n by A2, Def16;
then reconsider isd9 = incidence-sequence x,d as Element of n -tuples_on the carrier of Z_2 by FINSEQ_2:110;
len (incidence-sequence x,c) = n by A2, Def16;
then reconsider isc9 = incidence-sequence x,c as Element of n -tuples_on the carrier of Z_2 by FINSEQ_2:110;
Sum ((incidence-sequence x,c) + (incidence-sequence x,d)) = Sum (isc9 + isd9)
.= (Sum (incidence-sequence x,c)) + (Sum (incidence-sequence x,d)) by FVSUM_1:95 ;
hence Sum ((incidence-sequence x,c) + (incidence-sequence x,d)) = (Sum (incidence-sequence x,c)) + (Sum (incidence-sequence x,d)) ; :: thesis: verum

end;

end;