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