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;