let z1, z2 be FinSequence of D; :: thesis: ( ( len M = 0 & z1 = {} & z2 = {} implies z1 = z2 ) & ( not len M = 0 & ex p being FinSequence of D * st
( z1 = 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)) ) ) & ex p being FinSequence of D * st
( z2 = 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)) ) ) implies z1 = z2 ) )
thus ( len M = 0 & z1 = {} & z2 = {} implies z1 = z2 ) ; :: thesis: ( not len M = 0 & ex p being FinSequence of D * st
( z1 = 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)) ) ) & ex p being FinSequence of D * st
( z2 = 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)) ) ) implies z1 = z2 )
assume len M <> 0 ; :: thesis: ( for p being FinSequence of D * holds
( not z1 = p . (len M) or not len p = len M or not p . 1 = M . 1 or ex k being Nat st
( k >= 1 & k < len M & not p . (k + 1) = (p . k) ^ (M . (k + 1)) ) ) or for p being FinSequence of D * holds
( not z2 = p . (len M) or not len p = len M or not p . 1 = M . 1 or ex k being Nat st
( k >= 1 & k < len M & not p . (k + 1) = (p . k) ^ (M . (k + 1)) ) ) or z1 = z2 )
then A10: len M >= 1 by NAT_1:14;
given p1 being FinSequence of D * such that A11: z1 = p1 . (len M) and
len p1 = len M and
A12: p1 . 1 = M . 1 and
A13: for k being Nat st k >= 1 & k < len M holds
p1 . (k + 1) = (p1 . k) ^ (M . (k + 1)) ; :: thesis: ( for p being FinSequence of D * holds
( not z2 = p . (len M) or not len p = len M or not p . 1 = M . 1 or ex k being Nat st
( k >= 1 & k < len M & not p . (k + 1) = (p . k) ^ (M . (k + 1)) ) ) or z1 = z2 )
given p2 being FinSequence of D * such that A14: z2 = p2 . (len M) and
len p2 = len M and
A15: p2 . 1 = M . 1 and
A16: for k being Nat st k >= 1 & k < len M holds
p2 . (k + 1) = (p2 . k) ^ (M . (k + 1)) ; :: thesis: z1 = z2
for k being Nat st k >= 1 & k <= len M holds
p1 . k = p2 . k

proof

defpred S₁[ Nat] means ( $1 >= 1 & $1 <= len M implies p1 . $1 = p2 . $1 );
A17: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A18: ( n >= 1 & n <= len M implies p1 . n = p2 . n ) ; :: thesis: S₁[n + 1]
assume that
n + 1 >= 1 and
A19: n + 1 <= len M ; :: thesis: p1 . (n + 1) = p2 . (n + 1)

now :: thesis: p1 . (n + 1) = p2 . (n + 1)

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: p1 . (n + 1) = p2 . (n + 1)

hence p1 . (n + 1) = p2 . (n + 1) by A12, A15; :: thesis: verum

end;

suppose A20: n <> 0 ; :: thesis: p1 . (n + 1) = p2 . (n + 1)

A21: n < len M by A19, NAT_1:13;
hence p1 . (n + 1) = (p2 . n) ^ (M . (n + 1)) by A13, A18, A20, NAT_1:14
.= p2 . (n + 1) by A16, A20, A21, NAT_1:14 ;
:: thesis: verum

end;

end;

end;

hence p1 . (n + 1) = p2 . (n + 1) ; :: thesis: verum

end;

A22: S₁[ 0 ] ;
thus for n being Nat holds S₁[n] from NAT_1:sch 2(A22, A17); :: thesis: verum

end;

hence z1 = z2 by A10, A11, A14; :: thesis: verum