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 FinSequence st
( ( k < - 1 implies b₁ = <*> {} ) & ( k = - 1 implies b₁ = <*{}*> ) & ( - 1 < k & k < dim p implies b₁ = 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 <*> {} = 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 <*> {} = 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 FinSequence st
( ( k < - 1 implies b₁ = <*> {} ) & ( k = - 1 implies b₁ = <*{}*> ) & ( - 1 < k & k < dim p implies b₁ = 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 <*{}*> = 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 <*{}*> = 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 FinSequence st
( ( k < - 1 implies b₁ = <*> {} ) & ( k = - 1 implies b₁ = <*{}*> ) & ( - 1 < k & k < dim p implies b₁ = the PolytopsF of p . (k + 1) ) & ( k = dim p implies b₁ = <*p*> ) & ( k > dim p implies b₁ = <*> {} ) )

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

end;

suppose A4: k = dim p ; :: thesis: ex b₁ being FinSequence st
( ( k < - 1 implies b₁ = <*> {} ) & ( k = - 1 implies b₁ = <*{}*> ) & ( - 1 < k & k < dim p implies b₁ = 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*> = 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*> = 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 FinSequence st
( ( k < - 1 implies b₁ = <*> {} ) & ( k = - 1 implies b₁ = <*{}*> ) & ( - 1 < k & k < dim p implies b₁ = 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 <*> {} = 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 <*> {} = the PolytopsF of p . (k + 1) ) & ( k = dim p implies <*> {} = <*p*> ) & ( k > dim p implies <*> {} = <*> {} ) ) by A5; :: thesis: verum

end;

end;