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 over 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 over 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 over 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 over 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 object ; :: 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 object such that
A5: y in dom (transl (o,i,a,A)) and
A6: x = (transl (o,i,a,A)) . y by FUNCT_1:def 3;
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:5;
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:3; :: thesis: verum

end;

Result (o,A) = the Sorts of A . (the_result_sort_of o) by PRALG_2:3;
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:4; :: thesis: verum