let n be Nat; :: thesis: for k being non zero Element of NAT st k divides n holds
Fib k divides Fib n
let k be non zero Element of NAT ; :: thesis: ( k divides n implies Fib k divides Fib n )
assume k divides n ; :: thesis: Fib k divides Fib n
then ex m being Nat st n = k * m by NAT_D:def 3;
hence Fib k divides Fib n by Th41; :: thesis: verum