now

let x be set ; :: thesis: ( x in EvenNAT /\ {1,2} implies b₁ in {2} )
assume A1: x in EvenNAT /\ {1,2} ; :: thesis: b₁ in {2}
then A2: x in EvenNAT by XBOOLE_0:def 4;
A3: x in {1,2} by A1, XBOOLE_0:def 4;

per cases ( x = (2 * 0 ) + 1 or x = 2 * 1 ) by A3, TARSKI:def 2;

suppose x = (2 * 0 ) + 1 ; :: thesis: b₁ in {2}

hence x in {2} by A2, Th53; :: thesis: verum

end;

suppose x = 2 * 1 ; :: thesis: b₁ in {2}

hence x in {2} by TARSKI:def 1; :: thesis: verum

end;

end;

end;

then A4: EvenNAT /\ {1,2} c= {2} by TARSKI:def 3;
set q = {[2,(FIB . 2)]};
reconsider q = {[2,(FIB . 2)]} as FinSubsequence by Th19;
2 in NAT ;
then A5: 2 in dom FIB by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in {2} implies x in EvenNAT /\ {1,2} )
assume x in {2} ; :: thesis: x in EvenNAT /\ {1,2}
then x = 2 * 1 by TARSKI:def 1;
then ( x in EvenNAT & x in {1,2} ) by TARSKI:def 2;
hence x in EvenNAT /\ {1,2} by XBOOLE_0:def 4; :: thesis: verum

end;

then {2} c= EvenNAT /\ {1,2} by TARSKI:def 3;
then EvenNAT /\ {1,2} = {2} by A4, XBOOLE_0:def 10;
then EvenFibs 2 = Seq q by A5, FINSEQ_1:4, GRFUNC_1:89
.= <*(FIB . 2)*> by PNPROC_1:3
.= <*1*> by Def2, Th23 ;
hence EvenFibs 2 = <*1*> ; :: thesis: verum