theorem Th20: :: EQUATION:20

for I being set
for S being non empty non void ManySortedSign
for F being MSAlgebra-Family of I,S
for B being MSSubAlgebra of product F
for o being OperSymbol of S
for x being object st x in Args (o,B) holds
( (Den (o,B)) . x is Function & (Den (o,(product F))) . x is Function )