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

( 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