for F being real-valued FinSequence holds 1 * F = F by RFUNCT_1:21;