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 set ; :: 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