( u `2 <> 0. I & v `2 <> 0. I ) by Th2;
then (u `2) * (v `2) <> 0. I by VECTSP_2:def 1;
hence [(((u `1) * (v `2)) + ((v `1) * (u `2))),((u `2) * (v `2))] is Element of Q. I by Def1; :: thesis: verum