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

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