for V being Algebra
for V1 being Subset of V st V1 is additively-linearly-closed & V1 is multiplicatively-closed & not V1 is empty holds
AlgebraStr(# V1,(mult_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)),(One_ (V1,V)),(Zero_ (V1,V)) #) is Subalgebra of V