set q = {[2,(FIB . 2)],[4,(FIB . 4)]};
reconsider q = {[2,(FIB . 2)],[4,(FIB . 4)]} as FinSubsequence by Th17;
( 2 in NAT & 4 in NAT )
;
then A1:
( 2 in dom FIB & 4 in dom FIB )
by FUNCT_2:def 1;
A2:
EvenNAT /\ {1,2,3,4} = {2,4}
proof
thus
EvenNAT /\ {1,2,3,4} c= {2,4}
:: according to XBOOLE_0:def 10 :: thesis: {2,4} c= EvenNAT /\ {1,2,3,4}proof
now let x be
set ;
:: thesis: ( x in EvenNAT /\ {1,2,3,4} implies b1 in {2,4} )assume
x in EvenNAT /\ {1,2,3,4}
;
:: thesis: b1 in {2,4}then A3:
(
x in EvenNAT &
x in {1,2,3,4} )
by XBOOLE_0:def 4;
end;
hence
EvenNAT /\ {1,2,3,4} c= {2,4}
by TARSKI:def 3;
:: thesis: verum
end;
thus
{2,4} c= EvenNAT /\ {1,2,3,4}
:: thesis: verumproof
now let x be
set ;
:: thesis: ( x in {2,4} implies x in EvenNAT /\ {1,2,3,4} )assume A4:
x in {2,4}
;
:: thesis: x in EvenNAT /\ {1,2,3,4}then A5:
(
x = 2 or
x = 4 )
by TARSKI:def 2;
(
x = 2
* 1 or
x = 2
* 2 )
by A4, TARSKI:def 2;
then A6:
x in EvenNAT
;
x in {1,2,3,4}
by A5, ENUMSET1:def 2;
hence
x in EvenNAT /\ {1,2,3,4}
by A6, XBOOLE_0:def 4;
:: thesis: verum end;
hence
{2,4} c= EvenNAT /\ {1,2,3,4}
by TARSKI:def 3;
:: thesis: verum
end;
end;
FIB | ({2} \/ {4}) =
(FIB | {2}) \/ (FIB | {4})
by RELAT_1:107
.=
{[2,(FIB . 2)]} \/ (FIB | {4})
by A1, GRFUNC_1:89
.=
{[2,(FIB . 2)]} \/ {[4,(FIB . 4)]}
by A1, GRFUNC_1:89
.=
q
by ENUMSET1:41
;
then EvenFibs 4 =
Seq q
by A2, ENUMSET1:41, FINSEQ_3:2
.=
<*(FIB . 2),(FIB . 4)*>
by Th18
.=
<*(Fib 2),(FIB . 4)*>
by Def2
.=
<*1,3*>
by Def2, Th23, Th25
;
hence
EvenFibs 4 = <*1,3*>
; :: thesis: verum