let Al be QC-alphabet ; :: thesis: for k being Nat
for S being FCEx-Sequence of Al,k holds S . (k + 1) is QC-alphabet
let k be Nat; :: thesis: for S being FCEx-Sequence of Al,k holds S . (k + 1) is QC-alphabet
let S be FCEx-Sequence of Al,k; :: thesis: S . (k + 1) is QC-alphabet
0 < 0 + (k + 1) ;
then ( 1 <= k + 1 & k + 1 <= k + 1 ) by NAT_1:19;
hence S . (k + 1) is QC-alphabet by Def7; :: thesis: verum