let F be Field; :: thesis: for a, b, c being Element of F holds

( ( a <> 0. F & (a * c) - b = 0. F implies c = b * (a ") ) & ( a <> 0. F & b - (c * a) = 0. F implies c = b * (a ") ) )

let a, b, c be Element of F; :: thesis: ( ( a <> 0. F & (a * c) - b = 0. F implies c = b * (a ") ) & ( a <> 0. F & b - (c * a) = 0. F implies c = b * (a ") ) )

thus A1: ( a <> 0. F & (a * c) - b = 0. F implies c = b * (a ") ) :: thesis: ( a <> 0. F & b - (c * a) = 0. F implies c = b * (a ") )

assume b - (c * a) = 0. F ; :: thesis: c = b * (a ")

then - (b - (c * a)) = 0. F by RLVECT_1:12;

hence c = b * (a ") by A1, A3, RLVECT_1:33; :: thesis: verum

( ( a <> 0. F & (a * c) - b = 0. F implies c = b * (a ") ) & ( a <> 0. F & b - (c * a) = 0. F implies c = b * (a ") ) )

let a, b, c be Element of F; :: thesis: ( ( a <> 0. F & (a * c) - b = 0. F implies c = b * (a ") ) & ( a <> 0. F & b - (c * a) = 0. F implies c = b * (a ") ) )

thus A1: ( a <> 0. F & (a * c) - b = 0. F implies c = b * (a ") ) :: thesis: ( a <> 0. F & b - (c * a) = 0. F implies c = b * (a ") )

proof

assume A3:
a <> 0. F
; :: thesis: ( not b - (c * a) = 0. F or c = b * (a ") )
assume
a <> 0. F
; :: thesis: ( not (a * c) - b = 0. F or c = b * (a ") )

then A2: (a ") * a = 1. F by Def10;

assume (a * c) - b = 0. F ; :: thesis: c = b * (a ")

then (a ") * (a * c) = b * (a ") by RLVECT_1:21;

then ((a ") * a) * c = b * (a ") by GROUP_1:def 3;

hence c = b * (a ") by A2; :: thesis: verum

end;then A2: (a ") * a = 1. F by Def10;

assume (a * c) - b = 0. F ; :: thesis: c = b * (a ")

then (a ") * (a * c) = b * (a ") by RLVECT_1:21;

then ((a ") * a) * c = b * (a ") by GROUP_1:def 3;

hence c = b * (a ") by A2; :: thesis: verum

assume b - (c * a) = 0. F ; :: thesis: c = b * (a ")

then - (b - (c * a)) = 0. F by RLVECT_1:12;

hence c = b * (a ") by A1, A3, RLVECT_1:33; :: thesis: verum