let x, y be Element of REAL+ ; :: thesis: ( x = one implies x *' y = y )
assume A1: x = one ; :: thesis: x *' y = y
then ex r being Element of RAT+ st
( x = r & DEDEKIND_CUT x = { s where s is Element of RAT+ : s < r } ) by Def3;
hence x *' y = GLUED (DEDEKIND_CUT y) by A1, Lm44
.= y by Lm23 ;
:: thesis: verum