theorem :: REALALG2:77

for F being preordered Field
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)) ")