let S be non empty non void ManySortedSign ; :: thesis: for U1 being non-empty MSAlgebra of S holds MSAAut U1 c= product (MSFuncs ( the Sorts of U1, the Sorts of U1))
let U1 be non-empty MSAlgebra of S; :: thesis: MSAAut 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 MSAAut U1 or q in product (MSFuncs ( the Sorts of U1, the Sorts of U1)) )
assume q in MSAAut U1 ; :: thesis: q in product (MSFuncs ( the Sorts of U1, the Sorts of U1))
then ex f being Element of MSAAut U1 st f = q ;
hence q in product (MSFuncs ( the Sorts of U1, the Sorts of U1)) by Th22; :: thesis: verum