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 Th98
.= ((sqr F1) + (2 * (mlt (F1,(- F2))))) + (sqr F2) by Th83
.= ((sqr F1) + (2 * ((- 1) * (mlt (F1,F2))))) + (sqr F2) by RFUNCT_1:24
.= ((sqr F1) + (((- 1) * 2) * (mlt (F1,F2)))) + (sqr F2) by RFUNCT_1:29
.= ((sqr F1) - (2 * (mlt (F1,F2)))) + (sqr F2) by RFUNCT_1:29 ; :: thesis: verum