let p be polyhedron; :: thesis: for n being Nat st 1 < n & n < (dim p) + 2 holds
(alternating-f-vector p) . n = (alternating-proper-f-vector p) . (n - 1)
let n be Nat; :: thesis: ( 1 < n & n < (dim p) + 2 implies (alternating-f-vector p) . n = (alternating-proper-f-vector p) . (n - 1) )
assume A1: 1 < n ; :: thesis: ( not n < (dim p) + 2 or (alternating-f-vector p) . n = (alternating-proper-f-vector p) . (n - 1) )
1 - 1 = 0 ;
then reconsider m = n - 1 as Element of NAT by A1, INT_1:3, XREAL_1:13;
reconsider m = m as Nat ;
set apcs = alternating-proper-f-vector p;
set acs = alternating-f-vector p;
A2: 2 - 1 = 1 ;
1 + 1 = 2 ;
then 2 <= n by A1, INT_1:7;
then A3: 1 <= m by A2, XREAL_1:13;
assume A4: n < (dim p) + 2 ; :: thesis: (alternating-f-vector p) . n = (alternating-proper-f-vector p) . (n - 1)
then n < ((dim p) + 1) + 1 ;
then n <= (dim p) + 1 by NAT_1:13;
then n - 1 <= ((dim p) + 1) - 1 by XREAL_1:9;
then A5: (alternating-proper-f-vector p) . m = ((- 1) |^ (m + 1)) * (num-polytopes (p,(m - 1))) by A3, Def27;
(alternating-f-vector p) . n = ((- 1) |^ n) * (num-polytopes (p,(n - 2))) by A1, A4, Def26;
hence (alternating-f-vector p) . n = (alternating-proper-f-vector p) . (n - 1) by A5; :: thesis: verum