let PR be FinSequence of [:set_of_CQC-WFF-seq,Proof_Step_Kinds:]; for n being Nat st 1 <= n & n <= len PR & not (PR . n) `2 = 0 & not (PR . n) `2 = 1 & not (PR . n) `2 = 2 & not (PR . n) `2 = 3 & not (PR . n) `2 = 4 & not (PR . n) `2 = 5 & not (PR . n) `2 = 6 & not (PR . n) `2 = 7 & not (PR . n) `2 = 8 holds
(PR . n) `2 = 9
let n be Nat; ( 1 <= n & n <= len PR & not (PR . n) `2 = 0 & not (PR . n) `2 = 1 & not (PR . n) `2 = 2 & not (PR . n) `2 = 3 & not (PR . n) `2 = 4 & not (PR . n) `2 = 5 & not (PR . n) `2 = 6 & not (PR . n) `2 = 7 & not (PR . n) `2 = 8 implies (PR . n) `2 = 9 )
assume
( 1 <= n & n <= len PR )
; ( (PR . n) `2 = 0 or (PR . n) `2 = 1 or (PR . n) `2 = 2 or (PR . n) `2 = 3 or (PR . n) `2 = 4 or (PR . n) `2 = 5 or (PR . n) `2 = 6 or (PR . n) `2 = 7 or (PR . n) `2 = 8 or (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 Element of NAT : k <= 9 }
by CQC_THE1:def 3, MCART_1:10;
then
ex k being Element of NAT st
( k = (PR . n) `2 & k <= 9 )
;
hence
( (PR . n) `2 = 0 or (PR . n) `2 = 1 or (PR . n) `2 = 2 or (PR . n) `2 = 3 or (PR . n) `2 = 4 or (PR . n) `2 = 5 or (PR . n) `2 = 6 or (PR . n) `2 = 7 or (PR . n) `2 = 8 or (PR . n) `2 = 9 )
by NAT_1:33; verum