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

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