let S be non empty non void ManySortedSign ; :: thesis: for s1, s2 being SortSymbol of S
for A being feasible MSAlgebra of 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 of 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 of 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 ) ) by Def5;
Result o,A = the Sorts of A . (the_result_sort_of o) by PRALG_2:10;
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