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

proof

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

proof

now

let x be set ; :: thesis: ( x in OddNAT /\ {1,2,3} implies b₁ in {1,3} )
assume x in OddNAT /\ {1,2,3} ; :: thesis: b₁ in {1,3}
then A3: ( x in OddNAT & x in {1,2,3} ) by 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 A3, Th54; :: 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;

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

end;

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

proof

now

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

end;

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

end;

end;

A7: FIB | ({1} \/ {3}) = (FIB | {1}) \/ (FIB | {3}) by RELAT_1:107
.= {[1,(FIB . 1)]} \/ (FIB | {3}) by A1, GRFUNC_1:89
.= {[1,(FIB . 1)]} \/ {[3,(FIB . 3)]} by A1, GRFUNC_1:89
.= q by ENUMSET1:41 ;
OddFibs 3 = Seq (FIB | ({1} \/ {3})) by A2, ENUMSET1:41, FINSEQ_3:1
.= <*(FIB . 1),(FIB . 3)*> by A7, Th18
.= <*(Fib 1),(FIB . 3)*> by Def2
.= <*1,2*> by Def2, Th24, PRE_FF:1 ;
hence OddFibs 3 = <*1,2*> ; :: thesis: verum