let Al be QC-alphabet ; :: thesis: for k being Element of NAT st k > 0 holds
ex F being b1 -element FinSequence st
( ( for n being Nat st n <= k & 1 <= n holds
F . n is QC-alphabet ) & F . 1 = Al & ( for n being Nat st n < k & 1 <= n holds
ex Al2 being QC-alphabet st
( F . n = Al2 & F . (n + 1) = FCEx Al2 ) ) )

defpred S1[ Nat] means ( \$1 > 0 implies ex F being \$1 -element FinSequence st
( ( for n being Nat st n <= \$1 & 1 <= n holds
F . n is QC-alphabet ) & F . 1 = Al & ( for n being Nat st n < \$1 & 1 <= n holds
ex Al2 being QC-alphabet st
( F . n = Al2 & F . (n + 1) = FCEx Al2 ) ) ) );
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; :: thesis: S1[k + 1]
per cases ( k = 0 or k <> 0 ) ;
suppose A3: k = 0 ; :: thesis: S1[k + 1]
A4: ( <*Al*> is 1 -element FinSequence & <*Al*> . 1 = Al ) by FINSEQ_1:40;
A5: for n being Nat st n < 1 & 1 <= n holds
ex Al2 being QC-alphabet st
( <*Al*> . n = Al2 & <*Al*> . (n + 1) = FCEx Al2 ) ;
for n being Nat st n <= 1 & 1 <= n holds
<*Al*> . n is QC-alphabet by ;
hence S1[k + 1] by A3, A4, A5; :: thesis: verum
end;
suppose A6: k <> 0 ; :: thesis: S1[k + 1]
then consider F being k -element FinSequence such that
A7: ( ( for n being Nat st n <= k & 1 <= n holds
F . n is QC-alphabet ) & F . 1 = Al & ( for n being Nat st n < k & 1 <= n holds
ex Al2 being QC-alphabet st
( F . n = Al2 & F . (n + 1) = FCEx Al2 ) ) ) by A2;
set K = F . k;
F . k is QC-alphabet
proof
per cases ( k = 1 or k <> 1 ) ;
suppose A8: k <> 1 ; :: thesis: F . k is QC-alphabet
consider j being Nat such that
A9: k = j + 1 by ;
j <> 0 by A8, A9;
then ( j >= 1 & j < k ) by ;
then ex Al2 being QC-alphabet st
( F . j = Al2 & F . k = FCEx Al2 ) by A7, A9;
hence F . k is QC-alphabet ; :: thesis: verum
end;
end;
end;
then reconsider K = F . k as QC-alphabet ;
set K2 = <*(FCEx K)*>;
set F2 = F ^ <*(FCEx K)*>;
reconsider F2 = F ^ <*(FCEx K)*> as k + 1 -element FinSequence ;
A10: ( 1 <= k & len F = k ) by ;
A11: for n being Nat st n < k & 1 <= n holds
ex Al2 being QC-alphabet st
( F2 . n = Al2 & F2 . (n + 1) = FCEx Al2 )
proof
let n be Nat; :: thesis: ( n < k & 1 <= n implies ex Al2 being QC-alphabet st
( F2 . n = Al2 & F2 . (n + 1) = FCEx Al2 ) )

assume A12: ( n < k & 1 <= n ) ; :: thesis: ex Al2 being QC-alphabet st
( F2 . n = Al2 & F2 . (n + 1) = FCEx Al2 )

consider Al2 being QC-alphabet such that
A13: ( F . n = Al2 & F . (n + 1) = FCEx Al2 ) by ;
( 1 <= n + 1 & n + 1 <= k & k = len F ) by ;
then ( F2 . n = F . n & F2 . (n + 1) = F . (n + 1) ) by ;
hence ex Al2 being QC-alphabet st
( F2 . n = Al2 & F2 . (n + 1) = FCEx Al2 ) by A13; :: thesis: verum
end;
A14: ( K is QC-alphabet & F2 . k = K ) by ;
A15: for n being Nat st n < k + 1 & 1 <= n holds
ex Al2 being QC-alphabet st
( F2 . n = Al2 & F2 . (n + 1) = FCEx Al2 )
proof
let n be Nat; :: thesis: ( n < k + 1 & 1 <= n implies ex Al2 being QC-alphabet st
( F2 . n = Al2 & F2 . (n + 1) = FCEx Al2 ) )

assume A16: ( n < k + 1 & 1 <= n ) ; :: thesis: ex Al2 being QC-alphabet st
( F2 . n = Al2 & F2 . (n + 1) = FCEx Al2 )

per cases ( n <> k or n = k ) ;
suppose n <> k ; :: thesis: ex Al2 being QC-alphabet st
( F2 . n = Al2 & F2 . (n + 1) = FCEx Al2 )

hence ex Al2 being QC-alphabet st
( F2 . n = Al2 & F2 . (n + 1) = FCEx Al2 ) by ; :: thesis: verum
end;
suppose n = k ; :: thesis: ex Al2 being QC-alphabet st
( F2 . n = Al2 & F2 . (n + 1) = FCEx Al2 )

hence ex Al2 being QC-alphabet st
( F2 . n = Al2 & F2 . (n + 1) = FCEx Al2 ) by ; :: thesis: verum
end;
end;
end;
A17: for n being Nat st n <= k + 1 & 1 <= n holds
F2 . n is QC-alphabet
proof
let n be Nat; :: thesis: ( n <= k + 1 & 1 <= n implies F2 . n is QC-alphabet )
assume A18: ( n <= k + 1 & 1 <= n ) ; :: thesis: F2 . n is QC-alphabet
per cases ( n <> k + 1 or n = k + 1 ) ;
suppose n <> k + 1 ; :: thesis: F2 . n is QC-alphabet
then n <= k by ;
then ( F2 . n = F . n & F . n is QC-alphabet ) by ;
hence F2 . n is QC-alphabet ; :: thesis: verum
end;
suppose n = k + 1 ; :: thesis: F2 . n is QC-alphabet
hence F2 . n is QC-alphabet by ; :: thesis: verum
end;
end;
end;
F2 . 1 = Al by ;
hence S1[k + 1] by ; :: thesis: verum
end;
end;
end;
A19: S1[ 0 ] ;
for n being Nat holds S1[n] from NAT_1:sch 2(A19, A1);
hence for k being Element of NAT st k > 0 holds
ex F being b1 -element FinSequence st
( ( for n being Nat st n <= k & 1 <= n holds
F . n is QC-alphabet ) & F . 1 = Al & ( for n being Nat st n < k & 1 <= n holds
ex Al2 being QC-alphabet st
( F . n = Al2 & F . (n + 1) = FCEx Al2 ) ) ) ; :: thesis: verum