let S be non empty non void ManySortedSign ; for A being feasible MSAlgebra over S
for s1, s2 being SortSymbol of S
for q being RedSequence of TranslationRel S
for p being Function-yielding FinSequence st len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT
for f being Function
for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds
f is_e.translation_of A,s1,s2 ) holds
( compose (p,( the Sorts of A . s1)) is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & ( p <> {} implies ( the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) ) )
let A be feasible MSAlgebra over S; for s1, s2 being SortSymbol of S
for q being RedSequence of TranslationRel S
for p being Function-yielding FinSequence st len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT
for f being Function
for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds
f is_e.translation_of A,s1,s2 ) holds
( compose (p,( the Sorts of A . s1)) is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & ( p <> {} implies ( the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) ) )
let s1, s2 be SortSymbol of S; for q being RedSequence of TranslationRel S
for p being Function-yielding FinSequence st len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT
for f being Function
for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds
f is_e.translation_of A,s1,s2 ) holds
( compose (p,( the Sorts of A . s1)) is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & ( p <> {} implies ( the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) ) )
let q be RedSequence of TranslationRel S; for p being Function-yielding FinSequence st len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT
for f being Function
for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds
f is_e.translation_of A,s1,s2 ) holds
( compose (p,( the Sorts of A . s1)) is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & ( p <> {} implies ( the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) ) )
let p be Function-yielding FinSequence; ( len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT
for f being Function
for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds
f is_e.translation_of A,s1,s2 ) implies ( compose (p,( the Sorts of A . s1)) is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & ( p <> {} implies ( the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) ) ) )
assume that
A1:
len q = (len p) + 1
and
A2:
s1 = q . 1
and
A3:
s2 = q . (len q)
and
A4:
for i being Element of NAT
for f being Function
for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds
f is_e.translation_of A,s1,s2
; ( compose (p,( the Sorts of A . s1)) is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & ( p <> {} implies ( the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) ) )
per cases
( p = {} or p <> {} )
;
suppose
p <> {}
;
( compose (p,( the Sorts of A . s1)) is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & ( p <> {} implies ( the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) ) )then A7:
rng p <> {}
;
then A8:
1
in dom p
by FINSEQ_3:32;
then A9:
1
+ 1
in dom q
by A1, FUNCT_7:22;
1
in dom q
by A1, A8, FUNCT_7:22;
then
[(q . 1),(q . (1 + 1))] in TranslationRel S
by A9, REWRITE1:def 2;
then reconsider q1 =
q . 1,
q2 =
q . (1 + 1) as
SortSymbol of
S by ZFMISC_1:87;
deffunc H1(
set )
-> set = the
Sorts of
A . (q . $1);
reconsider f =
p . 1 as
Function ;
A10:
dom q = Seg (len q)
by FINSEQ_1:def 3;
consider pp being
FinSequence such that A11:
len pp = len q
and A12:
for
i being
Nat st
i in dom pp holds
pp . i = H1(
i)
from FINSEQ_1:sch 2();
defpred S1[
Nat]
means ( $1
in dom pp implies not
pp . $1 is
empty );
A13:
dom pp = Seg (len q)
by A11, FINSEQ_1:def 3;
f is_e.translation_of A,
q1,
q2
by A4, A7, FINSEQ_3:32;
then A14:
the
Sorts of
A . q1 <> {}
by Th11;
A15:
for
i being
Nat st
S1[
i] holds
S1[
i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume that
(
i in dom pp implies not
pp . i is
empty )
and A16:
i + 1
in dom pp
;
not pp . (i + 1) is empty
A17:
i <= i + 1
by NAT_1:11;
i + 1
<= len pp
by A16, FINSEQ_3:25;
then A18:
i <= len pp
by A17, XXREAL_0:2;
per cases
( i = 0 or i > 0 )
;
suppose
i > 0
;
not pp . (i + 1) is empty then
i >= 0 + 1
by NAT_1:13;
then A19:
i in dom pp
by A18, FINSEQ_3:25;
then
[(q . i),(q . (i + 1))] in TranslationRel S
by A10, A13, A16, REWRITE1:def 2;
then reconsider s1 =
q . i,
s2 =
q . (i + 1) as
SortSymbol of
S by ZFMISC_1:87;
reconsider f =
p . i as
Function ;
i in dom p
by A1, A11, A16, A19, FUNCT_7:22;
then A20:
f is_e.translation_of A,
s1,
s2
by A4;
pp . (i + 1) = the
Sorts of
A . s2
by A12, A16;
hence
not
pp . (i + 1) is
empty
by A20, Th11;
verum end;
end; A21:
S1[
0 ]
by FINSEQ_3:25;
A22:
for
i being
Nat holds
S1[
i]
from NAT_1:sch 2(A21, A15);
A23:
pp is
non-empty
by A22;
A24:
dom pp = Seg (len q)
by A11, FINSEQ_1:def 3;
reconsider pp =
pp as
non-empty non
empty FinSequence by A11, A23;
A25:
dom p = Seg (len p)
by FINSEQ_1:def 3;
p is
FuncSequence of
pp
proof
thus
(len p) + 1
= len pp
by A1, A11;
FUNCT_7:def 10 for b1 being set holds
( not b1 in dom p or p . b1 in K93((pp . b1),(pp . (b1 + 1))) )
let j be
Nat;
( not j in dom p or p . j in K93((pp . j),(pp . (j + 1))) )
reconsider f =
p . j as
Function ;
assume A26:
j in dom p
;
p . j in K93((pp . j),(pp . (j + 1)))
then A27:
j >= 1
by A25, FINSEQ_1:1;
then A28:
j + 1
>= 1
by NAT_1:13;
A29:
j <= len p
by A25, A26, FINSEQ_1:1;
then
j <= len q
by A1, NAT_1:13;
then A30:
j in Seg (len q)
by A27, FINSEQ_1:1;
j + 1
<= len q
by A1, A29, XREAL_1:6;
then A31:
j + 1
in Seg (len q)
by A28, FINSEQ_1:1;
then
[(q . j),(q . (j + 1))] in TranslationRel S
by A10, A30, REWRITE1:def 2;
then reconsider s1 =
q . j,
s2 =
q . (j + 1) as
SortSymbol of
S by ZFMISC_1:87;
A32:
pp . (j + 1) = the
Sorts of
A . s2
by A12, A24, A31;
A33:
f is_e.translation_of A,
s1,
s2
by A4, A26;
then A34:
p . j is
Function of
( the Sorts of A . s1),
( the Sorts of A . s2)
by Th11;
A35:
the
Sorts of
A . s2 <> {}
by A33, Th11;
pp . j = the
Sorts of
A . s1
by A12, A24, A30;
hence
p . j in K93(
(pp . j),
(pp . (j + 1)))
by A34, A35, A32, FUNCT_2:8;
verum
end; then reconsider p9 =
p as
FuncSequence of
pp ;
A36:
1
in dom q
by FINSEQ_5:6;
then A37:
pp . 1
= the
Sorts of
A . s1
by A2, A10, A12, A13;
then A38:
dom (compose (p9,( the Sorts of A . s1))) = the
Sorts of
A . s1
by FUNCT_7:67;
A39:
len q in dom q
by FINSEQ_5:6;
then A40:
pp . (len pp) = the
Sorts of
A . s2
by A3, A10, A11, A12, A13;
then
rng (compose (p9,( the Sorts of A . s1))) c= the
Sorts of
A . s2
by A37, FUNCT_7:67;
hence
compose (
p,
( the Sorts of A . s1)) is
Function of
( the Sorts of A . s1),
( the Sorts of A . s2)
by A10, A11, A13, A39, A40, A38, FUNCT_2:def 1, RELSET_1:4;
( p <> {} implies ( the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) )thus
(
p <> {} implies ( the
Sorts of
A . s1 <> {} & the
Sorts of
A . s2 <> {} ) )
by A10, A11, A13, A36, A39, A37, A40;
verum end;