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

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