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 x in Funcs A,B ; :: thesis: x in Funcs V
then ( ( B = {} implies A = {} ) & x is Function of A,B ) by FUNCT_2:121;
hence x in Funcs V by Th1; :: thesis: verum