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 ") )
proof
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;
assume A3: a <> 0. F ; :: thesis: ( not b - (c * a) = 0. F or 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