theorem Th1: :: CC0SP1:1

for X being non empty set
for V being ComplexAlgebra
for V1 being non empty Subset of V
for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for MR being Function of [:COMPLEX,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:COMPLEX,V1:] & V1 is having-inverse holds
ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra of V