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 Element of 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 Element of NAT st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) ) ) :: thesis: verum

proof

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 Element of NAT st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) )
defpred S₁[ Element of NAT , set , set ] means ex p1, q1 being Element of D * st
( q1 = $2 & p1 = M . ($1 + 1) & $3 = q1 ^ p1 );
reconsider M1 = M . 1 as Element of D * by FINSEQ_1:def 11;
A2: for n being Element of 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 Element of 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 A3: ( 1 <= n & n < len M ) ; :: thesis: for x being Element of D * ex y being Element of D * st S₁[n,x,y]
let x be Element of D * ; :: thesis: 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:27;
then reconsider p1 = M . (n + 1) as Element of D * by FINSEQ_2:13;
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 Element of 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 Element of NAT st 1 <= n & n < len M holds
S₁[n,p . n,p . (n + 1)] ;
A8: for n being Element of NAT st 1 <= n & n < len M holds
p . (n + 1) = (p . n) ^ (M . (n + 1))

proof

let n be Element of NAT ; :: thesis: ( 1 <= n & n < len M implies p . (n + 1) = (p . n) ^ (M . (n + 1)) )
assume A9: ( 1 <= n & n < len M ) ; :: thesis: p . (n + 1) = (p . n) ^ (M . (n + 1))
consider p1, q1 being Element of D * such that
A10: ( q1 = p . n & p1 = M . (n + 1) & p . (n + 1) = q1 ^ p1 ) by A7, A9;
thus p . (n + 1) = (p . n) ^ (M . (n + 1)) by A10; :: thesis: verum

end;

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 Element of NAT st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) )
thus ex p being FinSequence of D * st
( z = p . (len M) & len p = len M & p . 1 = M . 1 & ( for k being Element of NAT st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) ) by A1, A5, A6, A8; :: thesis: verum

end;