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: * x,y = 0 by Th14;
A3: ( inv x = 0 or inv y = 0 ) by A1, Def5;
thus inv (* x,y) = 0 by A2, Def5
.= * (inv x),(inv y) by A3, Th14 ; :: thesis: verum

end;

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

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

end;

end;