let F, H be LTL-formula; :: thesis: for W, W1 being Subset of (Subformulae H) st not F in W & W1 = W \/ {F} holds
len W1 = (len W) + (len F)
let W, W1 be Subset of (Subformulae H); :: thesis: ( not F in W & W1 = W \/ {F} implies len W1 = (len W) + (len F) )
assume A1: ( not F in W & W1 = W \/ {F} ) ; :: thesis: len W1 = (len W) + (len F)
consider L being FinSequence such that
A2: ( rng L = Subformulae H & L is one-to-one ) by FINSEQ_4:58;
len W1 = len (L,W1) by A2, Def26
.= (len (L,W)) + (len F) by A1, A2, Th7 ;
hence len W1 = (len W) + (len F) by A2, Def26; :: thesis: verum