let S be non empty non void ManySortedSign ; :: thesis: for s1, s2 being SortSymbol of S
for A being feasible MSAlgebra over S
for f being Function st f is_e.translation_of A,s1,s2 holds
( f is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} )
let s1, s2 be SortSymbol of S; :: thesis: for A being feasible MSAlgebra over S
for f being Function st f is_e.translation_of A,s1,s2 holds
( f is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} )
let A be feasible MSAlgebra over S; :: thesis: for f being Function st f is_e.translation_of A,s1,s2 holds
( f is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} )
let f be Function; :: thesis: ( f is_e.translation_of A,s1,s2 implies ( f is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) )
assume f is_e.translation_of A,s1,s2 ; :: thesis: ( f is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} )
then consider o being OperSymbol of S such that
A1: the_result_sort_of o = s2 and
A2: ex i being Element of NAT st
( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 & ex a being Function st
( a in Args (o,A) & f = transl (o,i,a,A) ) ) ;
Result (o,A) = the Sorts of A . (the_result_sort_of o) by PRALG_2:3;
hence ( f is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) by A1, A2, Def1, Th3, Th10; :: thesis: verum