consider q being RedSequence of TranslationRel S such that
A2:
q . 1 = s1
and
A3:
q . (len q) = s2
by A1;
defpred S1[ object , object ] means ex f being Function ex s1, s2 being SortSymbol of S ex i being Element of NAT st
( $2 = f & i = $1 & s1 = q . i & s2 = q . (i + 1) & f is_e.translation_of A,s1,s2 );
len q >= 0 + 1
by NAT_1:13;
then consider n being Nat such that
A4:
len q = 1 + n
by NAT_1:10;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
A5:
dom q = Seg (len q)
by FINSEQ_1:def 3;
A6:
for x being object st x in Seg n holds
ex y being object st S1[x,y]
proof
let x be
object ;
( x in Seg n implies ex y being object st S1[x,y] )
assume A7:
x in Seg n
;
ex y being object st S1[x,y]
then reconsider i =
x as
Element of
NAT ;
A8:
i <= n
by A7, FINSEQ_1:1;
then A9:
i + 1
<= len q
by A4, XREAL_1:6;
A10:
i >= 1
by A7, FINSEQ_1:1;
then
i + 1
>= 1
by NAT_1:13;
then A11:
i + 1
in dom q
by A5, A9, FINSEQ_1:1;
i <= n + 1
by A8, NAT_1:13;
then
i in dom q
by A4, A5, A10, FINSEQ_1:1;
then A12:
[(q . i),(q . (i + 1))] in TranslationRel S
by A11, REWRITE1:def 2;
then reconsider s1 =
q . i,
s2 =
q . (i + 1) as
SortSymbol of
S by ZFMISC_1:87;
consider o being
OperSymbol of
S such that A13:
the_result_sort_of o = s2
and A14:
ex
i being
Element of
NAT st
(
i in dom (the_arity_of o) &
(the_arity_of o) /. i = s1 )
by A12, Def3;
set a = the
Element of
Args (
o,
A);
consider j being
Element of
NAT such that A15:
j in dom (the_arity_of o)
and A16:
(the_arity_of o) /. j = s1
by A14;
take
transl (
o,
j, the
Element of
Args (
o,
A),
A)
;
S1[x, transl (o,j, the Element of Args (o,A),A)]
take
transl (
o,
j, the
Element of
Args (
o,
A),
A)
;
ex s1, s2 being SortSymbol of S ex i being Element of NAT st
( transl (o,j, the Element of Args (o,A),A) = transl (o,j, the Element of Args (o,A),A) & i = x & s1 = q . i & s2 = q . (i + 1) & transl (o,j, the Element of Args (o,A),A) is_e.translation_of A,s1,s2 )
take
s1
;
ex s2 being SortSymbol of S ex i being Element of NAT st
( transl (o,j, the Element of Args (o,A),A) = transl (o,j, the Element of Args (o,A),A) & i = x & s1 = q . i & s2 = q . (i + 1) & transl (o,j, the Element of Args (o,A),A) is_e.translation_of A,s1,s2 )
take
s2
;
ex i being Element of NAT st
( transl (o,j, the Element of Args (o,A),A) = transl (o,j, the Element of Args (o,A),A) & i = x & s1 = q . i & s2 = q . (i + 1) & transl (o,j, the Element of Args (o,A),A) is_e.translation_of A,s1,s2 )
take
i
;
( transl (o,j, the Element of Args (o,A),A) = transl (o,j, the Element of Args (o,A),A) & i = x & s1 = q . i & s2 = q . (i + 1) & transl (o,j, the Element of Args (o,A),A) is_e.translation_of A,s1,s2 )
thus
(
transl (
o,
j, the
Element of
Args (
o,
A),
A)
= transl (
o,
j, the
Element of
Args (
o,
A),
A) &
i = x &
s1 = q . i &
s2 = q . (i + 1) &
transl (
o,
j, the
Element of
Args (
o,
A),
A)
is_e.translation_of A,
s1,
s2 )
by A13, A15, A16;
verum
end;
consider p being Function such that
A17:
( dom p = Seg n & ( for x being object st x in Seg n holds
S1[x,p . x] ) )
from CLASSES1:sch 1(A6);
p is Function-yielding
then reconsider p = p as Function-yielding FinSequence by A17, FINSEQ_1:def 2;
A18:
now 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,s2let i be
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,s2let f be
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,s2let s1,
s2 be
SortSymbol of
S;
( i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) implies f is_e.translation_of A,s1,s2 )assume
i in dom p
;
( f = p . i & s1 = q . i & s2 = q . (i + 1) implies f is_e.translation_of A,s1,s2 )then
ex
f being
Function ex
s1,
s2 being
SortSymbol of
S ex
j being
Element of
NAT st
(
p . i = f &
j = i &
s1 = q . j &
s2 = q . (j + 1) &
f is_e.translation_of A,
s1,
s2 )
by A17;
hence
(
f = p . i &
s1 = q . i &
s2 = q . (i + 1) implies
f is_e.translation_of A,
s1,
s2 )
;
verum end;
len p = n
by A17, FINSEQ_1:def 3;
then reconsider t = compose (p,( the Sorts of A . s1)) as Function of ( the Sorts of A . s1),( the Sorts of A . s2) by A2, A3, A4, A18, Th14;
take
t
; ex q being RedSequence of TranslationRel S ex p being Function-yielding FinSequence st
( t = compose (p,( the Sorts of A . s1)) & 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 ) )
take
q
; ex p being Function-yielding FinSequence st
( t = compose (p,( the Sorts of A . s1)) & 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 ) )
take
p
; ( t = compose (p,( the Sorts of A . s1)) & 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 ) )
thus
( t = compose (p,( the Sorts of A . s1)) & 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 ) )
by A2, A3, A4, A17, A18, FINSEQ_1:def 3; verum