( u `2 in S & v `2 in S ) by Th18;
then (u `2) * (v `2) in S by C0SP1:def 4;
hence [(((u `1) * (v `2)) + ((v `1) * (u `2))),((u `2) * (v `2))] is Element of Frac S by Def3; :: thesis: verum