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

proof

thus EvenNAT /\ {1,2} c= {2} :: according to XBOOLE_0:def 10 :: thesis: {2} c= EvenNAT /\ {1,2}

proof

now

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

per cases ( x = (2 * 0 ) + 1 or x = 2 * 1 ) by A2, 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;

hence EvenNAT /\ {1,2} c= {2} by TARSKI:def 3; :: thesis: verum

end;

thus {2} c= EvenNAT /\ {1,2} :: thesis: verum

proof

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 A3: x = 2 * 1 by TARSKI:def 1;
then A4: x in EvenNAT ;
x in {1,2} by A3, TARSKI:def 2;
hence x in EvenNAT /\ {1,2} by A4, XBOOLE_0:def 4; :: thesis: verum

end;

hence {2} c= EvenNAT /\ {1,2} by TARSKI:def 3; :: thesis: verum

end;

end;

then EvenFibs 2 = Seq q by A1, FINSEQ_1:4, GRFUNC_1:89
.= <*(FIB . 2)*> by PNPROC_1:3
.= <*1*> by Def2, Th23 ;
hence EvenFibs 2 = <*1*> ; :: thesis: verum