let Al be QC-alphabet ; :: thesis: for k being Nat holds FCEx (k -th_FCEx Al) = (k + 1) -th_FCEx Al
let k be Nat; :: thesis: 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; :: thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; :: thesis: S1[n + 1]
per cases ( n + 1 <= k + 1 or not n + 1 <= k + 1 ) ;
suppose A5: n + 1 <= k + 1 ; :: thesis: S1[n + 1]
per cases ( n = 0 or n <> 0 ) ;
suppose A6: n = 0 ; :: thesis: S1[n + 1]
the FCEx-Sequence of Al,k . 1 = Al by Def7
.= the FCEx-Sequence of Al,k + 1 . 1 by Def7 ;
hence S1[n + 1] by A6; :: thesis: verum
end;
suppose A7: n <> 0 ; :: thesis: 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; :: thesis: verum
end;
end;
end;
suppose not n + 1 <= k + 1 ; :: thesis: S1[n + 1]
hence S1[n + 1] ; :: thesis: verum
end;
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 ; :: thesis: verum
end;
hence FCEx (k -th_FCEx Al) = (k + 1) -th_FCEx Al by A1; :: thesis: verum