let p be polyhedron; :: thesis: for k being Integer
for c being Element of (k -chain-space p)
for a being Element of Z_2
for x being Element of (k - 1) -polytopes p holds incidence-sequence x,(a * c) = a * (incidence-sequence x,c)
let k be Integer; :: thesis: for c being Element of (k -chain-space p)
for a being Element of Z_2
for x being Element of (k - 1) -polytopes p holds incidence-sequence x,(a * c) = a * (incidence-sequence x,c)
let c be Element of (k -chain-space p); :: thesis: for a being Element of Z_2
for x being Element of (k - 1) -polytopes p holds incidence-sequence x,(a * c) = a * (incidence-sequence x,c)
let a be Element of Z_2 ; :: thesis: for x being Element of (k - 1) -polytopes p holds incidence-sequence x,(a * c) = a * (incidence-sequence x,c)
let x be Element of (k - 1) -polytopes p; :: thesis: incidence-sequence x,(a * c) = a * (incidence-sequence x,c)
set l = incidence-sequence x,(a * c);
set isc = incidence-sequence x,c;
set r = a * (incidence-sequence x,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: incidence-sequence x,(a * c) = a * (incidence-sequence x,c)

then incidence-sequence x,c = <*> the carrier of Z_2 by Def16;
then reconsider isc = incidence-sequence x,c as Element of 0 -tuples_on the carrier of Z_2 by FINSEQ_2:151;
a * isc is Element of 0 -tuples_on the carrier of Z_2 ;
then reconsider r = a * (incidence-sequence x,c) as Element of 0 -tuples_on the carrier of Z_2 ;
r = <*> the carrier of Z_2 ;
hence incidence-sequence x,(a * c) = a * (incidence-sequence x,c) by A1, Def16; :: thesis: verum

end;

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

set n = num-polytopes p,k;
A3: ( len (incidence-sequence x,(a * c)) = num-polytopes p,k & len (a * (incidence-sequence x,c)) = num-polytopes p,k )

proof

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:110;
set r = a * isc;
reconsider r = a * isc as Element of (num-polytopes p,k) -tuples_on the carrier of Z_2 ;
len r = num-polytopes p,k by FINSEQ_1:def 18;
hence ( len (incidence-sequence x,(a * c)) = num-polytopes p,k & len (a * (incidence-sequence x,c)) = num-polytopes p,k ) by A2, Def16; :: thesis: verum

end;

for m being Nat st 1 <= m & m <= len (incidence-sequence x,(a * c)) holds
(incidence-sequence x,(a * c)) . m = (a * (incidence-sequence x,c)) . m

proof

A4: dom (a * (incidence-sequence x,c)) = Seg (num-polytopes p,k) by A3, FINSEQ_1:def 3;
let m be Nat; :: thesis: ( 1 <= m & m <= len (incidence-sequence x,(a * c)) implies (incidence-sequence x,(a * c)) . m = (a * (incidence-sequence x,c)) . m )
assume A5: ( 1 <= m & m <= len (incidence-sequence x,(a * c)) ) ; :: thesis: (incidence-sequence x,(a * c)) . m = (a * (incidence-sequence x,c)) . m
set s = m -th-polytope p,k;
set ivs = incidence-value x,(m -th-polytope p,k);
A6: len (incidence-sequence x,(a * c)) = num-polytopes p,k by A2, Def16;
then A7: (incidence-sequence x,(a * c)) . m = ((a * c) @ (m -th-polytope p,k)) * (incidence-value x,(m -th-polytope p,k)) by A2, A5, Def16;
( len (incidence-sequence x,(a * c)) = num-polytopes p,k & m in NAT ) by A2, Def16, ORDINAL1:def 13;
then A8: m in Seg (num-polytopes p,k) by A5;
(incidence-sequence x,c) . m = (c @ (m -th-polytope p,k)) * (incidence-value x,(m -th-polytope p,k)) by A2, A5, A6, Def16;
then (a * (incidence-sequence x,c)) . m = a * ((c @ (m -th-polytope p,k)) * (incidence-value x,(m -th-polytope p,k))) by A4, A8, FVSUM_1:62
.= (a * (c @ (m -th-polytope p,k))) * (incidence-value x,(m -th-polytope p,k)) by GROUP_1:def 4
.= (incidence-sequence x,(a * c)) . m by A7, Th42 ;
hence (incidence-sequence x,(a * c)) . m = (a * (incidence-sequence x,c)) . m ; :: thesis: verum

end;

hence incidence-sequence x,(a * c) = a * (incidence-sequence x,c) by A3, FINSEQ_1:18; :: thesis: verum

end;

end;