consider L being FinSequence such that
A1: ( rng L = Subformulae H & L is one-to-one ) by FINSEQ_4:58;
set IT = len (L,W);
take len (L,W) ; :: thesis: ex L being FinSequence st
( rng L = Subformulae H & L is one-to-one & len (L,W) = len (L,W) )
thus ex L being FinSequence st
( rng L = Subformulae H & L is one-to-one & len (L,W) = len (L,W) ) by A1; :: thesis: verum