let S be non empty non void ManySortedSign ; :: thesis: for s1, s2 being SortSymbol of S
for A being non-empty MSAlgebra over S st [s1,s2] in TranslationRel S holds
ex f being Function st f is_e.translation_of A,s1,s2
let s1, s2 be SortSymbol of S; :: thesis: for A being non-empty MSAlgebra over S st [s1,s2] in TranslationRel S holds
ex f being Function st f is_e.translation_of A,s1,s2
let A be non-empty MSAlgebra over S; :: thesis: ( [s1,s2] in TranslationRel S implies ex f being Function st f is_e.translation_of A,s1,s2 )
assume [s1,s2] in TranslationRel S ; :: thesis: ex f being Function st f is_e.translation_of A,s1,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 ) by Def3;
set a = the Element of Args (o,A);
consider i being Element of NAT such that
A3: i in dom (the_arity_of o) and
A4: (the_arity_of o) /. i = s1 by A2;
take transl (o,i, the Element of Args (o,A),A) ; :: thesis: transl (o,i, the Element of Args (o,A),A) is_e.translation_of A,s1,s2
take o ; :: according to MSUALG_6:def 5 :: thesis: ( the_result_sort_of o = s2 & 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) & transl (o,i, the Element of Args (o,A),A) = transl (o,i,a,A) ) ) )
thus ( the_result_sort_of o = s2 & 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) & transl (o,i, the Element of Args (o,A),A) = transl (o,i,a,A) ) ) ) by A1, A3, A4; :: thesis: verum