:: deftheorem Def3 defines Subalgebra POLYALG1:def 3 :
for L being 1-sorted
for A, b₃ being AlgebraStr over L holds
( b₃ is Subalgebra of A iff ( the carrier of b₃ c= the carrier of A & 1. b₃ = 1. A & 0. b₃ = 0. A & the addF of b₃ = the addF of A || the carrier of b₃ & the multF of b₃ = the multF of A || the carrier of b₃ & the lmult of b₃ = the lmult of A | [: the carrier of L, the carrier of b₃:] ) );