set V1 = [#] V;
( the addF of V = the addF of V || ([#] V) & the multF of V = the multF of V || ([#] V) ) by RELSET_1:19;
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