let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for R being invariant ManySortedRelation of A
for s1, s2 being SortSymbol of S
for a, b being Element of A,s1 st a,b are_convertible_wrt R . s1 holds
for t being Function st t is_e.translation_of A,s1,s2 holds
t . a,t . b are_convertible_wrt R . s2
let A be non-empty MSAlgebra over S; :: thesis: for R being invariant ManySortedRelation of A
for s1, s2 being SortSymbol of S
for a, b being Element of A,s1 st a,b are_convertible_wrt R . s1 holds
for t being Function st t is_e.translation_of A,s1,s2 holds
t . a,t . b are_convertible_wrt R . s2
let R be invariant ManySortedRelation of A; :: thesis: for s1, s2 being SortSymbol of S
for a, b being Element of A,s1 st a,b are_convertible_wrt R . s1 holds
for t being Function st t is_e.translation_of A,s1,s2 holds
t . a,t . b are_convertible_wrt R . s2
let s1, s2 be SortSymbol of S; :: thesis: for a, b being Element of A,s1 st a,b are_convertible_wrt R . s1 holds
for t being Function st t is_e.translation_of A,s1,s2 holds
t . a,t . b are_convertible_wrt R . s2
let a, b be Element of A,s1; :: thesis: ( a,b are_convertible_wrt R . s1 implies for t being Function st t is_e.translation_of A,s1,s2 holds
t . a,t . b are_convertible_wrt R . s2 )
assume (R . s1) \/ ((R . s1) ~) reduces a,b ; :: according to REWRITE1:def 4 :: thesis: for t being Function st t is_e.translation_of A,s1,s2 holds
t . a,t . b are_convertible_wrt R . s2
then consider p being RedSequence of (R . s1) \/ ((R . s1) ~) such that
A1: p . 1 = a and
A2: p . (len p) = b ;
let t be Function; :: thesis: ( t is_e.translation_of A,s1,s2 implies t . a,t . b are_convertible_wrt R . s2 )
assume A3: t is_e.translation_of A,s1,s2 ; :: thesis: t . a,t . b are_convertible_wrt R . s2
defpred S₁[ Nat] means ( $1 in dom p implies t . a,t . (p . $1) are_convertible_wrt R . s2 );
A4: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume that
A5: ( i in dom p implies t . a,t . (p . i) are_convertible_wrt R . s2 ) and
A6: i + 1 in dom p ; :: thesis: t . a,t . (p . (i + 1)) are_convertible_wrt R . s2
A7: i <= i + 1 by NAT_1:11;
i + 1 <= len p by A6, FINSEQ_3:25;
then A8: i <= len p by A7, XXREAL_0:2;

per cases ( i = 0 or i > 0 ) ;

suppose i = 0 ; :: thesis: t . a,t . (p . (i + 1)) are_convertible_wrt R . s2

hence t . a,t . (p . (i + 1)) are_convertible_wrt R . s2 by A1, REWRITE1:26; :: thesis: verum

end;

suppose i > 0 ; :: thesis: t . a,t . (p . (i + 1)) are_convertible_wrt R . s2

then A9: i >= 0 + 1 by NAT_1:13;
then i in dom p by A8, FINSEQ_3:25;
then A10: [(p . i),(p . (i + 1))] in (R . s1) \/ ((R . s1) ~) by A6, REWRITE1:def 2;
then reconsider ppi = p . i, pj = p . (i + 1) as Element of A,s1 by ZFMISC_1:87;
( [(p . i),(p . (i + 1))] in R . s1 or [(p . i),(p . (i + 1))] in (R . s1) ~ ) by A10, XBOOLE_0:def 3;
then ( [(p . i),(p . (i + 1))] in R . s1 or [(p . (i + 1)),(p . i)] in R . s1 ) by RELAT_1:def 7;
then ( [(t . ppi),(t . pj)] in R . s2 or [(t . pj),(t . ppi)] in R . s2 ) by A3, Def8;
then ( t . ppi,t . pj are_convertible_wrt R . s2 or t . pj,t . ppi are_convertible_wrt R . s2 ) by REWRITE1:29;
then t . ppi,t . pj are_convertible_wrt R . s2 by REWRITE1:31;
hence t . a,t . (p . (i + 1)) are_convertible_wrt R . s2 by A5, A8, A9, FINSEQ_3:25, REWRITE1:30; :: thesis: verum

end;

end;

end;

A11: len p in dom p by FINSEQ_5:6;
A12: S₁[ 0 ] by FINSEQ_3:25;
for i being Nat holds S₁[i] from NAT_1:sch 2(A12, A4);
hence t . a,t . b are_convertible_wrt R . s2 by A2, A11; :: thesis: verum