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 3
.= (b * (a * (a "))) * (b ") by GROUP_1:def 3
.= (b * (1_ F)) * (b ") by A1, VECTSP_1:def 10
.= b * (b ")
.= 1_ F by A2, VECTSP_1:def 10 ;
b * a <> 0. F by A1, A2, VECTSP_1:12;
hence (a ") * (b ") = (b * a) " by A3, VECTSP_1:def 10; :: thesis: verum