reconsider jj = 1 as Element of REAL by NUMBERS:19;
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 Def4;
* (x,y) = 0 by A1, Th12;
hence inv (* (x,y)) = 0 by Def4
.= * ((inv x),(inv y)) by A2, Th12 ;
:: 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, Th21;
A6: * (x,(inv x)) = 1 by A3, Def4;
A7: * (y,(inv y)) = 1 by A4, Def4;
* ((* (x,y)),(* ((inv x),(inv y)))) = * ((* ((* (x,y)),(inv x))),(inv y)) by Th13
.= * ((* (jj,y)),(inv y)) by A6, Th13
.= 1 by A7, Th19 ;
hence inv (* (x,y)) = * ((inv x),(inv y)) by A5, Def4; :: thesis: verum
end;
end;