let x, y be real-valued FinSequence; :: thesis: sqr (x - y) = sqr (y - x)
thus (x - y) ^2 = ((x ^2 ) - (2 (#) (x (#) y))) + (y ^2 ) by RVSUM_1:99
.= (sqr y) + ((- (2 * (mlt x,y))) + (sqr x))
.= ((sqr y) - (2 * (mlt y,x))) + (sqr x) by RFUNCT_1:19
.= sqr (y - x) by RVSUM_1:99 ; :: thesis: verum