let S be non empty non void ManySortedSign ; :: thesis: for A1, A2 being non-empty MSAlgebra over 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 over 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 :: thesis: for x being Element of A1,((the_arity_of o) /. i) holds ((h . (the_result_sort_of o)) * t) . x = (T * (h . ((the_arity_of o) /. i))) . x

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:15
.= (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
.= T . ((h . ((the_arity_of o) /. i)) . x) by Def4
.= (T * (h . ((the_arity_of o) /. i))) . x by FUNCT_2:15 ; :: 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:63; :: thesis: verum