let V be non empty set ; :: thesis: for A, B being Element of V holds Maps (A,B) c= Maps V
let A, B be Element of V; :: thesis: Maps (A,B) c= Maps V
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Maps (A,B) or z in Maps V )
assume z in Maps (A,B) ; :: thesis: z in Maps V
then ex f being Element of Funcs V st
( z = [[A,B],f] & [[A,B],f] in Maps V ) ;
hence z in Maps V ; :: thesis: verum