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