let Al be QC-alphabet ; :: thesis: for k being Nat
for S being FCEx-Sequence of Al,k holds S . (k + 1) is Al -expanding QC-alphabet
let k be Nat; :: thesis: for S being FCEx-Sequence of Al,k holds S . (k + 1) is Al -expanding QC-alphabet
let S be FCEx-Sequence of Al,k; :: thesis: S . (k + 1) is Al -expanding QC-alphabet
set Al2 = S . (k + 1);
reconsider Al2 = S . (k + 1) as QC-alphabet by Th3;
Al c= Al2

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Al or x in Al2 )
assume A1: x in Al ; :: thesis: x in Al2
defpred S₁[ Nat] means ( $1 < k + 1 implies x in S . ($1 + 1) );
A2: S₁[ 0 ] by A1, Def7;
A3: for l being Nat st S₁[l] holds
S₁[l + 1]

proof

let l be Nat; :: thesis: ( S₁[l] implies S₁[l + 1] )
assume A4: S₁[l] ; :: thesis: S₁[l + 1]
assume A5: l + 1 < k + 1 ; :: thesis: x in S . ((l + 1) + 1)
A6: for n being Nat st n + 1 < k + 1 & 1 <= n + 1 holds
ex Al2 being QC-alphabet st
( S . (n + 1) = Al2 & S . (n + 2) = FCEx Al2 )

proof

let n be Nat; :: thesis: ( n + 1 < k + 1 & 1 <= n + 1 implies ex Al2 being QC-alphabet st
( S . (n + 1) = Al2 & S . (n + 2) = FCEx Al2 ) )
assume A7: ( n + 1 < k + 1 & 1 <= n + 1 ) ; :: thesis: ex Al2 being QC-alphabet st
( S . (n + 1) = Al2 & S . (n + 2) = FCEx Al2 )
set m = n + 1;
ex Al2 being QC-alphabet st
( S . (n + 1) = Al2 & S . ((n + 1) + 1) = FCEx Al2 ) by Def7, A7;
hence ex Al2 being QC-alphabet st
( S . (n + 1) = Al2 & S . (n + 2) = FCEx Al2 ) ; :: thesis: verum

end;

0 < 0 + (l + 1) ;
then consider Al2 being QC-alphabet such that
A8: ( S . (l + 1) = Al2 & S . (l + 2) = FCEx Al2 ) by A5, A6, NAT_1:19;
S . (l + 1) c= S . (l + 2) by A8, QC_TRANS:def 1;
hence x in S . ((l + 1) + 1) by A4, A5, NAT_1:16, XXREAL_0:2; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
then ( k < k + 1 implies x in S . (k + 1) ) ;
hence x in Al2 by NAT_1:13; :: thesis: verum

end;

hence S . (k + 1) is Al -expanding QC-alphabet by QC_TRANS:def 1; :: thesis: verum