let L be FinSequence; :: thesis: for H, F 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 H, F 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)
F in {F} by TARSKI:def 1;
then A4: F in W1 by A3, XBOOLE_0:def 3;
W1 \ {F} = W

proof

B1: for x being set st x in W1 \ {F} holds
x in W

proof

let x be set ; :: 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 set st x in W holds
x in W1 \ {F}

proof

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

end;

hence W1 \ {F} = W by B1, TARSKI:2; :: thesis: verum

end;

then len L,W = (len L,W1) - (len F) by Thlen02, A1, A4;
hence len L,W1 = (len L,W) + (len F) ; :: thesis: verum