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 consider f being Element of UAAut UA such that
A1: f = q ;
thus q in Funcs the carrier of UA,the carrier of UA by A1, FUNCT_2:12; :: thesis: verum