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