let S be non empty non void ManySortedSign ; 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; 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; ( 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
; 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; 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 ; ( 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)
; 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); (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 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))) . xlet x be
Element of
A1,
((the_arity_of o) /. i);
((h . (the_result_sort_of o)) * t) . x = (T * (h . ((the_arity_of o) /. i))) . xreconsider 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
;
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; verum