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