let R be ordered domRing; :: thesis: for P being Ordering of R
for a being Element of R holds a = (signum (P,a)) '*' (abs (P,a))
let P be Ordering of R; :: thesis: for a being Element of R holds a = (signum (P,a)) '*' (abs (P,a))
let a be Element of R; :: thesis: a = (signum (P,a)) '*' (abs (P,a))
H: P \/ (- P) = the carrier of R by REALALG1:def 15;

per cases ( a in P \ {(0. R)} or a = 0. R or ( not a in P \ {(0. R)} & a <> 0. R ) ) ;

suppose A: a in P \ {(0. R)} ; :: thesis: a = (signum (P,a)) '*' (abs (P,a))

then B: a in P by XBOOLE_0:def 5;
thus (signum (P,a)) '*' (abs (P,a)) = 1 '*' (abs (P,a)) by A, defsgn
.= 1 '*' a by B, REALALG2:def 11
.= a by RING_3:60 ; :: thesis: verum

end;

suppose A: a = 0. R ; :: thesis: a = (signum (P,a)) '*' (abs (P,a))

hence (signum (P,a)) '*' (abs (P,a)) = 0 '*' (abs (P,a)) by defsgn
.= a by A, RING_3:59 ;
:: thesis: verum

end;

suppose A: ( not a in P \ {(0. R)} & a <> 0. R ) ; :: thesis: a = (signum (P,a)) '*' (abs (P,a))

then ( not a in P or a in {(0. R)} ) by XBOOLE_0:def 5;
then a in - P by A, H, XBOOLE_0:def 3, TARSKI:def 1;
then - a in - (- P) ;
then B: a <= P, 0. R ;
thus (signum (P,a)) '*' (abs (P,a)) = (- 1) '*' (abs (P,a)) by A, defsgn
.= (- 1) '*' (- a) by B, REALALG2:70
.= - (- a) by RING_3:61
.= a ; :: thesis: verum

end;

end;