let Al be QC-alphabet ; :: thesis: for k being Element of NAT st k > 0 holds
ex F being b₁ -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 S₁[ 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 S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]

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

suppose A3: k = 0 ; :: thesis: S₁[k + 1]

A4: ( <*Al*> is 1 -element FinSequence & <*Al*> . 1 = Al ) ;
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 A4, XXREAL_0:1;
hence S₁[k + 1] by A3, A4, A5; :: thesis: verum

end;

suppose A6: k <> 0 ; :: thesis: S₁[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 k = 1 ; :: thesis: F . k is QC-alphabet

hence F . k is QC-alphabet by A7; :: thesis: verum

end;

suppose A8: k <> 1 ; :: thesis: F . k is QC-alphabet

consider j being Nat such that
A9: k = j + 1 by NAT_1:6, A6;
j <> 0 by A8, A9;
then ( j >= 1 & j < k ) by A9, NAT_1:25, NAT_1:19;
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 A6, NAT_1:25, CARD_1:def 7;
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 A7, A12;
( 1 <= n + 1 & n + 1 <= k & k = len F ) by A12, NAT_1:13, CARD_1:def 7;
then ( F2 . n = F . n & F2 . (n + 1) = F . (n + 1) ) by A12, FINSEQ_1:64;
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 A10, FINSEQ_1:64;
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 A11, A16, NAT_1:22; :: 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 A10, A14, FINSEQ_1:42; :: 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 A18, NAT_1:8;
then ( F2 . n = F . n & F . n is QC-alphabet ) by A7, A10, A18, FINSEQ_1:64;
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 A10, FINSEQ_1:42; :: thesis: verum

end;

end;

end;

F2 . 1 = Al by A7, A10, FINSEQ_1:64;
hence S₁[k + 1] by A15, A17; :: thesis: verum

end;

end;

end;

A19: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A19, A1);
hence for k being Element of NAT st k > 0 holds
ex F being b₁ -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