reconsider I = <*> {} as Function-yielding FinSequence ;
reconsider F = <*<*{}*>*> as FinSequence-yielding FinSequence ;
take p = PolyhedronStr(# F,I #); :: thesis: ( p is polyhedron_1 & p is polyhedron_2 & p is polyhedron_3 )
A1: len F = 1 by FINSEQ_1:39;
len I = 1 - 1 ;
hence p is polyhedron_1 by A1, Def1; :: thesis: ( p is polyhedron_2 & p is polyhedron_3 )
for n being Nat st 1 <= n & n < 1 holds
I . n is incidence-matrix of (rng (F . n)),(rng (F . (n + 1))) ;
hence p is polyhedron_2 by A1, Def2; :: thesis: p is polyhedron_3
let n be Nat; :: according to POLYFORM:def 3 :: thesis: ( 1 <= n & n <= len the PolytopsF of p implies ( not the PolytopsF of p . n is empty & the PolytopsF of p . n is one-to-one ) )
assume ( 1 <= n & n <= len the PolytopsF of p ) ; :: thesis: ( not the PolytopsF of p . n is empty & the PolytopsF of p . n is one-to-one )
then n = 1 by A1, XXREAL_0:1;
hence ( not the PolytopsF of p . n is empty & the PolytopsF of p . n is one-to-one ) by FINSEQ_1:def 8; :: thesis: verum