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

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A1: x in Al ; :: thesis:
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]

let l be Nat; :: thesis:
assume A4: S₁[l] ; :: thesis:
assume A5: l + 1 < k + 1 ; :: thesis:
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 )

let n be Nat; :: thesis:
assume A7: ( n + 1 < k + 1 & 1 <= n + 1 ) ; :: thesis:
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:

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:

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:

end;