let f be FinSequence of [:CQC-WFF ,Proof_Step_Kinds :]; for n being Nat st 1 <= n & n <= len f & not (f . n) `2 = 0 & not (f . n) `2 = 1 & not (f . n) `2 = 2 & not (f . n) `2 = 3 & not (f . n) `2 = 4 & not (f . n) `2 = 5 & not (f . n) `2 = 6 & not (f . n) `2 = 7 & not (f . n) `2 = 8 holds
(f . n) `2 = 9
let n be Nat; ( 1 <= n & n <= len f & not (f . n) `2 = 0 & not (f . n) `2 = 1 & not (f . n) `2 = 2 & not (f . n) `2 = 3 & not (f . n) `2 = 4 & not (f . n) `2 = 5 & not (f . n) `2 = 6 & not (f . n) `2 = 7 & not (f . n) `2 = 8 implies (f . n) `2 = 9 )
assume A1:
( 1 <= n & n <= len f )
; ( (f . n) `2 = 0 or (f . n) `2 = 1 or (f . n) `2 = 2 or (f . n) `2 = 3 or (f . n) `2 = 4 or (f . n) `2 = 5 or (f . n) `2 = 6 or (f . n) `2 = 7 or (f . n) `2 = 8 or (f . n) `2 = 9 )
A2:
dom f = Seg (len f)
by FINSEQ_1:def 3;
A3:
n in dom f
by A1, A2, FINSEQ_1:3;
A4:
( rng f c= [:CQC-WFF ,Proof_Step_Kinds :] & f . n in rng f )
by A3, FINSEQ_1:def 4, FUNCT_1:def 5;
A5:
(f . n) `2 in Proof_Step_Kinds
by A4, MCART_1:10;
A6:
ex k being Element of NAT st
( k = (f . n) `2 & k <= 9 )
by A5;
thus
( (f . n) `2 = 0 or (f . n) `2 = 1 or (f . n) `2 = 2 or (f . n) `2 = 3 or (f . n) `2 = 4 or (f . n) `2 = 5 or (f . n) `2 = 6 or (f . n) `2 = 7 or (f . n) `2 = 8 or (f . n) `2 = 9 )
by A6, NAT_1:34; verum