let F be Field; :: thesis: for S being Subset of F st S * S c= S & S \/ (- S) = the carrier of F holds
( S /\ (- S) = {(0. F)} iff not - (1. F) in S )
let S be Subset of F; :: thesis: ( S * S c= S & S \/ (- S) = the carrier of F implies ( S /\ (- S) = {(0. F)} iff not - (1. F) in S ) )
assume AS: ( S * S c= S & S \/ (- S) = the carrier of F ) ; :: thesis: ( S /\ (- S) = {(0. F)} iff not - (1. F) in S )
SQ F c= S
proof
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in SQ F or o in S )
assume o in SQ F ; :: thesis: o in S
then consider a being Element of F such that
A: ( a = o & a is square ) ;
consider b being Element of F such that
B: b ^2 = a by A;
per cases ( b in S or b in - S ) by AS, XBOOLE_0:def 3;
suppose b in S ; :: thesis: o in S
then b * b in S * S ;
hence o in S by AS, A, B; :: thesis: verum
end;
suppose b in - S ; :: thesis: o in S
then - b in - (- S) ;
then (- b) * (- b) in S * S ;
then (- b) * (- b) in S by AS;
hence o in S by A, B, VECTSP_1:10; :: thesis: verum
end;
end;
end;
hence ( S /\ (- S) = {(0. F)} iff not - (1. F) in S ) by X1, AS; :: thesis: verum