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:131;
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:131;
reconsider s = isc + isd as Element of 0 -tuples_on the carrier of Z_2 ;
Sum s = 0. Z_2 by FVSUM_1:74;
hence Sum ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) = (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d))) by RLVECT_1:def 4; :: 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:92;
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:92;
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:76 ;
hence Sum ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) = (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d))) ; :: thesis: verum
end;
end;