set F = the PolytopsF of p;

per cases ( k < - 1 or k = - 1 or ( - 1 < k & k < dim p ) or k = dim p or k > dim p ) by XXREAL_0:1;

suppose A1: k < - 1 ; :: thesis: ex b₁ being finite set st
( ( k < - 1 implies b₁ = {} ) & ( k = - 1 implies b₁ = {{}} ) & ( - 1 < k & k < dim p implies b₁ = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies b₁ = {p} ) & ( k > dim p implies b₁ = {} ) )

take {} ; :: thesis: ( ( k < - 1 implies {} = {} ) & ( k = - 1 implies {} = {{}} ) & ( - 1 < k & k < dim p implies {} = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies {} = {p} ) & ( k > dim p implies {} = {} ) )
thus ( ( k < - 1 implies {} = {} ) & ( k = - 1 implies {} = {{}} ) & ( - 1 < k & k < dim p implies {} = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies {} = {p} ) & ( k > dim p implies {} = {} ) ) by A1; :: thesis: verum

end;

suppose A2: k = - 1 ; :: thesis: ex b₁ being finite set st
( ( k < - 1 implies b₁ = {} ) & ( k = - 1 implies b₁ = {{}} ) & ( - 1 < k & k < dim p implies b₁ = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies b₁ = {p} ) & ( k > dim p implies b₁ = {} ) )

take {{}} ; :: thesis: ( ( k < - 1 implies {{}} = {} ) & ( k = - 1 implies {{}} = {{}} ) & ( - 1 < k & k < dim p implies {{}} = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies {{}} = {p} ) & ( k > dim p implies {{}} = {} ) )
thus ( ( k < - 1 implies {{}} = {} ) & ( k = - 1 implies {{}} = {{}} ) & ( - 1 < k & k < dim p implies {{}} = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies {{}} = {p} ) & ( k > dim p implies {{}} = {} ) ) by A2; :: thesis: verum

end;

suppose A3: ( - 1 < k & k < dim p ) ; :: thesis: ex b₁ being finite set st
( ( k < - 1 implies b₁ = {} ) & ( k = - 1 implies b₁ = {{}} ) & ( - 1 < k & k < dim p implies b₁ = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies b₁ = {p} ) & ( k > dim p implies b₁ = {} ) )

(- 1) + 1 = 0 ;
then 0 <= k by A3, INT_1:7;
then reconsider k = k as Element of NAT by INT_1:3;
set n = k + 1;
reconsider Fn = the PolytopsF of p . (k + 1) as FinSequence ;
take rng Fn ; :: thesis: ( ( k < - 1 implies rng Fn = {} ) & ( k = - 1 implies rng Fn = {{}} ) & ( - 1 < k & k < dim p implies rng Fn = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies rng Fn = {p} ) & ( k > dim p implies rng Fn = {} ) )
thus ( ( k < - 1 implies rng Fn = {} ) & ( k = - 1 implies rng Fn = {{}} ) & ( - 1 < k & k < dim p implies rng Fn = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies rng Fn = {p} ) & ( k > dim p implies rng Fn = {} ) ) by A3; :: thesis: verum

end;

suppose A4: k = dim p ; :: thesis: ex b₁ being finite set st
( ( k < - 1 implies b₁ = {} ) & ( k = - 1 implies b₁ = {{}} ) & ( - 1 < k & k < dim p implies b₁ = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies b₁ = {p} ) & ( k > dim p implies b₁ = {} ) )

take {p} ; :: thesis: ( ( k < - 1 implies {p} = {} ) & ( k = - 1 implies {p} = {{}} ) & ( - 1 < k & k < dim p implies {p} = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies {p} = {p} ) & ( k > dim p implies {p} = {} ) )
thus ( ( k < - 1 implies {p} = {} ) & ( k = - 1 implies {p} = {{}} ) & ( - 1 < k & k < dim p implies {p} = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies {p} = {p} ) & ( k > dim p implies {p} = {} ) ) by A4; :: thesis: verum

end;

suppose A5: k > dim p ; :: thesis: ex b₁ being finite set st
( ( k < - 1 implies b₁ = {} ) & ( k = - 1 implies b₁ = {{}} ) & ( - 1 < k & k < dim p implies b₁ = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies b₁ = {p} ) & ( k > dim p implies b₁ = {} ) )

take {} ; :: thesis: ( ( k < - 1 implies {} = {} ) & ( k = - 1 implies {} = {{}} ) & ( - 1 < k & k < dim p implies {} = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies {} = {p} ) & ( k > dim p implies {} = {} ) )
thus ( ( k < - 1 implies {} = {} ) & ( k = - 1 implies {} = {{}} ) & ( - 1 < k & k < dim p implies {} = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies {} = {p} ) & ( k > dim p implies {} = {} ) ) by A5; :: thesis: verum

end;

end;