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 set ; :: 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:121;
( B = {} implies A = {} ) by A1;
hence x in Funcs V by A2, Th1; :: thesis: verum