:: deftheorem Def7 defines FCEx-Sequence GOEDCPUC:def 7 :
for Al being QC-alphabet
for k being Nat
for b₃ being b₂ + 1 -element FinSequence holds
( b₃ is FCEx-Sequence of Al,k iff ( ( for n being Nat st n <= k + 1 & 1 <= n holds
b₃ . n is QC-alphabet ) & b₃ . 1 = Al & ( for n being Nat st n < k + 1 & 1 <= n holds
ex Al2 being QC-alphabet st
( b₃ . n = Al2 & b₃ . (n + 1) = FCEx Al2 ) ) ) );