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:22; :: thesis: verum