let F be almost_left_invertible commutative Ring; :: thesis: for a, b being Element of F st a <> 0. F & b <> 0. F holds
(a " ) * (b " ) = (b * a) "
let a, b be Element of F; :: thesis: ( a <> 0. F & b <> 0. F implies (a " ) * (b " ) = (b * a) " )
assume that
A1: a <> 0. F and
A2: b <> 0. F ; :: thesis: (a " ) * (b " ) = (b * a) "
A3: (b * a) * ((a " ) * (b " )) = ((b * a) * (a " )) * (b " ) by GROUP_1:def 4
.= (b * (a * (a " ))) * (b " ) by GROUP_1:def 4
.= (b * (1_ F)) * (b " ) by A1, VECTSP_1:def 22
.= b * (b " ) by VECTSP_1:def 13
.= 1_ F by A2, VECTSP_1:def 22 ;
b * a <> 0. F by A1, A2, VECTSP_1:44;
hence (a " ) * (b " ) = (b * a) " by A3, VECTSP_1:def 22; :: thesis: verum