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;
thus p is polyhedron_1 by A1; :: thesis: ( p is polyhedron_2 & p is polyhedron_3 )
thus p is polyhedron_2 by A1; :: 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