( 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 `1)),((u `2) * (v `2))] is Element of Frac S by Def3; :: thesis: verum