let S be non empty non void ManySortedSign ; :: thesis: for s1, s2 being SortSymbol of S
for A being MSAlgebra of S
for f being Function st f is_e.translation_of A,s1,s2 holds
[s1,s2] in TranslationRel S
let s1, s2 be SortSymbol of S; :: thesis: for A being MSAlgebra of S
for f being Function st f is_e.translation_of A,s1,s2 holds
[s1,s2] in TranslationRel S
let A be MSAlgebra of S; :: thesis: for f being Function st f is_e.translation_of A,s1,s2 holds
[s1,s2] in TranslationRel S
let f be Function; :: thesis: ( f is_e.translation_of A,s1,s2 implies [s1,s2] in TranslationRel S )
assume f is_e.translation_of A,s1,s2 ; :: thesis: [s1,s2] in TranslationRel S
then ex o being OperSymbol of S st
( 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 & f = transl o,i,a,A ) ) ) by Def5;
hence [s1,s2] in TranslationRel S by Def3; :: thesis: verum