let L be 1-sorted ; :: thesis: for A being AlgebraStr over L holds A is Subalgebra of A
let A be AlgebraStr over 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:] ) ; :: according to POLYALG1:def 3 :: thesis: verum