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,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 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,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; :: 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,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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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); :: thesis: (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 ; :: thesis: verum