let I be set ; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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) ; :: thesis: ( (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 ; :: thesis: (Den (o,(product F))) . x is Function
thus (Den (o,(product F))) . x is Function by A1, A2, Th19; :: thesis: verum