let R be Field; :: thesis:
assume AS: ( Char R <> 2 & QS R <> the carrier of R ) ; :: thesis:
assume - (1. R) in QS R ; :: thesis:
then consider e being Element of R such that
H: ( e = - (1. R) & e is sum_of_squares ) ;

let a be Element of R; :: thesis:
(((a + (1. R)) / (2 '*' (1. R))) ^2) + ((- (1. R)) * (((a - (1. R)) / (2 '*' (1. R))) ^2)) = (((a + (1. R)) / (2 '*' (1. R))) ^2) + (- ((1. R) * (((a - (1. R)) / (2 '*' (1. R))) ^2))) by VECTSP_1:9
.= (((a + (1. R)) / (2 '*' (1. R))) ^2) - (((a - (1. R)) / (2 '*' (1. R))) ^2)
.= a by AS, P5 ;
hence a in QS R by H; :: thesis:

end;