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 Th12; :: thesis: verum

end;

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

A3: now :: thesis: ( inv x = 0 implies 1 = 0 )

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

end;

A5: ex x9, y9 being Element of REAL+ st
( y = x9 & y = y9 & * (y,y) = x9 *' y9 ) by A1, Def2, ARYTM_2:20;
A6: * (x,(inv x)) = 1 by A2, Def4;
* ((* (x,y)),(inv x)) = * ((* (x,(inv x))),y) by Th13
.= * (y,y) by A1, A2, Def4
.= 1 by A1, A5, ARYTM_2:15 ;
hence * (x,y) = x by A3, A6, Th18; :: thesis: verum

end;

end;