let a be Element of dom o; :: thesis: ( a is Relation-like & a is Function-like )
( a in dom o & dom o c= the carrier of S * ) ;
then a is Element of the carrier of S * ;
hence ( a is Relation-like & a is Function-like ) ; :: thesis: verum