set F = the PolytopsF of p;
let s, t be FinSequence; :: thesis: ( ( k < - 1 implies s = <*> {} ) & ( k = - 1 implies s = <*{}*> ) & ( - 1 < k & k < dim p implies s = the PolytopsF of p . (k + 1) ) & ( k = dim p implies s = <*p*> ) & ( k > dim p implies s = <*> {} ) & ( k < - 1 implies t = <*> {} ) & ( k = - 1 implies t = <*{}*> ) & ( - 1 < k & k < dim p implies t = the PolytopsF of p . (k + 1) ) & ( k = dim p implies t = <*p*> ) & ( k > dim p implies t = <*> {} ) implies s = t )
assume that
A6: ( k < - 1 implies s = <*> {} ) and
A7: ( k = - 1 implies s = <*{}*> ) and
A8: ( - 1 < k & k < dim p implies s = the PolytopsF of p . (k + 1) ) and
A9: ( k = dim p implies s = <*p*> ) and
A10: ( k > dim p implies s = <*> {} ) and
A11: ( k < - 1 implies t = <*> {} ) and
A12: ( k = - 1 implies t = <*{}*> ) and
A13: ( - 1 < k & k < dim p implies t = the PolytopsF of p . (k + 1) ) and
A14: ( k = dim p implies t = <*p*> ) and
A15: ( k > dim p implies t = <*> {} ) ; :: thesis: s = t
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 k < - 1 ; :: thesis: s = t
hence s = t by A6, A11; :: thesis: verum
end;
suppose k = - 1 ; :: thesis: s = t
hence s = t by A7, A12; :: thesis: verum
end;
suppose ( - 1 < k & k < dim p ) ; :: thesis: s = t
hence s = t by A8, A13; :: thesis: verum
end;
suppose k = dim p ; :: thesis: s = t
hence s = t by A9, A14; :: thesis: verum
end;
suppose k > dim p ; :: thesis: s = t
hence s = t by A10, A15; :: thesis: verum
end;
end;