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,(Free (S,X0))) holds (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . x) = (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . ((canonical_homomorphism A0) # 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,(Free (S,X0))) holds (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . x) = (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . ((canonical_homomorphism A0) # 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,(Free (S,X0))) holds (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . x) = (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . ((canonical_homomorphism A0) # 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,(Free (S,X0))) holds (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . x) = (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . ((canonical_homomorphism A0) # x)) )
assume h is_homomorphism Free (S,X0),A0 ; :: thesis: for o being OperSymbol of S
for x being Element of Args (o,(Free (S,X0))) holds (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . x) = (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . ((canonical_homomorphism A0) # 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,(Free (S,X0))) holds (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . x) = (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . ((canonical_homomorphism A0) # x))
let x be Element of Args (o,(Free (S,X0))); :: thesis: (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . x) = (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . ((canonical_homomorphism A0) # x))
set k = canonical_homomorphism A0;
A2: ( (canonical_homomorphism A0) # 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,(Free (S,X0)))) . x) = ((g . (the_result_sort_of o)) * ((canonical_homomorphism A0) . (the_result_sort_of o))) . ((Den (o,(Free (S,X0)))) . x) by A1, MSUALG_3:2
.= (g . (the_result_sort_of o)) . (((canonical_homomorphism A0) . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . x)) by MSUALG_9:18, FUNCT_2:15
.= (g . (the_result_sort_of o)) . ((Den (o,A0)) . ((canonical_homomorphism A0) # x)) by Def7, MSUALG_3:def 7
.= (g . (the_result_sort_of o)) . (((canonical_homomorphism A0) . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . ((canonical_homomorphism A0) # x))) by Th66
.= ((g . (the_result_sort_of o)) * ((canonical_homomorphism A0) . (the_result_sort_of o))) . ((Den (o,(Free (S,X0)))) . ((canonical_homomorphism A0) # x)) by A2, MSUALG_9:18, FUNCT_2:15
.= (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . ((canonical_homomorphism A0) # x)) by A1, MSUALG_3:2 ; :: thesis: verum