let V be non empty set ; :: thesis: for W being non empty Subset of V holds Funcs W c= Funcs V
let W be non empty Subset of V; :: thesis: Funcs W c= Funcs V
let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in Funcs W or f in Funcs V )
assume f in Funcs W ; :: thesis: f in Funcs V
then ex A, B being Element of W st
( ( B = {} implies A = {} ) & f is Function of A,B ) by Th1;
hence f in Funcs V by Th1; :: thesis: verum