let K be Field; :: thesis: for a1, a2, a3, a4 being Element of K st a2 <> 0. K & a4 <> 0. K & a1 * (a2 ") = a3 * (a4 ") holds
a1 * a4 = a2 * a3
let a1, a2, a3, a4 be Element of K; :: thesis: ( a2 <> 0. K & a4 <> 0. K & a1 * (a2 ") = a3 * (a4 ") implies a1 * a4 = a2 * a3 )
assume A1: ( a2 <> 0. K & a4 <> 0. K ) ; :: thesis: ( not a1 * (a2 ") = a3 * (a4 ") or a1 * a4 = a2 * a3 )
assume A2: a1 * (a2 ") = a3 * (a4 ") ; :: thesis: a1 * a4 = a2 * a3
a1 * ((a2 ") * a2) = (a3 * (a4 ")) * a2 by A2, GROUP_1:def 3;
then a1 * (1. K) = (a3 * (a4 ")) * a2 by A1, VECTSP_1:def 10;
then a1 = (a3 * a2) * (a4 ") by GROUP_1:def 3;
then a1 * a4 = (a3 * a2) * ((a4 ") * a4) by GROUP_1:def 3
.= (a3 * a2) * (1. K) by A1, VECTSP_1:def 10
.= a3 * a2 ;
hence a1 * a4 = a2 * a3 ; :: thesis: verum