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₁ being set st b₁ = m `2 holds
( b₁ is Function-like & b₁ is Relation-like ) ; :: thesis: verum