let S be non empty non void ManySortedSign ; 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; 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; 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; 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; ( 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
; REWRITE1:def 4 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; (h . s) . a,(h . s) . b are_convertible_wrt R . s
defpred S1[ 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 S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[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
;
(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
;
(h . s) . a,(h . s) . (p . (i + 1)) are_convertible_wrt R . sthen 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;
verum end; end;
end;
A10:
len p in dom p
by FINSEQ_5:6;
A11:
S1[ 0 ]
by FINSEQ_3:25;
for i being Nat holds S1[i]
from NAT_1:sch 2(A11, A3);
hence
(h . s) . a,(h . s) . b are_convertible_wrt R . s
by A2, A10; verum