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 ) by Th4;

hence for b_{1} being set st b_{1} = m `2 holds

( b_{1} is Function-like & b_{1} is Relation-like )
; :: thesis: verum

( m = [[A,B],f] & ( B = {} implies A = {} ) & f is Function of A,B ) by Th4;

hence for b

( b