let V be non empty set ; :: thesis: for A, B being Element of V holds Funcs (A,B) c= Funcs V
let A, B be Element of V; :: thesis: Funcs (A,B) c= Funcs V
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Funcs (A,B) or x in Funcs V )
assume A1: x in Funcs (A,B) ; :: thesis: x in Funcs V
then A2: x is Function of A,B by FUNCT_2:66;
( B = {} implies A = {} ) by A1;
hence x in Funcs V by A2, Th1; :: thesis: verum