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

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