let F be preordered Field; :: thesis: for P being Preordering of F
for a being non zero b₁ -ordered Element of F
for b being b₁ -ordered Element of F holds abs (P,(b * (a "))) = (abs (P,b)) * ((abs (P,a)) ")
let P be Preordering of F; :: thesis: for a being non zero P -ordered Element of F
for b being P -ordered Element of F holds abs (P,(b * (a "))) = (abs (P,b)) * ((abs (P,a)) ")
let a be non zero P -ordered Element of F; :: thesis: for b being P -ordered Element of F holds abs (P,(b * (a "))) = (abs (P,b)) * ((abs (P,a)) ")
let b be P -ordered Element of F; :: thesis: abs (P,(b * (a "))) = (abs (P,b)) * ((abs (P,a)) ")
thus abs (P,(b * (a "))) = (abs (P,b)) * (abs (P,(a "))) by abs10
.= (abs (P,b)) * ((abs (P,a)) ") by sq2 ; :: thesis: verum