let V be non empty set ; :: thesis: Maps V c= [:[:V,V:],(Funcs V):]
let m be set ; :: according to TARSKI:def 3 :: thesis: ( not m in Maps V or m in [:[:V,V:],(Funcs V):] )
assume m in Maps V ; :: thesis: m in [:[:V,V:],(Funcs V):]
then ex A, B being Element of V ex f being Element of Funcs V st
( m = [[A,B],f] & ( B = {} implies A = {} ) & f is Function of A,B ) ;
hence m in [:[:V,V:],(Funcs V):] ; :: thesis: verum