:: deftheorem Def9 defines EF-Sequence GOEDCPUC:def 9 :
for Al being QC-alphabet
for PHI being Consistent Subset of (CQC-WFF Al)
for b₃ being Function holds
( b₃ is EF-Sequence of Al,PHI iff ( dom b₃ = NAT & b₃ . 0 = PHI & ( for n being Nat holds b₃ . (n + 1) = (b₃ . n) \/ (Example_Formulae_of (n -th_FCEx Al)) ) ) );