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 by XBOOLE_1: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();
A5: dom s = Seg (num-polytopes p,k) by A3, FINSEQ_1:def 3;
A6: 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 that
A7: 1 <= n and
A8: n <= num-polytopes p,k ; :: thesis: s . n = (v @ (n -th-polytope p,k)) * (incidence-value x,(n -th-polytope p,k))
A9: n in Seg (num-polytopes p,k) by A7, A8, FINSEQ_1:3;
thus s . n = (v @ (n -th-polytope p,k)) * (incidence-value x,(n -th-polytope p,k)) by A4, A9, A5; :: thesis: verum

end;

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 A2, A3, A6; :: thesis: verum

end;

end;