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 set 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 set 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 set 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 set 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 set st x in Args o,B holds
( (Den o,B) . x is Function & (Den o,(product F)) . x is Function )
let x be set ; :: 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 Th20;
then (Den o,(product F)) . x in product (Carrier F,(the_result_sort_of o)) by PRALG_3:20;
then (Den o,B) . x in product (Carrier F,(the_result_sort_of o)) by A1, Th21;
then reconsider p = (Den o,B) . x as Element of (SORTS F) . (the_result_sort_of o) by PRALG_2:def 17;
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, Th21; :: thesis: verum