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);
A2: for n being Element of NAT holds (Partial_seq L,({} H)) . n = (0 * n) + 0 by DefPartialseq;
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
reconsider n = n as Element of NAT by ORDINAL1:def 13;
B1: (Partial_seq L,({} H)) . 0 = 0 by DefPartialseq;
(Partial_Sums (Partial_seq L,({} H))) . n = ((n + 1) * (((Partial_seq L,({} H)) . 0 ) + ((Partial_seq L,({} H)) . n))) / 2 by A2, SERIES_2:42
.= ((n + 1) * (0 + 0 )) / 2 by B1, DefPartialseq ;
hence (Partial_Sums (Partial_seq L,({} H))) . n = 0 ; :: thesis: verum

end;

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