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: ex b₁ being FinSequence of Z_2 st
( ( (k - 1) -polytopes p is empty implies b₁ = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len b₁ = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
b₁ . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) )

set s = <*> {};
rng (<*> {}) c= the carrier of Z_2 ;
then reconsider s = <*> {} as FinSequence of Z_2 by FINSEQ_1:def 4;
take s ; :: thesis: ( ( (k - 1) -polytopes p is empty implies s = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len s = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
s . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) )
thus ( ( (k - 1) -polytopes p is empty implies s = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len s = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
s . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) ) by A1; :: thesis: verum

end;

suppose A2: not (k - 1) -polytopes p is empty ; :: thesis: ex b₁ being FinSequence of Z_2 st
( ( (k - 1) -polytopes p is empty implies b₁ = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len b₁ = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
b₁ . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) )

deffunc H₁( Nat) -> Element of the carrier of Z_2 = (v @ ($1 -th-polytope (p,k))) * (incidence-value (x,($1 -th-polytope (p,k))));
consider s being FinSequence of Z_2 such that
A3: len s = num-polytopes (p,k) and
A4: for n being Nat st n in dom s holds
s . n = H₁(n) from FINSEQ_2:sch 1();
take s ; :: thesis: ( ( (k - 1) -polytopes p is empty implies s = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len s = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
s . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) )
A5: dom s = Seg (num-polytopes (p,k)) by A3, FINSEQ_1:def 3;
for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
s . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k))))

proof

let n be Nat; :: thesis: ( 1 <= n & n <= num-polytopes (p,k) implies s . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) )
assume ( 1 <= n & n <= num-polytopes (p,k) ) ; :: thesis: s . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k))))
then n in Seg (num-polytopes (p,k)) ;
hence s . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) by A4, A5; :: thesis: verum

end;

hence ( ( (k - 1) -polytopes p is empty implies s = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len s = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
s . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) ) by A2, A3; :: thesis: verum

end;

end;