let V be non empty set ; :: thesis: for W being non empty Subset of V holds Maps W c= Maps V
let W be non empty Subset of V; :: thesis: Maps W c= Maps V
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Maps W or x in Maps V )
assume x in Maps W ; :: thesis: x in Maps V
then consider A, B being Element of W, f being Element of Funcs W such that
A1: ( x = [[A,B],f] & ( B = {} implies A = {} ) & f is Function of A,B ) ;
( Funcs W c= Funcs V & f in Funcs W ) by Th3;
hence x in Maps V by A1; :: thesis: verum