let Al be QC-alphabet ; :: thesis: for k being Element of NAT st k > 0 holds

ex F being b_{1} -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_{1}[ 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_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A19, A1);

hence for k being Element of NAT st k > 0 holds

ex F being b_{1} -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

ex F being b

( ( 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

( ( 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

S

proof

A19:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A2: S_{1}[k]
; :: thesis: S_{1}[k + 1]

end;assume A2: S

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

end;

suppose A3:
k = 0
; :: thesis: S_{1}[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 S_{1}[k + 1]
by A3, A4, A5; :: thesis: verum

end;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

suppose A6:
k <> 0
; :: thesis: S_{1}[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

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 )

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 )

F2 . n is QC-alphabet

hence S_{1}[k + 1]
by A15, A17; :: thesis: verum

end;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
end;

then reconsider K = F . k as QC-alphabet ;per cases
( k = 1 or k <> 1 )
;

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;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

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

A14:
( K is QC-alphabet & F2 . k = K )
by A10, FINSEQ_1:64;
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;( 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

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

A17:
for n being Nat st n <= k + 1 & 1 <= n holds
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 )

end;( 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 )
;

end;

suppose
n <> k
; :: thesis: ex Al2 being QC-alphabet st

( F2 . n = Al2 & F2 . (n + 1) = FCEx Al2 )

( 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;( F2 . n = Al2 & F2 . (n + 1) = FCEx Al2 ) by A11, A16, NAT_1:22; :: thesis: verum

suppose
n = k
; :: thesis: ex Al2 being QC-alphabet st

( F2 . n = Al2 & F2 . (n + 1) = FCEx Al2 )

( 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;( F2 . n = Al2 & F2 . (n + 1) = FCEx Al2 ) by A10, A14, FINSEQ_1:42; :: thesis: verum

F2 . n is QC-alphabet

proof

F2 . 1 = Al
by A7, A10, FINSEQ_1:64;
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;assume A18: ( n <= k + 1 & 1 <= n ) ; :: thesis: F2 . n is QC-alphabet

per cases
( n <> k + 1 or n = k + 1 )
;

end;

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;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

hence S

for n being Nat holds S

hence for k being Element of NAT st k > 0 holds

ex F being b

( ( 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