let t be Element of A . x; :: thesis: ( t is Relation-like & t is Function-like )
per cases ( x nin dom A or A . x = {} or ( x in the carrier of S & A . x <> {} ) ) ;
suppose ( x nin dom A or A . x = {} ) ; :: thesis: ( t is Relation-like & t is Function-like )
then A . x = {} by FUNCT_1:def 2;
hence ( t is Relation-like & t is Function-like ) ; :: thesis: verum
end;
suppose A1: ( x in the carrier of S & A . x <> {} ) ; :: thesis: ( t is Relation-like & t is Function-like )
then reconsider s = x as SortSymbol of S ;
( A . s c= the Sorts of (FreeMSA X) . s & t in A . s ) by A1, PBOOLE:def 2, PBOOLE:def 18;
then t is Element of the Sorts of (FreeMSA X) . s ;
then t is Term of S,X by MSATERM:13;
hence ( t is Relation-like & t is Function-like ) ; :: thesis: verum
end;
end;