let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for R being stable ManySortedRelation of A
for s being SortSymbol of S
for a, b being Element of A,s st a,b are_convertible_wrt R . s holds
for h being Endomorphism of A holds (h . s) . a,(h . s) . b are_convertible_wrt R . s
let A be non-empty MSAlgebra over S; :: thesis: for R being stable ManySortedRelation of A
for s being SortSymbol of S
for a, b being Element of A,s st a,b are_convertible_wrt R . s holds
for h being Endomorphism of A holds (h . s) . a,(h . s) . b are_convertible_wrt R . s
let R be stable ManySortedRelation of A; :: thesis: for s being SortSymbol of S
for a, b being Element of A,s st a,b are_convertible_wrt R . s holds
for h being Endomorphism of A holds (h . s) . a,(h . s) . b are_convertible_wrt R . s
let s be SortSymbol of S; :: thesis: for a, b being Element of A,s st a,b are_convertible_wrt R . s holds
for h being Endomorphism of A holds (h . s) . a,(h . s) . b are_convertible_wrt R . s
let a, b be Element of A,s; :: thesis: ( a,b are_convertible_wrt R . s implies for h being Endomorphism of A holds (h . s) . a,(h . s) . b are_convertible_wrt R . s )
assume (R . s) \/ ((R . s) ~) reduces a,b ; :: according to REWRITE1:def 4 :: thesis: for h being Endomorphism of A holds (h . s) . a,(h . s) . b are_convertible_wrt R . s
then consider p being RedSequence of (R . s) \/ ((R . s) ~) such that
A1: p . 1 = a and
A2: p . (len p) = b ;
let h be Endomorphism of A; :: thesis: (h . s) . a,(h . s) . b are_convertible_wrt R . s
defpred S₁[ Nat] means ( $1 in dom p implies (h . s) . a,(h . s) . (p . $1) are_convertible_wrt R . s );
A3: 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
A4: ( i in dom p implies (h . s) . a,(h . s) . (p . i) are_convertible_wrt R . s ) and
A5: i + 1 in dom p ; :: thesis: (h . s) . a,(h . s) . (p . (i + 1)) are_convertible_wrt R . s
A6: i <= i + 1 by NAT_1:11;
i + 1 <= len p by A5, FINSEQ_3:25;
then A7: i <= len p by A6, XXREAL_0:2;

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

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

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

end;

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

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

end;

end;

end;

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