let L be FinSequence; 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; 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); ( 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}
; len (L,W1) = (len (L,W)) + (len F)
A4:
for x being object st x in W1 \ {F} holds
x in W
for x being object st x in W holds
x in W1 \ {F}
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)
; verum