thus ( len M = 0 implies ex z being FinSequence of D st z = {} ) :: thesis: ( not len M = 0 implies ex b₁ being FinSequence of D ex p being FinSequence of D * st
( b₁ = 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)) ) ) )

proof

assume len M = 0 ; :: thesis: ex z being FinSequence of D st z = {}
<*> D = {} ;
hence ex z being FinSequence of D st z = {} ; :: thesis: verum

end;

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)) ) ) ) :: thesis: verum

proof

reconsider M1 = M . 1 as Element of D * by FINSEQ_1:def 11;
defpred S₁[ 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 ; :: thesis: 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 S₁[n,x,y]

proof

let n be Nat; :: thesis: ( 1 <= n & n < len M implies for x being Element of D * ex y being Element of D * st S₁[n,x,y] )
assume that
1 <= n and
A3: n < len M ; :: thesis: for x being Element of D * ex y being Element of D * st S₁[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 * ; :: thesis: ex y being Element of D * st S₁[n,x,y]
set y = x ^ p1;
reconsider y = x ^ p1 as Element of D * by FINSEQ_1:def 11;
take y ; :: thesis: S₁[n,x,y]
take p1 ; :: thesis: ex q1 being Element of D * st
( q1 = x & p1 = M . (n + 1) & y = q1 ^ p1 )
take x ; :: thesis: ( x = x & p1 = M . (n + 1) & y = x ^ p1 )
thus ( x = x & p1 = M . (n + 1) & y = x ^ p1 ) ; :: thesis: 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
S₁[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
S₁[n,p . n,p . (n + 1)] ;
reconsider z = p . (len M) as FinSequence of D ;
take z ; :: thesis: 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; :: thesis: ( 1 <= n & n < len M implies p . (n + 1) = (p . n) ^ (M . (n + 1)) )
assume that
A8: 1 <= n and
A9: n < len M ; :: thesis: 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)) ; :: thesis: 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; :: thesis: verum

end;