let x be Element of REAL+ ; :: thesis: ( x <> {} implies ex y being Element of REAL+ st x *' y = one )
reconsider rone = one as Element of REAL+ by Th1;
assume x <> {} ; :: thesis: ex y being Element of REAL+ st x *' y = one
then DEDEKIND_CUT x <> {} by Lm10;
then consider B being Element of DEDEKIND_CUTS such that
A1: (DEDEKIND_CUT x) *' B = DEDEKIND_CUT rone by Lm43;
take y = GLUED B; :: thesis: x *' y = one
thus x *' y = GLUED (DEDEKIND_CUT rone) by A1, Lm12
.= one by Lm23 ; :: thesis: verum