let L be FinSequence; :: thesis: for H, F being LTL-formula
for W being Subset of (Subformulae H) st rng L = Subformulae H & L is one-to-one & F in W holds
len L,(W \ {F}) = (len L,W) - (len F)
let H, F be LTL-formula; :: thesis: for W being Subset of (Subformulae H) st rng L = Subformulae H & L is one-to-one & F in W holds
len L,(W \ {F}) = (len L,W) - (len F)
let W be Subset of (Subformulae H); :: thesis: ( rng L = Subformulae H & L is one-to-one & F in W implies len L,(W \ {F}) = (len L,W) - (len F) )
assume that
A1: ( rng L = Subformulae H & L is one-to-one ) and
A2: F in W ; :: thesis: len L,(W \ {F}) = (len L,W) - (len F)
set n = len L;
consider x being set such that
A3: x in dom L and
A4: L . x = F by A1, A2, FUNCT_1:def 5;
x in Seg (len L) by A3, FINSEQ_1:def 3;
then x in { k where k is Element of NAT : ( 1 <= k & k <= len L ) } by FINSEQ_1:def 1;
then consider k being Element of NAT such that
A5: ( x = k & 1 <= k & k <= len L ) ;
reconsider k = k as Nat ;
L . k in {F} by A4, A5, TARSKI:def 1;
then A7: not L . k in W \ {F} by XBOOLE_0:def 5;
set R1 = Partial_seq L,W;
set R2 = Partial_seq L,(W \ {F});
A801: F in LTL_WFF by MODELC_2:1;
A8: (Partial_seq L,W) . k = len (CastLTL (L . k)) by A4, A5, A2, DefPartialseq
.= len F by A801, A4, A5, MODELC_2:def 25 ;
A9: (Partial_seq L,(W \ {F})) . k = 0 by A7, DefPartialseq;
for i being Nat st i <= len L & not i = k holds
(Partial_seq L,W) . i = (Partial_seq L,(W \ {F})) . i

proof

let i be Nat; :: thesis: ( i <= len L & not i = k implies (Partial_seq L,W) . i = (Partial_seq L,(W \ {F})) . i )
assume B1: ( i <= len L & not i = k ) ; :: thesis: (Partial_seq L,W) . i = (Partial_seq L,(W \ {F})) . i

now

per cases ( not i in dom L or i in dom L ) ;

suppose not i in dom L ; :: thesis: (Partial_seq L,W) . i = (Partial_seq L,(W \ {F})) . i

then B401: L . i = {} by FUNCT_1:def 4;
then B4: not L . i in W by LemSubformulae04;
not L . i in W \ {F} by B401, LemSubformulae04;
then (Partial_seq L,(W \ {F})) . i = 0 by DefPartialseq
.= (Partial_seq L,W) . i by B4, DefPartialseq ;
hence (Partial_seq L,W) . i = (Partial_seq L,(W \ {F})) . i ; :: thesis: verum

end;

suppose i in dom L ; :: thesis: (Partial_seq L,W) . i = (Partial_seq L,(W \ {F})) . i

then not L . i = F by A1, A3, A4, A5, B1, FUNCT_1:def 8;
then B6: not L . i in {F} by TARSKI:def 1;

now

per cases ( L . i in W or not L . i in W ) ;

suppose C1: L . i in W ; :: thesis: (Partial_seq L,W) . i = (Partial_seq L,(W \ {F})) . i

then L . i in W \ {F} by B6, XBOOLE_0:def 5;
then (Partial_seq L,(W \ {F})) . i = len (CastLTL (L . i)) by DefPartialseq
.= (Partial_seq L,W) . i by C1, DefPartialseq ;
hence (Partial_seq L,W) . i = (Partial_seq L,(W \ {F})) . i ; :: thesis: verum

end;

suppose C2: not L . i in W ; :: thesis: (Partial_seq L,W) . i = (Partial_seq L,(W \ {F})) . i

then not L . i in W \ {F} by XBOOLE_0:def 5;
then (Partial_seq L,(W \ {F})) . i = 0 by DefPartialseq
.= (Partial_seq L,W) . i by C2, DefPartialseq ;
hence (Partial_seq L,W) . i = (Partial_seq L,(W \ {F})) . i ; :: thesis: verum

end;

end;

end;

hence (Partial_seq L,W) . i = (Partial_seq L,(W \ {F})) . i ; :: thesis: verum

end;

end;

end;

hence (Partial_seq L,W) . i = (Partial_seq L,(W \ {F})) . i ; :: thesis: verum

end;

then (Sum (Partial_seq L,W),(len L)) - ((Partial_seq L,W) . k) = (Sum (Partial_seq L,(W \ {F})),(len L)) - ((Partial_seq L,(W \ {F})) . k) by A5, lemlen03;
hence len L,(W \ {F}) = (len L,W) - (len F) by A8, A9; :: thesis: verum