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