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 4
.= (x " ) * (((y " ) * y) * x) by GROUP_1:def 4
.= (x " ) * ((1_ SF) * x) by A2, Th43
.= (x " ) * x by VECTSP_1:def 19
.= 1_ SF by A1, Th43 ;
hence (x " ) * (y " ) = (y * x) " by Th45; :: thesis: verum