let S be non empty non void ManySortedSign ; :: thesis: for X0 being V5() countable ManySortedSet of S
for A0 being b₁,S -terms MSAlgebra over S
for o being OperSymbol of S
for x being Element of Args (o,A0) holds (Den (o,A0)) . x = ((canonical_homomorphism A0) . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . x)
let X0 be V5() countable ManySortedSet of S; :: thesis: for A0 being X0,S -terms MSAlgebra over S
for o being OperSymbol of S
for x being Element of Args (o,A0) holds (Den (o,A0)) . x = ((canonical_homomorphism A0) . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . x)
let A0 be X0,S -terms MSAlgebra over S; :: thesis: for o being OperSymbol of S
for x being Element of Args (o,A0) holds (Den (o,A0)) . x = ((canonical_homomorphism A0) . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . x)
set A = A0;
let o be OperSymbol of S; :: thesis: for x being Element of Args (o,A0) holds (Den (o,A0)) . x = ((canonical_homomorphism A0) . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . x)
let x be Element of Args (o,A0); :: thesis: (Den (o,A0)) . x = ((canonical_homomorphism A0) . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . x)
set k = canonical_homomorphism A0;
set s = the_result_sort_of o;
( x in Args (o,A0) & Args (o,A0) c= Args (o,(Free (S,X0))) ) by Th40;
then reconsider x0 = x as Element of Args (o,(Free (S,X0))) ;
(canonical_homomorphism A0) # x0 = x by Th65;
hence (Den (o,A0)) . x = ((canonical_homomorphism A0) . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . x) by Def7, MSUALG_3:def 7; :: thesis: verum