let I be 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 )
let S be 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 )
let F be 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 )
let B be 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 )
let o be 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 )
let x be object ; ( x in Args (o,B) implies ( (Den (o,B)) . x is Function & (Den (o,(product F))) . x is Function ) )
set r = the_result_sort_of o;
assume A1:
x in Args (o,B)
; ( (Den (o,B)) . x is Function & (Den (o,(product F))) . x is Function )
then
x in Args (o,(product F))
by Th18;
then
(Den (o,(product F))) . x in product (Carrier (F,(the_result_sort_of o)))
by PRALG_3:19;
then
(Den (o,B)) . x in product (Carrier (F,(the_result_sort_of o)))
by A1, Th19;
then reconsider p = (Den (o,B)) . x as Element of (SORTS F) . (the_result_sort_of o) by PRALG_2:def 10;
A2:
p is Function
;
hence
(Den (o,B)) . x is Function
; (Den (o,(product F))) . x is Function
thus
(Den (o,(product F))) . x is Function
by A1, A2, Th19; verum