let F1, F2 be real-valued FinSequence; :: thesis: sqr (F1 - F2) = ((sqr F1) - (2 * (mlt (F1,F2)))) + (sqr F2)
thus sqr (F1 - F2) = ((sqr F1) + (2 * (mlt (F1,(- F2))))) + (sqr (- F2)) by Th68
.= ((sqr F1) + (2 * (mlt (F1,(- F2))))) + (sqr F2) by Th57
.= ((sqr F1) + (2 * ((- 1) * (mlt (F1,F2))))) + (sqr F2) by RFUNCT_1:12
.= ((sqr F1) + (((- 1) * 2) * (mlt (F1,F2)))) + (sqr F2) by RFUNCT_1:17
.= ((sqr F1) - (2 * (mlt (F1,F2)))) + (sqr F2) by RFUNCT_1:17 ; :: thesis: verum