theorem Th5: :: MSAFREE:5

for S being non empty non void ManySortedSign
for X being ManySortedSet of the carrier of S
for o being OperSymbol of S
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [[o, the carrier of S],b] in REL X iff ( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) )