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