let R be preordered domRing; :: thesis: for P being Preordering of R
for a being b1 -ordered Element of R holds (abs (P,a)) ^2 = a ^2
let P be Preordering of R; :: thesis: for a being P -ordered Element of R holds (abs (P,a)) ^2 = a ^2
let a be P -ordered Element of R; :: thesis: (abs (P,a)) ^2 = a ^2
a in P \/ (- P) by defppp;
per cases then ( a in P or a in - P ) by XBOOLE_0:def 3;
suppose a in P ; :: thesis: (abs (P,a)) ^2 = a ^2
then 0. R <= P,a ;
hence (abs (P,a)) ^2 = a ^2 by av2; :: thesis: verum
end;
suppose a in - P ; :: thesis: (abs (P,a)) ^2 = a ^2
then - a in - (- P) ;
then a <= P, 0. R ;
hence (abs (P,a)) ^2 = (- a) ^2 by av3
.= a ^2 by VECTSP_1:10 ;
:: thesis: verum
end;
end;