let z1, z2 be FinSequence of D; ( ( 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 )
; ( 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
; ( 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))
; ( 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))
; z1 = z2
for k being Nat st k >= 1 & k <= len M holds
p1 . k = p2 . k
proof
defpred S1[
Nat]
means ( $1
>= 1 & $1
<= len M implies
p1 . $1
= p2 . $1 );
A17:
for
n being
Nat st
S1[
n] holds
S1[
n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A18:
(
n >= 1 &
n <= len M implies
p1 . n = p2 . n )
;
S1[n + 1]
assume that
n + 1
>= 1
and A19:
n + 1
<= len M
;
p1 . (n + 1) = p2 . (n + 1)
hence
p1 . (n + 1) = p2 . (n + 1)
;
verum
end;
A22:
S1[
0 ]
;
thus
for
n being
Nat holds
S1[
n]
from NAT_1:sch 2(A22, A17); verum
end;
hence
z1 = z2
by A10, A11, A14; verum