let UA be Universal_Algebra; :: thesis: UAAut UA c= Funcs the carrier of UA,the carrier of UA
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in UAAut UA or q in Funcs the carrier of UA,the carrier of UA )
assume q in UAAut UA ; :: thesis: q in Funcs the carrier of UA,the carrier of UA
then ex f being Element of UAAut UA st f = q ;
hence q in Funcs the carrier of UA,the carrier of UA by FUNCT_2:12; :: thesis: verum