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 incidence-sequence (x,(c + d)) = (incidence-sequence (x,c)) + (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 incidence-sequence (x,(c + d)) = (incidence-sequence (x,c)) + (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 incidence-sequence (x,(c + d)) = (incidence-sequence (x,c)) + (incidence-sequence (x,d))
let x be Element of (k - 1) -polytopes p; :: thesis: incidence-sequence (x,(c + d)) = (incidence-sequence (x,c)) + (incidence-sequence (x,d))
set n = num-polytopes (p,k);
set l = incidence-sequence (x,(c + d));
set isc = incidence-sequence (x,c);
set isd = incidence-sequence (x,d);
set r = (incidence-sequence (x,c)) + (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: incidence-sequence (x,(c + d)) = (incidence-sequence (x,c)) + (incidence-sequence (x,d))

then incidence-sequence (x,d) is Tuple of 0 , 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;
isc + isd is Element of 0 -tuples_on the carrier of Z_2 ;
hence incidence-sequence (x,(c + d)) = (incidence-sequence (x,c)) + (incidence-sequence (x,d)) by A1, Def16; :: thesis: verum

end;

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

A3: ( len (incidence-sequence (x,(c + d))) = num-polytopes (p,k) & len ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) = num-polytopes (p,k) )

proof

len (incidence-sequence (x,d)) = num-polytopes (p,k) by A2, Def16;
then reconsider isd = incidence-sequence (x,d) as Element of (num-polytopes (p,k)) -tuples_on the carrier of Z_2 by FINSEQ_2:92;
len (incidence-sequence (x,c)) = num-polytopes (p,k) by A2, Def16;
then reconsider isc = incidence-sequence (x,c) as Element of (num-polytopes (p,k)) -tuples_on the carrier of Z_2 by FINSEQ_2:92;
reconsider s = isc + isd as Element of (num-polytopes (p,k)) -tuples_on the carrier of Z_2 ;
len s = num-polytopes (p,k) by CARD_1:def 7;
hence ( len (incidence-sequence (x,(c + d))) = num-polytopes (p,k) & len ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) = num-polytopes (p,k) ) by A2, Def16; :: thesis: verum

end;

for n being Nat st 1 <= n & n <= len (incidence-sequence (x,(c + d))) holds
(incidence-sequence (x,(c + d))) . n = ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) . n

proof

A4: ( dom ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) = Seg (num-polytopes (p,k)) & len (incidence-sequence (x,(c + d))) = num-polytopes (p,k) ) by A3, FINSEQ_1:def 3;
let m be Nat; :: thesis: ( 1 <= m & m <= len (incidence-sequence (x,(c + d))) implies (incidence-sequence (x,(c + d))) . m = ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) . m )
assume A5: ( 1 <= m & m <= len (incidence-sequence (x,(c + d))) ) ; :: thesis: (incidence-sequence (x,(c + d))) . m = ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) . m
set a = m -th-polytope (p,k);
set iva = incidence-value (x,(m -th-polytope (p,k)));
A6: len (incidence-sequence (x,(c + d))) = num-polytopes (p,k) by A2, Def16;
then A7: (incidence-sequence (x,(c + d))) . m = ((c + d) @ (m -th-polytope (p,k))) * (incidence-value (x,(m -th-polytope (p,k)))) by A2, A5, Def16;
A8: m in dom ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) by A4, A5;
( (incidence-sequence (x,c)) . m = (c @ (m -th-polytope (p,k))) * (incidence-value (x,(m -th-polytope (p,k)))) & (incidence-sequence (x,d)) . m = (d @ (m -th-polytope (p,k))) * (incidence-value (x,(m -th-polytope (p,k)))) ) by A2, A5, A6, Def16;
then ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) . m = ((c @ (m -th-polytope (p,k))) * (incidence-value (x,(m -th-polytope (p,k))))) + ((d @ (m -th-polytope (p,k))) * (incidence-value (x,(m -th-polytope (p,k))))) by A8, FVSUM_1:17
.= ((c @ (m -th-polytope (p,k))) + (d @ (m -th-polytope (p,k)))) * (incidence-value (x,(m -th-polytope (p,k)))) by VECTSP_1:def 3
.= (incidence-sequence (x,(c + d))) . m by A7, Th35 ;
hence (incidence-sequence (x,(c + d))) . m = ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) . m ; :: thesis: verum

end;

hence incidence-sequence (x,(c + d)) = (incidence-sequence (x,c)) + (incidence-sequence (x,d)) by A3; :: thesis: verum

end;

end;