let UA be Universal_Algebra; :: thesis: UAEnd UA c= Funcs ( the carrier of UA, the carrier of UA)
let q be object ; :: 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:9; :: thesis: verum