let L1, L2 be FinSequence; :: thesis: for H being LTL-formula
for W being Subset of (Subformulae H) st rng L1 = Subformulae H & L1 is one-to-one & rng L2 = Subformulae H & L2 is one-to-one holds
len (L1,W) = len (L2,W)
let H be LTL-formula; :: thesis: for W being Subset of (Subformulae H) st rng L1 = Subformulae H & L1 is one-to-one & rng L2 = Subformulae H & L2 is one-to-one holds
len (L1,W) = len (L2,W)
let W be Subset of (Subformulae H); :: thesis: ( rng L1 = Subformulae H & L1 is one-to-one & rng L2 = Subformulae H & L2 is one-to-one implies len (L1,W) = len (L2,W) )
defpred S₁[ Nat] means for W1 being Subset of (Subformulae H) st card W1 <= $1 & rng L1 = Subformulae H & L1 is one-to-one & rng L2 = Subformulae H & L2 is one-to-one holds
len (L1,W1) = len (L2,W1);
set k = card W;
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
S₁[k + 1]

proof

let W1 be Subset of (Subformulae H); :: thesis: ( card W1 <= k + 1 & rng L1 = Subformulae H & L1 is one-to-one & rng L2 = Subformulae H & L2 is one-to-one implies len (L1,W1) = len (L2,W1) )
assume A3: card W1 <= k + 1 ; :: thesis: ( not rng L1 = Subformulae H or not L1 is one-to-one or not rng L2 = Subformulae H or not L2 is one-to-one or len (L1,W1) = len (L2,W1) )
( rng L1 = Subformulae H & L1 is one-to-one & rng L2 = Subformulae H & L2 is one-to-one implies len (L1,W1) = len (L2,W1) )

proof

assume that
A4: ( rng L1 = Subformulae H & L1 is one-to-one ) and
A5: ( rng L2 = Subformulae H & L2 is one-to-one ) ; :: thesis: len (L1,W1) = len (L2,W1)

now :: thesis: len (L1,W1) = len (L2,W1)

per cases ( card W1 <= k or card W1 = k + 1 ) by A3, NAT_1:8;

suppose card W1 <= k ; :: thesis: len (L1,W1) = len (L2,W1)

hence len (L1,W1) = len (L2,W1) by A2, A4, A5; :: thesis: verum

end;

suppose A6: card W1 = k + 1 ; :: thesis: len (L1,W1) = len (L2,W1)

then W1 <> {} ;
then consider F being object such that
A7: F in W1 by XBOOLE_0:def 1;
F in Subformulae H by A7;
then reconsider F = F as LTL-formula by MODELC_2:1;
{F} c= W1 by A7, ZFMISC_1:31;
then A8: card (W1 \ {F}) = (card W1) - (card {F}) by CARD_2:44
.= (card W1) - 1 by CARD_1:30
.= k by A6 ;
A9: len (L1,W1) = ((len (L1,W1)) - (len F)) + (len F)
.= (len (L1,(W1 \ {F}))) + (len F) by A4, A7, Th6 ;
len (L2,W1) = ((len (L2,W1)) - (len F)) + (len F)
.= (len (L2,(W1 \ {F}))) + (len F) by A5, A7, Th6
.= (len (L1,(W1 \ {F}))) + (len F) by A2, A4, A5, A8 ;
hence len (L1,W1) = len (L2,W1) by A9; :: thesis: verum

end;

end;

end;

hence len (L1,W1) = len (L2,W1) ; :: thesis: verum

end;

hence ( not rng L1 = Subformulae H or not L1 is one-to-one or not rng L2 = Subformulae H or not L2 is one-to-one or len (L1,W1) = len (L2,W1) ) ; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A10: S₁[ 0 ]

proof

let W1 be Subset of (Subformulae H); :: thesis: ( card W1 <= 0 & rng L1 = Subformulae H & L1 is one-to-one & rng L2 = Subformulae H & L2 is one-to-one implies len (L1,W1) = len (L2,W1) )
assume card W1 <= 0 ; :: thesis: ( not rng L1 = Subformulae H or not L1 is one-to-one or not rng L2 = Subformulae H or not L2 is one-to-one or len (L1,W1) = len (L2,W1) )
then A11: W1 = {} H ;
then len (L1,W1) = 0 by Th4;
hence ( not rng L1 = Subformulae H or not L1 is one-to-one or not rng L2 = Subformulae H or not L2 is one-to-one or len (L1,W1) = len (L2,W1) ) by A11, Th4; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A10, A1);
then S₁[ card W] ;
hence ( rng L1 = Subformulae H & L1 is one-to-one & rng L2 = Subformulae H & L2 is one-to-one implies len (L1,W) = len (L2,W) ) ; :: thesis: verum