let x, y be Element of REAL ; :: thesis: inv (* (x,y)) = * ((inv x),(inv y))

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

suppose A1: ( x = 0 or y = 0 ) ; :: thesis: inv (* (x,y)) = * ((inv x),(inv y))

then A2: ( inv x = 0 or inv y = 0 ) by Def5;
* (x,y) = 0 by A1, Th14;
hence inv (* (x,y)) = 0 by Def5
.= * ((inv x),(inv y)) by A2, Th14 ;
:: thesis: verum

end;

suppose that A3: x <> 0 and
A4: y <> 0 ; :: thesis: inv (* (x,y)) = * ((inv x),(inv y))

A5: * (x,y) <> 0 by A3, A4, Th23;
A6: * (x,(inv x)) = 1 by A3, Def5;
A7: * (y,(inv y)) = 1 by A4, Def5;
* ((* (x,y)),(* ((inv x),(inv y)))) = * ((* ((* (x,y)),(inv x))),(inv y)) by Th15
.= * ((* (j,y)),(inv y)) by A6, Th15
.= 1 by A7, Th21 ;
hence inv (* (x,y)) = * ((inv x),(inv y)) by A5, Def5; :: thesis: verum

end;

end;