theorem Th2:
for
V being
ComplexAlgebra for
V1 being non
empty multiplicatively-closed Cadditively-linearly-closed Subset of
V holds
ComplexAlgebraStr(#
V1,
(mult_ (V1,V)),
(Add_ (V1,V)),
(Mult_ (V1,V)),
(One_ (V1,V)),
(Zero_ (V1,V)) #) is
ComplexSubAlgebra of
V