thus
( len M = 0 implies ex z being FinSequence of D st z = {} )
( not len M = 0 implies ex b1 being FinSequence of D ex p being FinSequence of D * st
( b1 = p . (len M) & len p = len M & p . 1 = M . 1 & ( for k being Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) ) )
thus
( len M <> 0 implies ex z being FinSequence of D ex p being FinSequence of D * st
( z = p . (len M) & len p = len M & p . 1 = M . 1 & ( for k being Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) ) )
verumproof
reconsider M1 =
M . 1 as
Element of
D * by FINSEQ_1:def 11;
defpred S1[
Nat,
set ,
set ]
means ex
p1,
q1 being
Element of
D * st
(
q1 = $2 &
p1 = M . ($1 + 1) & $3
= q1 ^ p1 );
assume A1:
len M <> 0
;
ex z being FinSequence of D ex p being FinSequence of D * st
( z = p . (len M) & len p = len M & p . 1 = M . 1 & ( for k being Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) )
A2:
for
n being
Nat st 1
<= n &
n < len M holds
for
x being
Element of
D * ex
y being
Element of
D * st
S1[
n,
x,
y]
proof
let n be
Nat;
( 1 <= n & n < len M implies for x being Element of D * ex y being Element of D * st S1[n,x,y] )
assume that
1
<= n
and A3:
n < len M
;
for x being Element of D * ex y being Element of D * st S1[n,x,y]
A4:
1
<= n + 1
by NAT_1:11;
n + 1
<= len M
by A3, NAT_1:13;
then
n + 1
in dom M
by A4, FINSEQ_3:25;
then reconsider p1 =
M . (n + 1) as
Element of
D * by FINSEQ_2:11;
let x be
Element of
D * ;
ex y being Element of D * st S1[n,x,y]
set y =
x ^ p1;
reconsider y =
x ^ p1 as
Element of
D * by FINSEQ_1:def 11;
take
y
;
S1[n,x,y]
take
p1
;
ex q1 being Element of D * st
( q1 = x & p1 = M . (n + 1) & y = q1 ^ p1 )
take
x
;
( x = x & p1 = M . (n + 1) & y = x ^ p1 )
thus
(
x = x &
p1 = M . (n + 1) &
y = x ^ p1 )
;
verum
end;
ex
p being
FinSequence of
D * st
(
len p = len M & (
p . 1
= M1 or
len M = 0 ) & ( for
n being
Nat st 1
<= n &
n < len M holds
S1[
n,
p . n,
p . (n + 1)] ) )
from RECDEF_1:sch 4(A2);
then consider p being
FinSequence of
D * such that A5:
len p = len M
and A6:
(
p . 1
= M1 or
len M = 0 )
and A7:
for
n being
Nat st 1
<= n &
n < len M holds
S1[
n,
p . n,
p . (n + 1)]
;
reconsider z =
p . (len M) as
FinSequence of
D ;
take
z
;
ex p being FinSequence of D * st
( z = p . (len M) & len p = len M & p . 1 = M . 1 & ( for k being Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) )
for
n being
Nat st 1
<= n &
n < len M holds
p . (n + 1) = (p . n) ^ (M . (n + 1))
proof
let n be
Nat;
( 1 <= n & n < len M implies p . (n + 1) = (p . n) ^ (M . (n + 1)) )
assume that A8:
1
<= n
and A9:
n < len M
;
p . (n + 1) = (p . n) ^ (M . (n + 1))
ex
p1,
q1 being
Element of
D * st
(
q1 = p . n &
p1 = M . (n + 1) &
p . (n + 1) = q1 ^ p1 )
by A7, A8, A9;
hence
p . (n + 1) = (p . n) ^ (M . (n + 1))
;
verum
end;
hence
ex
p being
FinSequence of
D * st
(
z = p . (len M) &
len p = len M &
p . 1
= M . 1 & ( for
k being
Nat st
k >= 1 &
k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) )
by A1, A5, A6;
verum
end;