take IT = { the Function of A,B}; :: thesis: for x being Element of IT holds x is Function of A,B
let g be Element of IT; :: thesis: g is Function of A,B
thus g is Function of A,B by TARSKI:def 1; :: thesis: verum