per cases ( x nin dom C or x in dom C ) ;
suppose x nin dom C ; :: thesis: ( C . x is segmental & C . x is Function-like & C . x is Relation-like )
hence ( C . x is segmental & C . x is Function-like & C . x is Relation-like ) by FUNCT_1:def 2; :: thesis: verum
end;
suppose x in dom C ; :: thesis: ( C . x is segmental & C . x is Function-like & C . x is Relation-like )
hence ( C . x is segmental & C . x is Function-like & C . x is Relation-like ) by Def14; :: thesis: verum
end;
end;