let Al be QC-alphabet ; for k being Nat holds FCEx (k -th_FCEx Al) = (k + 1) -th_FCEx Al
let k be Nat; FCEx (k -th_FCEx Al) = (k + 1) -th_FCEx Al
( (k + 1) + 1 <= (k + 1) + 1 & 0 < 0 + (k + 1) )
;
then
( k + 1 < k + 2 & 1 <= k + 1 )
by NAT_1:19;
then consider Al2 being QC-alphabet such that
A1:
( the FCEx-Sequence of Al,k + 1 . (k + 1) = Al2 & the FCEx-Sequence of Al,k + 1 . (k + 2) = FCEx Al2 )
by Def7;
set X = the FCEx-Sequence of Al,k + 1 . (k + 1);
the FCEx-Sequence of Al,k + 1 . (k + 1) = k -th_FCEx Al
proof
defpred S1[
Nat]
means (
0 < $1 & $1
<= k + 1 implies the
FCEx-Sequence of
Al,
k . $1
= the
FCEx-Sequence of
Al,
k + 1
. $1 );
A2:
S1[
0 ]
;
A3:
for
n being
Nat st
S1[
n] holds
S1[
n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A4:
S1[
n]
;
S1[n + 1]
per cases
( n + 1 <= k + 1 or not n + 1 <= k + 1 )
;
suppose A5:
n + 1
<= k + 1
;
S1[n + 1]per cases
( n = 0 or n <> 0 )
;
suppose A7:
n <> 0
;
S1[n + 1]A8:
(
0 < 0 + n &
n <= n + 1 )
by A7, NAT_1:11;
0 < 0 + n
by A7;
then A9:
1
<= n
by NAT_1:19;
A10:
n < k + 1
by A5, NAT_1:13;
then
n < (k + 1) + 1
by NAT_1:13;
then consider Al3 being
QC-alphabet such that A11:
( the
FCEx-Sequence of
Al,
k + 1
. n = Al3 & the
FCEx-Sequence of
Al,
k + 1
. (n + 1) = FCEx Al3 )
by A9, Def7;
consider Al4 being
QC-alphabet such that A12:
( the
FCEx-Sequence of
Al,
k . n = Al4 & the
FCEx-Sequence of
Al,
k . (n + 1) = FCEx Al4 )
by A9, A10, Def7;
thus
S1[
n + 1]
by A4, A8, A11, A12, XXREAL_0:2;
verum end;
end;
for
n being
Nat holds
S1[
n]
from NAT_1:sch 2(A2, A3);
hence
the
FCEx-Sequence of
Al,
k + 1
. (k + 1) = k -th_FCEx Al
;
verum
end;
hence
FCEx (k -th_FCEx Al) = (k + 1) -th_FCEx Al
by A1; verum