let S be non empty non void ManySortedSign ; :: thesis: for s1, s2 being SortSymbol of S
for A being non-empty MSAlgebra of 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 of 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 of 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;
consider i being Element of NAT such that
A3: ( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 ) by A2;
consider a being Element of Args o,A;
take transl o,i,a,A ; :: thesis: transl o,i,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,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,a,A = transl o,i,a,A ) ) ) by A1, A3; :: thesis: verum