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:69
.= (sqr y) + ((- (2 * (mlt (x,y)))) + (sqr x))
.= ((sqr y) - (2 * (mlt (y,x)))) + (sqr x) by RFUNCT_1:8
.= sqr (y - x) by RVSUM_1:69 ; :: thesis: verum