( 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 `1)),((u `2) * (v `2))] is Element of Q. I by Def1; :: thesis: verum