set V1 = [#] V;
( the addF of V = the addF of V || ([#] V) & the multF of V = the multF of V || ([#] V) ) by RELSET_1:34;
then doubleLoopStr(# the carrier of V,the addF of V,the multF of V,(1. V),(0. V) #) is Subring of V by Th1;
hence ex b₁ being Subring of V st b₁ is strict ; :: thesis: verum