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 h being ManySortedFunction of (Free (S,X0)),A0 st h is_homomorphism Free (S,X0),A0 holds
for o being OperSymbol of S
for x being Element of Args (o,A0) holds (h . (the_result_sort_of o)) . ((Den (o,A0)) . x) = (h . (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 h being ManySortedFunction of (Free (S,X0)),A0 st h is_homomorphism Free (S,X0),A0 holds
for o being OperSymbol of S
for x being Element of Args (o,A0) holds (h . (the_result_sort_of o)) . ((Den (o,A0)) . x) = (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . x)
let A0 be X0,S -terms MSAlgebra over S; :: thesis: for h being ManySortedFunction of (Free (S,X0)),A0 st h is_homomorphism Free (S,X0),A0 holds
for o being OperSymbol of S
for x being Element of Args (o,A0) holds (h . (the_result_sort_of o)) . ((Den (o,A0)) . x) = (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . x)
set A = A0;
let h be ManySortedFunction of (Free (S,X0)),A0; :: thesis: ( h is_homomorphism Free (S,X0),A0 implies for o being OperSymbol of S
for x being Element of Args (o,A0) holds (h . (the_result_sort_of o)) . ((Den (o,A0)) . x) = (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . x) )
assume h is_homomorphism Free (S,X0),A0 ; :: thesis: for o being OperSymbol of S
for x being Element of Args (o,A0) holds (h . (the_result_sort_of o)) . ((Den (o,A0)) . x) = (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . x)
then consider g being ManySortedFunction of A0,A0 such that
A1: ( g is_homomorphism A0,A0 & h = g ** (canonical_homomorphism A0) ) by Th64;
let o be OperSymbol of S; :: thesis: for x being Element of Args (o,A0) holds (h . (the_result_sort_of o)) . ((Den (o,A0)) . x) = (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . x)
let x be Element of Args (o,A0); :: thesis: (h . (the_result_sort_of o)) . ((Den (o,A0)) . x) = (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . x)
A2: ( dom h = the carrier of S & dom (canonical_homomorphism A0) = the carrier of S ) by PARTFUN1:def 2;
A3: dom (h ** (canonical_homomorphism A0)) = (dom h) /\ (dom (canonical_homomorphism A0)) by PBOOLE:def 19;
A4: ( x in Args (o,A0) & Args (o,A0) c= Args (o,(Free (S,X0))) ) by Th40;
thus (h . (the_result_sort_of o)) . ((Den (o,A0)) . x) = (h . (the_result_sort_of o)) . (((canonical_homomorphism A0) . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . x)) by Th66
.= ((h . (the_result_sort_of o)) * ((canonical_homomorphism A0) . (the_result_sort_of o))) . ((Den (o,(Free (S,X0)))) . x) by A4, MSUALG_9:18, FUNCT_2:15
.= ((h ** (canonical_homomorphism A0)) . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . x) by A2, A3, PBOOLE:def 19
.= ((g ** ((canonical_homomorphism A0) ** (canonical_homomorphism A0))) . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . x) by A1, PBOOLE:140
.= (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . x) by A1, Th47 ; :: thesis: verum