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 for x being object st x in {1,3} holds
x in OddNAT /\ {1,2,3}let x be
object ;
( x in {1,3} implies x in OddNAT /\ {1,2,3} )assume A8:
x in {1,3}
;
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;
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*>
; verum