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) )
assume A2: n < (dim p) + 2 ; :: thesis: (alternating-f-vector p) . n = (alternating-proper-f-vector p) . (n - 1)
set acs = alternating-f-vector p;
set apcs = alternating-proper-f-vector p;
A3: (alternating-f-vector p) . n = ((- 1) |^ n) * (num-polytopes p,(n - 2)) by A1, A2, Def26;
0 <= n - 1

proof

1 - 1 = 0 ;
hence 0 <= n - 1 by A1, XREAL_1:15; :: thesis: verum

end;

then reconsider m = n - 1 as Element of NAT by INT_1:16;
reconsider m = m as Nat ;
A4: 1 <= m

proof

A5: 2 <= n

proof

1 + 1 = 2 ;
hence 2 <= n by A1, INT_1:20; :: thesis: verum

end;

2 - 1 = 1 ;
hence 1 <= m by A5, XREAL_1:15; :: thesis: verum

end;

m <= dim p

proof

n < ((dim p) + 1) + 1 by A2;
then n <= (dim p) + 1 by NAT_1:13;
then n - 1 <= ((dim p) + 1) - 1 by XREAL_1:11;
hence m <= dim p ; :: thesis: verum

end;

then (alternating-proper-f-vector p) . m = ((- 1) |^ (m + 1)) * (num-polytopes p,(m - 1)) by A4, Def27;
hence (alternating-f-vector p) . n = (alternating-proper-f-vector p) . (n - 1) by A3; :: thesis: verum