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 h being ManySortedFunction of (Free (S,X)),A st h is_homomorphism Free (S,X),A holds
for o being OperSymbol of S
for x being Element of Args (o,(Free (S,X))) holds (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . x) = (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . ((canonical_homomorphism A) # 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 h being ManySortedFunction of (Free (S,X)),A st h is_homomorphism Free (S,X),A holds
for o being OperSymbol of S
for x being Element of Args (o,(Free (S,X))) holds (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . x) = (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . ((canonical_homomorphism A) # x))
let A be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: for h being ManySortedFunction of (Free (S,X)),A st h is_homomorphism Free (S,X),A holds
for o being OperSymbol of S
for x being Element of Args (o,(Free (S,X))) holds (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . x) = (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . ((canonical_homomorphism A) # x))
set X0 = X;
let h be ManySortedFunction of (Free (S,X)),A; :: thesis: ( h is_homomorphism Free (S,X),A implies for o being OperSymbol of S
for x being Element of Args (o,(Free (S,X))) holds (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . x) = (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . ((canonical_homomorphism A) # x)) )
assume h is_homomorphism Free (S,X),A ; :: thesis: for o being OperSymbol of S
for x being Element of Args (o,(Free (S,X))) holds (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . x) = (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . ((canonical_homomorphism A) # x))
then consider g being ManySortedFunction of A,A such that
A1: ( g is_homomorphism A,A & h = g ** (canonical_homomorphism A) ) by Th65;
let o be OperSymbol of S; :: thesis: for x being Element of Args (o,(Free (S,X))) holds (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . x) = (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . ((canonical_homomorphism A) # x))
let x be Element of Args (o,(Free (S,X))); :: thesis: (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . x) = (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . ((canonical_homomorphism A) # x))
set k = canonical_homomorphism A;
A2: ( (canonical_homomorphism A) # x in Args (o,A) & Args (o,A) c= Args (o,(Free (S,X))) ) by Th41;
thus (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . x) = ((g . (the_result_sort_of o)) * ((canonical_homomorphism A) . (the_result_sort_of o))) . ((Den (o,(Free (S,X)))) . x) by A1, MSUALG_3:2
.= (g . (the_result_sort_of o)) . (((canonical_homomorphism A) . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . x)) by MSUALG_9:18, FUNCT_2:15
.= (g . (the_result_sort_of o)) . ((Den (o,A)) . ((canonical_homomorphism A) # x)) by Def10, MSUALG_3:def 7
.= (g . (the_result_sort_of o)) . (((canonical_homomorphism A) . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . ((canonical_homomorphism A) # x))) by Th67
.= ((g . (the_result_sort_of o)) * ((canonical_homomorphism A) . (the_result_sort_of o))) . ((Den (o,(Free (S,X)))) . ((canonical_homomorphism A) # x)) by A2, MSUALG_9:18, FUNCT_2:15
.= (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . ((canonical_homomorphism A) # x)) by A1, MSUALG_3:2 ; :: thesis: verum