let L be 1-sorted ; :: thesis: for A being AlgebraStr of L holds A is Subalgebra of A
let A be AlgebraStr of L; :: thesis: A is Subalgebra of A
thus ( the carrier of A c= the carrier of A & 1. A = 1. A & 0. A = 0. A & the addF of A = the addF of A || the carrier of A & the multF of A = the multF of A || the carrier of A & the lmult of A = the lmult of A | [:the carrier of L,the carrier of A:] ) by Lm2; :: according to POLYALG1:def 3 :: thesis: verum