theorem Th24: :: MSUALG_9:24

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for F being ManySortedFunction of A,(Trivial_Algebra S)
for o being OperSymbol of S
for x being Element of Args (o,A) holds
( (F . (the_result_sort_of o)) . ((Den (o,A)) . x) = 0 & (Den (o,(Trivial_Algebra S))) . (F # x) = 0 )