let k be Nat; :: thesis: for n being non empty Element of NAT holds Fib n divides Fib (n * k)
let n be non empty Element of NAT ; :: thesis: Fib n divides Fib (n * k)
defpred S₁[ Nat] means Fib n divides Fib (n * $1);
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
Fib (n * (k + 1)) = Fib ((n * k) + n)
.= ((Fib n) * (Fib ((n * k) + 1))) + ((Fib (n * k)) * (Fib (n -' 1))) by Th42 ;
hence S₁[k + 1] by A2, Th14; :: thesis: verum

end;

A3: S₁[ 0 ] by NAT_D:6, PRE_FF:1;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A1);
hence Fib n divides Fib (n * k) ; :: thesis: verum