now :: thesis: for x being object st x in EvenNAT /\ {1,2,3,4} holds
x in {2,4}
let x be object ; :: thesis: ( x in EvenNAT /\ {1,2,3,4} implies b1 in {2,4} )
assume A1: x in EvenNAT /\ {1,2,3,4} ; :: thesis: b1 in {2,4}
then A2: x in EvenNAT by XBOOLE_0:def 4;
A3: x in {1,2,3,4} by A1, XBOOLE_0:def 4;
per cases ( x = (2 * 0) + 1 or x = 2 * 1 or x = (2 * 1) + 1 or x = 2 * 2 ) by A3, ENUMSET1:def 2;
suppose x = (2 * 0) + 1 ; :: thesis: b1 in {2,4}
hence x in {2,4} by A2, Th51; :: thesis: verum
end;
suppose x = (2 * 1) + 1 ; :: thesis: b1 in {2,4}
hence x in {2,4} by A2, Th51; :: thesis: verum
end;
end;
end;
then A4: EvenNAT /\ {1,2,3,4} c= {2,4} ;
set q = {[2,(FIB . 2)],[4,(FIB . 4)]};
4 in NAT ;
then A5: 4 in dom FIB by FUNCT_2:def 1;
reconsider q = {[2,(FIB . 2)],[4,(FIB . 4)]} as FinSubsequence by Th15;
2 in NAT ;
then A6: 2 in dom FIB by FUNCT_2:def 1;
A7: FIB | ({2} \/ {4}) = (FIB | {2}) \/ (FIB | {4}) by RELAT_1:78
.= {[2,(FIB . 2)]} \/ (FIB | {4}) by A6, GRFUNC_1:28
.= {[2,(FIB . 2)]} \/ {[4,(FIB . 4)]} by A5, GRFUNC_1:28
.= q by ENUMSET1:1 ;
now :: thesis: for x being object st x in {2,4} holds
x in EvenNAT /\ {1,2,3,4}
let x be object ; :: thesis: ( x in {2,4} implies x in EvenNAT /\ {1,2,3,4} )
assume A8: x in {2,4} ; :: thesis: x in EvenNAT /\ {1,2,3,4}
then ( x = 2 * 1 or x = 2 * 2 ) by TARSKI:def 2;
then A9: x in EvenNAT ;
( x = 2 or x = 4 ) by A8, TARSKI:def 2;
then x in {1,2,3,4} by ENUMSET1:def 2;
hence x in EvenNAT /\ {1,2,3,4} by A9, XBOOLE_0:def 4; :: thesis: verum
end;
then {2,4} c= EvenNAT /\ {1,2,3,4} ;
then EvenNAT /\ {1,2,3,4} = {2,4} by A4;
then EvenFibs 4 = Seq q by A7, ENUMSET1:1, FINSEQ_3:2
.= <*(FIB . 2),(FIB . 4)*> by Th16
.= <*(Fib 2),(FIB . 4)*> by Def2
.= <*1,3*> by Def2, Th21, Th23 ;
hence EvenFibs 4 = <*1,3*> ; :: thesis: verum