theorem Th2: :: GOEDCPUC:2

for Al being QC-alphabet
for k being Element of NAT st k > 0 holds
ex F being b₂ -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 ) ) )