let SF be Skew-Field; :: thesis: for x, y being Scalar of SF st x <> 0. SF & y <> 0. SF holds
(x ") * (y ") = (y * x) "
let x, y be Scalar of SF; :: thesis: ( x <> 0. SF & y <> 0. SF implies (x ") * (y ") = (y * x) " )
assume A1: x <> 0. SF ; :: thesis: ( not y <> 0. SF or (x ") * (y ") = (y * x) " )
assume A2: y <> 0. SF ; :: thesis: (x ") * (y ") = (y * x) "
((x ") * (y ")) * (y * x) = (x ") * ((y ") * (y * x)) by GROUP_1:def 3
.= (x ") * (((y ") * y) * x) by GROUP_1:def 3
.= (x ") * ((1_ SF) * x) by A2, Th9
.= (x ") * x
.= 1_ SF by A1, Th9 ;
hence (x ") * (y ") = (y * x) " by Th10; :: thesis: verum