let L be FinSequence; :: thesis: for H being LTL-formula holds len (L,({} H)) = 0
let H be LTL-formula; :: thesis: len (L,({} H)) = 0
set s = Partial_seq (L,({} H));
A1: for n being Nat holds (Partial_seq (L,({} H))) . n = (0 * n) + 0 by Def24;
for n being Nat holds (Partial_Sums (Partial_seq (L,({} H)))) . n = 0

proof

let n be Nat; :: thesis: (Partial_Sums (Partial_seq (L,({} H)))) . n = 0
A2: (Partial_seq (L,({} H))) . 0 = 0 by Def24;
(Partial_Sums (Partial_seq (L,({} H)))) . n = ((n + 1) * (((Partial_seq (L,({} H))) . 0) + ((Partial_seq (L,({} H))) . n))) / 2 by A1, SERIES_2:42
.= ((n + 1) * (0 + 0)) / 2 by A2, Def24 ;
hence (Partial_Sums (Partial_seq (L,({} H)))) . n = 0 ; :: thesis: verum

end;

hence len (L,({} H)) = 0 ; :: thesis: verum