let Al be QC-alphabet ; :: thesis: for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]
for n being Nat st 1 <= n & n <= len f holds
not not (f . n) `2 = 0 & ... & not (f . n) `2 = 9
let f be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]; :: thesis: for n being Nat st 1 <= n & n <= len f holds
not not (f . n) `2 = 0 & ... & not (f . n) `2 = 9
let n be Nat; :: thesis: ( 1 <= n & n <= len f implies not not (f . n) `2 = 0 & ... & not (f . n) `2 = 9 )
assume A1: ( 1 <= n & n <= len f ) ; :: thesis: not not (f . n) `2 = 0 & ... & not (f . n) `2 = 9
dom f = Seg (len f) by FINSEQ_1:def 3;
then n in dom f by A1, FINSEQ_1:1;
then ( rng f c= [:(CQC-WFF Al),Proof_Step_Kinds:] & f . n in rng f ) by FINSEQ_1:def 4, FUNCT_1:def 3;
then (f . n) `2 in Proof_Step_Kinds by MCART_1:10;
then ex k being Nat st
( k = (f . n) `2 & k <= 9 ) ;
hence not not (f . n) `2 = 0 & ... & not (f . n) `2 = 9 ; :: thesis: verum