let x be object ; :: thesis:
assume A1: x in EvenNAT /\ {1,2} ; :: thesis:
then A2: x in EvenNAT by XBOOLE_0:def 4;
A3: x in {1,2} by A1, XBOOLE_0:def 4;

per cases by A3, TARSKI:def 2;

suppose x = 1 ; :: thesis:

then x = 0 + 1 ;
then A4: x = (2 * 0) + 1 ;
ex k being Nat st x = 2 * k by A2;
hence x in {2} by A4; :: thesis:

end;

suppose x = 2 * 1 ; :: thesis:

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

end;

end;

end;

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

let x be object ; :: thesis:
assume x in {2} ; :: thesis:
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:

end;

then {2} c= EvenNAT /\ {1,2} ;
then EvenNAT /\ {1,2} = {2} by A5;
then EvenFibs 2 = Seq q by A6, FINSEQ_1:2, GRFUNC_1:28
.= <*(FIB . 2)*> by FINSEQ_3:157
.= <*1*> by Def2, Th21 ;
hence EvenFibs 2 = <*1*> ; :: thesis: