let f be FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:]; :: thesis: for n being Nat st 1 <= n & n <= len f holds
not not (f . n) `2 = 0 & ... & not (f . n) `2 = 10
let n be Nat; :: thesis: ( 1 <= n & n <= len f implies not not (f . n) `2 = 0 & ... & not (f . n) `2 = 10 )
assume ( 1 <= n & n <= len f ) ; :: thesis: not not (f . n) `2 = 0 & ... & not (f . n) `2 = 10
then n in dom f by FINSEQ_3:25;
then ( rng f c= [:MC-wff,Proof_Step_Kinds_IPC:] & f . n in rng f ) by FINSEQ_1:def 4, FUNCT_1:def 3;
then (f . n) `2 in Proof_Step_Kinds_IPC by MCART_1:10;
then ex k being Nat st
( k = (f . n) `2 & k <= 10 ) ;
hence not not (f . n) `2 = 0 & ... & not (f . n) `2 = 10 ; :: thesis: verum