let n, k be Nat; :: thesis: ( k < n & n <= 7 implies ex i being Nat st (Fib i) mod n = k )
assume A1: ( k < n & n <= 7 ) ; :: thesis: ex i being Nat st (Fib i) mod n = k
not not n = 0 & ... & not n = 7 by A1;

per cases then ( n = 1 or n = 2 or n = 3 or n = 4 or n = 5 or n = 6 or n = 7 ) by A1;

suppose A2: n = 1 ; :: thesis: ex i being Nat st (Fib i) mod n = k

then A3: k = 0 by A1, NAT_1:14;
((1 * 1) + 0) mod 1 = 0 ;
hence ex i being Nat st (Fib i) mod n = k by A2, A3, PRE_FF:1; :: thesis: verum

end;

suppose A4: n = 2 ; :: thesis: ex i being Nat st (Fib i) mod n = k

then A5: not not k = 0 & ... & not k = 2 by A1;
( ((2 * 0) + 1) mod 2 = 1 & ((2 * 1) + 0) mod 2 = 0 ) ;
hence ex i being Nat st (Fib i) mod n = k by A1, A4, A5, FIB_NUM2:22, PRE_FF:1; :: thesis: verum

end;

suppose A6: n = 3 ; :: thesis: ex i being Nat st (Fib i) mod n = k

then A7: not not k = 0 & ... & not k = 3 by A1;
( ((3 * 0) + 2) mod 3 = 2 & ((3 * 0) + 1) mod 3 = 1 & ((3 * 1) + 0) mod 3 = 0 ) by NUMBER02:16;
hence ex i being Nat st (Fib i) mod n = k by A1, A6, A7, FIB_NUM2:22, FIB_NUM2:23, PRE_FF:1; :: thesis: verum

end;

suppose A8: n = 4 ; :: thesis: ex i being Nat st (Fib i) mod n = k

then A9: not not k = 0 & ... & not k = 4 by A1;
( ((4 * 0) + 1) mod 4 = 1 & ((4 * 0) + 2) mod 4 = 2 & ((4 * 0) + 3) mod 4 = 3 & ((4 * 2) + 0) mod 4 = 0 ) by NUMBER02:16;
hence ex i being Nat st (Fib i) mod n = k by A1, A8, A9, FIB_NUM2:21, FIB_NUM2:22, FIB_NUM2:23, Th7; :: thesis: verum

end;

suppose A10: n = 5 ; :: thesis: ex i being Nat st (Fib i) mod n = k

then A11: not not k = 0 & ... & not k = 5 by A1;
( ((5 * 1) + 0) mod 5 = 0 & ((5 * 0) + 1) mod 5 = 1 & ((5 * 0) + 2) mod 5 = 2 & ((5 * 0) + 3) mod 5 = 3 & ((5 * 6) + 4) mod 5 = 4 ) by NUMBER02:16;
hence ex i being Nat st (Fib i) mod n = k by A1, A10, A11, FIB_NUM2:22, FIB_NUM2:23, PRE_FF:1, Th7, NUMBER06:46; :: thesis: verum

end;

suppose A12: n = 6 ; :: thesis: ex i being Nat st (Fib i) mod n = k

then A13: not not k = 0 & ... & not k = 6 by A1;
( ((24 * 6) + 0) mod 6 = 0 & ((6 * 0) + 1) mod 6 = 1 & ((6 * 0) + 2) mod 6 = 2 & ((6 * 0) + 3) mod 6 = 3 & ((6 * 5) + 4) mod 6 = 4 & ((6 * 0) + 5) mod 6 = 5 ) by NUMBER02:16;
hence ex i being Nat st (Fib i) mod n = k by A1, A12, A13, FIB_NUM2:22, FIB_NUM2:23, NUMBER06:46, PRE_FF:1, Th7; :: thesis: verum

end;

suppose A14: n = 7 ; :: thesis: ex i being Nat st (Fib i) mod n = k

then A15: not not k = 0 & ... & not k = 7 by A1;
( ((3 * 7) + 0) mod 7 = 0 & ((7 * 0) + 1) mod 7 = 1 & ((7 * 0) + 2) mod 7 = 2 & ((7 * 0) + 3) mod 7 = 3 & ((20 * 7) + 4) mod 7 = 4 & ((7 * 0) + 5) mod 7 = 5 & ((7 * 1) + 6) mod 7 = 6 ) by NUMBER02:16;
hence ex i being Nat st (Fib i) mod n = k by A1, A14, A15, FIB_NUM2:21, FIB_NUM2:22, FIB_NUM2:23, NUMBER06:46, Th7; :: thesis: verum

end;

end;