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

( 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