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