let S be non empty non void ManySortedSign ; for X being V5() ManySortedSet of S
for A being b1,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,A) holds (h . (the_result_sort_of o)) . ((Den (o,A)) . x) = (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . x)
let X be V5() ManySortedSet of S; 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,A) holds (h . (the_result_sort_of o)) . ((Den (o,A)) . x) = (h . (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; 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,A) holds (h . (the_result_sort_of o)) . ((Den (o,A)) . x) = (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . x)
set X0 = X;
let h be ManySortedFunction of (Free (S,X)),A; ( h is_homomorphism Free (S,X),A implies for o being OperSymbol of S
for x being Element of Args (o,A) holds (h . (the_result_sort_of o)) . ((Den (o,A)) . x) = (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . x) )
assume
h is_homomorphism Free (S,X),A
; for o being OperSymbol of S
for x being Element of Args (o,A) holds (h . (the_result_sort_of o)) . ((Den (o,A)) . x) = (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . 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; for x being Element of Args (o,A) holds (h . (the_result_sort_of o)) . ((Den (o,A)) . x) = (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . x)
let x be Element of Args (o,A); (h . (the_result_sort_of o)) . ((Den (o,A)) . x) = (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . x)
A2:
( dom h = the carrier of S & dom (canonical_homomorphism A) = the carrier of S )
by PARTFUN1:def 2;
A3:
dom (h ** (canonical_homomorphism A)) = (dom h) /\ (dom (canonical_homomorphism A))
by PBOOLE:def 19;
A4:
( 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,A)) . x) =
(h . (the_result_sort_of o)) . (((canonical_homomorphism A) . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . x))
by Th67
.=
((h . (the_result_sort_of o)) * ((canonical_homomorphism A) . (the_result_sort_of o))) . ((Den (o,(Free (S,X)))) . x)
by A4, MSUALG_9:18, FUNCT_2:15
.=
((h ** (canonical_homomorphism A)) . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . x)
by A2, A3, PBOOLE:def 19
.=
((g ** ((canonical_homomorphism A) ** (canonical_homomorphism A))) . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . x)
by A1, PBOOLE:140
.=
(h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . x)
by A1, Th48
; verum