let V be non empty set ; :: thesis: for m being Element of Maps V ex f being Element of Funcs V ex A, B being Element of V st
( m = [[A,B],f] & ( B = {} implies A = {} ) & f is Function of A,B )
let m be Element of Maps V; :: thesis: ex f being Element of Funcs V ex A, B being Element of V st
( m = [[A,B],f] & ( B = {} implies A = {} ) & f is Function of A,B )
m in { [[A,B],f] where A, B is Element of V, f is Element of Funcs V : ( ( B = {} implies A = {} ) & f is Function of A,B ) } ;
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 ex f being Element of Funcs V ex A, B being Element of V st
( m = [[A,B],f] & ( B = {} implies A = {} ) & f is Function of A,B ) ; :: thesis: verum