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_{1} being ComplexSubAlgebra of V st b_{1} is strict
; :: thesis: verum

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