let S be non empty non void ManySortedSign ; :: thesis: for U1 being non-empty MSAlgebra of S holds MSAEnd U1 c= product (MSFuncs ( the Sorts of U1, the Sorts of U1))
let U1 be non-empty MSAlgebra of S; :: thesis: MSAEnd U1 c= product (MSFuncs ( the Sorts of U1, the Sorts of U1))
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in MSAEnd U1 or q in product (MSFuncs ( the Sorts of U1, the Sorts of U1)) )
assume q in MSAEnd U1 ; :: thesis: q in product (MSFuncs ( the Sorts of U1, the Sorts of U1))
then q is Element of MSAEnd U1 ;
hence q in product (MSFuncs ( the Sorts of U1, the Sorts of U1)) by AUTALG_1:19; :: thesis: verum