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

now :: thesis: for a being Element of R holds a in QS R

let a be Element of R; :: thesis: a in QS R
(((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: verum

end;

then the carrier of R c= QS R ;
hence contradiction by AS; :: thesis: verum