for F1, F2 being real-valued FinSequence holds sqr (F1 + F2) = ((sqr F1) + (2 * (mlt (F1,F2)))) + (sqr F2)