consider L being FinSequence such that
A1: ( rng L = Subformulae H & L is one-to-one ) by FINSEQ_4:73;
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