let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for i being Element of NAT
for A being feasible MSAlgebra of S
for a being Function st a in Args o,A holds
transl o,i,a,A is Function of (the Sorts of A . ((the_arity_of o) /. i)),(the Sorts of A . (the_result_sort_of o))
let o be OperSymbol of S; :: thesis: for i being Element of NAT
for A being feasible MSAlgebra of S
for a being Function st a in Args o,A holds
transl o,i,a,A is Function of (the Sorts of A . ((the_arity_of o) /. i)),(the Sorts of A . (the_result_sort_of o))
let i be Element of NAT ; :: thesis: for A being feasible MSAlgebra of S
for a being Function st a in Args o,A holds
transl o,i,a,A is Function of (the Sorts of A . ((the_arity_of o) /. i)),(the Sorts of A . (the_result_sort_of o))
let A be feasible MSAlgebra of S; :: thesis: for a being Function st a in Args o,A holds
transl o,i,a,A is Function of (the Sorts of A . ((the_arity_of o) /. i)),(the Sorts of A . (the_result_sort_of o))
let a be Function; :: thesis: ( a in Args o,A implies transl o,i,a,A is Function of (the Sorts of A . ((the_arity_of o) /. i)),(the Sorts of A . (the_result_sort_of o)) )
assume A1: a in Args o,A ; :: thesis: transl o,i,a,A is Function of (the Sorts of A . ((the_arity_of o) /. i)),(the Sorts of A . (the_result_sort_of o))
then A2: Result o,A <> {} by Def1;
A3: dom (transl o,i,a,A) = the Sorts of A . ((the_arity_of o) /. i) by Def4;
A4: rng (transl o,i,a,A) c= the Sorts of A . (the_result_sort_of o)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (transl o,i,a,A) or x in the Sorts of A . (the_result_sort_of o) )
assume x in rng (transl o,i,a,A) ; :: thesis: x in the Sorts of A . (the_result_sort_of o)
then consider y being set such that
A5: y in dom (transl o,i,a,A) and
A6: x = (transl o,i,a,A) . y by FUNCT_1:def 5;
reconsider y = y as Element of A,((the_arity_of o) /. i) by A5, Def4;
set b = a +* i,y;
A7: (Den o,A) . (a +* i,y) in Result o,A by A1, A2, Th7, FUNCT_2:7;
x = (Den o,A) . (a +* i,y) by A3, A5, A6, Def4;
hence x in the Sorts of A . (the_result_sort_of o) by A7, PRALG_2:10; :: thesis: verum

end;

Result o,A = the Sorts of A . (the_result_sort_of o) by PRALG_2:10;
hence transl o,i,a,A is Function of (the Sorts of A . ((the_arity_of o) /. i)),(the Sorts of A . (the_result_sort_of o)) by A2, A3, A4, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum