let L be FinSequence; :: thesis: for F, H being LTL-formula
for W, W1 being Subset of (Subformulae H) st rng L = Subformulae H & L is one-to-one & not F in W & W1 = W \/ {F} holds
len (L,W1) = (len (L,W)) + (len F)
let F, H be LTL-formula; :: thesis: for W, W1 being Subset of (Subformulae H) st rng L = Subformulae H & L is one-to-one & not F in W & W1 = W \/ {F} holds
len (L,W1) = (len (L,W)) + (len F)
let W, W1 be Subset of (Subformulae H); :: thesis: ( rng L = Subformulae H & L is one-to-one & not F in W & W1 = W \/ {F} implies len (L,W1) = (len (L,W)) + (len F) )
assume that
A1: ( rng L = Subformulae H & L is one-to-one ) and
A2: not F in W and
A3: W1 = W \/ {F} ; :: thesis: len (L,W1) = (len (L,W)) + (len F)
A4: for x being object st x in W1 \ {F} holds
x in W

proof

let x be object ; :: thesis: ( x in W1 \ {F} implies x in W )
assume x in W1 \ {F} ; :: thesis: x in W
then ( x in W1 & not x in {F} ) by XBOOLE_0:def 5;
hence x in W by A3, XBOOLE_0:def 3; :: thesis: verum

end;

for x being object st x in W holds
x in W1 \ {F}

proof

let x be object ; :: thesis: ( x in W implies x in W1 \ {F} )
assume x in W ; :: thesis: x in W1 \ {F}
then ( not x in {F} & x in W1 ) by A2, A3, TARSKI:def 1, XBOOLE_0:def 3;
hence x in W1 \ {F} by XBOOLE_0:def 5; :: thesis: verum

end;

then A5: W1 \ {F} = W by A4, TARSKI:2;
F in {F} by TARSKI:def 1;
then F in W1 by A3, XBOOLE_0:def 3;
then len (L,W) = (len (L,W1)) - (len F) by A1, A5, Th6;
hence len (L,W1) = (len (L,W)) + (len F) ; :: thesis: verum