let K be Field; :: thesis: for a2, a4, a1, a3 being Element of K st a2 <> 0. K & a4 <> 0. K & a1 * a4 = a2 * a3 holds
a1 * (a2 ") = a3 * (a4 ")
let a2, a4, a1, a3 be Element of K; :: thesis: ( a2 <> 0. K & a4 <> 0. K & a1 * a4 = a2 * a3 implies a1 * (a2 ") = a3 * (a4 ") )
assume AS1: ( a2 <> 0. K & a4 <> 0. K ) ; :: thesis: ( not a1 * a4 = a2 * a3 or a1 * (a2 ") = a3 * (a4 ") )
assume B1: a1 * a4 = a2 * a3 ; :: thesis: a1 * (a2 ") = a3 * (a4 ")
(a2 * a3) * (a4 ") = a1 * ((a4 ") * a4) by B1, GROUP_1:def 3
.= a1 * (1. K) by AS1, VECTSP_1:def 10
.= a1 by VECTSP_1:def 6 ;
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 AS1, VECTSP_1:def 10
.= a3 * (a4 ") by VECTSP_1:def 6 ;
hence a1 * (a2 ") = a3 * (a4 ") ; :: thesis: verum