for x being FinSequence of REAL holds |(x,((len x) |-> 1))| = Sum x by Th32;