now :: thesis: for x being object st x in OddNAT /\ {1,2,3} holds
x in {1,3}

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

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

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

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

end;

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

hence x in {1,3} by A2, Th52; :: thesis: verum

end;

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

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

end;

end;

end;

then A4: OddNAT /\ {1,2,3} c= {1,3} ;
set q = {[1,(FIB . 1)],[3,(FIB . 3)]};
3 in NAT ;
then A5: 3 in dom FIB by FUNCT_2:def 1;
reconsider q = {[1,(FIB . 1)],[3,(FIB . 3)]} as FinSubsequence by Th15;
1 in NAT ;
then A6: 1 in dom FIB by FUNCT_2:def 1;
A7: FIB | ({1} \/ {3}) = (FIB | {1}) \/ (FIB | {3}) by RELAT_1:78
.= {[1,(FIB . 1)]} \/ (FIB | {3}) by A6, GRFUNC_1:28
.= {[1,(FIB . 1)]} \/ {[3,(FIB . 3)]} by A5, GRFUNC_1:28
.= q by ENUMSET1:1 ;

now :: thesis: for x being object st x in {1,3} holds
x in OddNAT /\ {1,2,3}

let x be object ; :: thesis: ( x in {1,3} implies x in OddNAT /\ {1,2,3} )
assume A8: x in {1,3} ; :: thesis: x in OddNAT /\ {1,2,3}
then ( x = (2 * 0) + 1 or x = (2 * 1) + 1 ) by TARSKI:def 2;
then A9: x in OddNAT ;
( x = 1 or x = 3 ) by A8, TARSKI:def 2;
then x in {1,2,3} by ENUMSET1:def 1;
hence x in OddNAT /\ {1,2,3} by A9, XBOOLE_0:def 4; :: thesis: verum

end;

then {1,3} c= OddNAT /\ {1,2,3} ;
then OddNAT /\ {1,2,3} = {1,3} by A4;
then OddFibs 3 = Seq (FIB | ({1} \/ {3})) by ENUMSET1:1, FINSEQ_3:1
.= <*(FIB . 1),(FIB . 3)*> by A7, Th16
.= <*(Fib 1),(FIB . 3)*> by Def2
.= <*1,2*> by Def2, Th22, PRE_FF:1 ;
hence OddFibs 3 = <*1,2*> ; :: thesis: verum