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