let Al be QC-alphabet ; :: thesis: for PR being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]
for n being Nat st 1 <= n & n <= len PR holds
not not (PR . n) `2 = 0 & ... & not (PR . n) `2 = 9
let PR be FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]; :: thesis: for n being Nat st 1 <= n & n <= len PR holds
not not (PR . n) `2 = 0 & ... & not (PR . n) `2 = 9
let n be Nat; :: thesis: ( 1 <= n & n <= len PR implies not not (PR . n) `2 = 0 & ... & not (PR . n) `2 = 9 )
assume ( 1 <= n & n <= len PR ) ; :: thesis: not not (PR . n) `2 = 0 & ... & not (PR . n) `2 = 9
then n in dom PR by FINSEQ_3:25;
then PR . n in rng PR by FUNCT_1:def 3;
then (PR . n) `2 in { k where k is Nat : k <= 9 } by CQC_THE1:def 3, MCART_1:10;
then ex k being Nat st
( k = (PR . n) `2 & k <= 9 ) ;
hence not not (PR . n) `2 = 0 & ... & not (PR . n) `2 = 9 ; :: thesis: verum