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 A4, XXREAL_0:1;
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 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
end;
F2 . 1 = Al by A7, A10, FINSEQ_1:64;
hence S1[k + 1] by A15, A17; :: 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