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