consider f being Function of A,B;
reconsider IT = {f} as non empty functional set by Th8;
take IT ; :: 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