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