let S be non empty non void ManySortedSign ; :: thesis: for A1, A2 being non-empty MSAlgebra of S
for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
for o being OperSymbol of S
for i being Element of NAT st i in dom (the_arity_of o) holds
for a being Element of Args o,A1 holds (h . (the_result_sort_of o)) * (transl o,i,a,A1) = (transl o,i,(h # a),A2) * (h . ((the_arity_of o) /. i))
let A1, A2 be non-empty MSAlgebra of S; :: thesis: for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
for o being OperSymbol of S
for i being Element of NAT st i in dom (the_arity_of o) holds
for a being Element of Args o,A1 holds (h . (the_result_sort_of o)) * (transl o,i,a,A1) = (transl o,i,(h # a),A2) * (h . ((the_arity_of o) /. i))
let h be ManySortedFunction of A1,A2; :: thesis: ( h is_homomorphism A1,A2 implies for o being OperSymbol of S
for i being Element of NAT st i in dom (the_arity_of o) holds
for a being Element of Args o,A1 holds (h . (the_result_sort_of o)) * (transl o,i,a,A1) = (transl o,i,(h # a),A2) * (h . ((the_arity_of o) /. i)) )
assume A1: h is_homomorphism A1,A2 ; :: thesis: for o being OperSymbol of S
for i being Element of NAT st i in dom (the_arity_of o) holds
for a being Element of Args o,A1 holds (h . (the_result_sort_of o)) * (transl o,i,a,A1) = (transl o,i,(h # a),A2) * (h . ((the_arity_of o) /. i))
let o be OperSymbol of S; :: thesis: for i being Element of NAT st i in dom (the_arity_of o) holds
for a being Element of Args o,A1 holds (h . (the_result_sort_of o)) * (transl o,i,a,A1) = (transl o,i,(h # a),A2) * (h . ((the_arity_of o) /. i))
let i be Element of NAT ; :: thesis: ( i in dom (the_arity_of o) implies for a being Element of Args o,A1 holds (h . (the_result_sort_of o)) * (transl o,i,a,A1) = (transl o,i,(h # a),A2) * (h . ((the_arity_of o) /. i)) )
assume A2: i in dom (the_arity_of o) ; :: thesis: for a being Element of Args o,A1 holds (h . (the_result_sort_of o)) * (transl o,i,a,A1) = (transl o,i,(h # a),A2) * (h . ((the_arity_of o) /. i))
let a be Element of Args o,A1; :: thesis: (h . (the_result_sort_of o)) * (transl o,i,a,A1) = (transl o,i,(h # a),A2) * (h . ((the_arity_of o) /. i))
set s1 = (the_arity_of o) /. i;
set s2 = the_result_sort_of o;
reconsider T = transl o,i,(h # a),A2 as Function of (the Sorts of A2 . ((the_arity_of o) /. i)),(the Sorts of A2 . (the_result_sort_of o)) by Th10;
reconsider t = transl o,i,a,A1 as Function of (the Sorts of A1 . ((the_arity_of o) /. i)),(the Sorts of A1 . (the_result_sort_of o)) by Th10;

now

let x be Element of A1,((the_arity_of o) /. i); :: thesis: ((h . (the_result_sort_of o)) * t) . x = (T * (h . ((the_arity_of o) /. i))) . x
reconsider b = a +* i,x as Element of Args o,A1 by Th7;
A3: h # b = (h # a) +* i,((h # b) . i) by A2, Th9;
h # a in Args o,A2 ;
then A4: (h # b) . i = (h . ((the_arity_of o) /. i)) . x by A2, Th9;
thus ((h . (the_result_sort_of o)) * t) . x = (h . (the_result_sort_of o)) . (t . x) by FUNCT_2:21
.= (h . (the_result_sort_of o)) . ((Den o,A1) . b) by Def4
.= (Den o,A2) . ((h # a) +* i,((h . ((the_arity_of o) /. i)) . x)) by A1, A4, A3, MSUALG_3:def 9
.= T . ((h . ((the_arity_of o) /. i)) . x) by Def4
.= (T * (h . ((the_arity_of o) /. i))) . x by FUNCT_2:21 ; :: thesis: verum

end;

hence (h . (the_result_sort_of o)) * (transl o,i,a,A1) = (transl o,i,(h # a),A2) * (h . ((the_arity_of o) /. i)) by FUNCT_2:113; :: thesis: verum