let x, y be Element of REAL ; :: thesis: ( y = 1 implies * x,y = x )
assume A1: y = 1 ; :: thesis: * x,y = x

per cases ( x = 0 or x <> 0 ) ;

suppose x = 0 ; :: thesis: * x,y = x

hence * x,y = x by Th14; :: thesis: verum

end;

suppose A2: x <> 0 ; :: thesis: * x,y = x

A3: now

assume A4: inv x = 0 ; :: thesis: 1 = 0
thus 1 = * x,(inv x) by A2, Def5
.= 0 by A4, Th14 ; :: thesis: verum

end;

A5: ex x9, y9 being Element of REAL+ st
( y = x9 & y = y9 & * y,y = x9 *' y9 ) by A1, Def3, ARYTM_2:21;
A6: * x,(inv x) = 1 by A2, Def5;
* (* x,y),(inv x) = * (* x,(inv x)),y by Th15
.= * y,y by A1, A2, Def5
.= 1 by A1, A5, ARYTM_2:16 ;
hence * x,y = x by A3, A6, Th20; :: thesis: verum

end;

end;