per cases ( j in dom B or not j in dom B ) ;

suppose j in dom B ; :: thesis: ( B . j is Function-like & B . j is Relation-like )

hence ( B . j is Function-like & B . j is Relation-like ) by Def6; :: thesis: verum

end;

suppose not j in dom B ; :: thesis: ( B . j is Function-like & B . j is Relation-like )

hence ( B . j is Function-like & B . j is Relation-like ) by FUNCT_1:def 2; :: thesis: verum

end;

end;