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 Def22;
assume (a * c) - b = 0. F ; :: thesis: c = b * (a " )
then (a " ) * (a * c) = b * (a " ) by RLVECT_1:35;
then ((a " ) * a) * c = b * (a " ) by GROUP_1:def 4;
hence c = b * (a " ) by A2, Def16; :: 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:25;
hence c = b * (a " ) by A1, A3, RLVECT_1:47; :: thesis: verum