let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of S
for A being b₁,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for o being OperSymbol of S
for x being Element of Args (o,A) holds (Den (o,A)) . x = ((canonical_homomorphism A) . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . x)
let X be non-empty ManySortedSet of S; :: thesis: for A being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for o being OperSymbol of S
for x being Element of Args (o,A) holds (Den (o,A)) . x = ((canonical_homomorphism A) . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . x)
let A be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: for o being OperSymbol of S
for x being Element of Args (o,A) holds (Den (o,A)) . x = ((canonical_homomorphism A) . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . x)
let o be OperSymbol of S; :: thesis: for x being Element of Args (o,A) holds (Den (o,A)) . x = ((canonical_homomorphism A) . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . x)
let x be Element of Args (o,A); :: thesis: (Den (o,A)) . x = ((canonical_homomorphism A) . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . x)
set k = canonical_homomorphism A;
set s = the_result_sort_of o;
( x in Args (o,A) & Args (o,A) c= Args (o,(Free (S,X))) ) by Th41;
then reconsider x0 = x as Element of Args (o,(Free (S,X))) ;
(canonical_homomorphism A) # x0 = x by Th66;
hence (Den (o,A)) . x = ((canonical_homomorphism A) . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . x) by Def10, MSUALG_3:def 7; :: thesis: verum