defpred S₁[ Element of NAT , Element of NAT ] means (Fib $1) gcd (Fib $2) = Fib ($1 gcd $2);
A1: for k being Element of NAT st ( for m, n being Element of NAT st m < k & n < k holds
S₁[m,n] ) holds
for m being Element of NAT st m <= k holds
S₁[k,m]

let k be Element of NAT ; :: thesis:
assume A2: for m, n being Element of NAT st m < k & n < k holds
S₁[m,n] ; :: thesis:
let m be Element of NAT ; :: thesis:
assume A3: m <= k ; :: thesis:

hence (Fib k) gcd (Fib m) = Fib k by NAT_D:32
.= Fib (k gcd m) by A4, NAT_D:32 ;
:: thesis:

end;

end;

consider r being Nat such that
A9: k = m + r by A3, NAT_1:10;
reconsider r = r as Element of NAT by ORDINAL1:def 13;
A10: r <= k by A9, NAT_1:11;
r <> 0 by A5, A9;
then consider rr being Nat such that
A11: r = rr + 1 by NAT_1:6;
reconsider rr = rr as Element of NAT by ORDINAL1:def 13;
Fib k = ((Fib (rr + 1)) * (Fib (m + 1))) + ((Fib rr) * (Fib m)) by A9, A11, Th4;
then A12: (Fib k) gcd (Fib m) = (Fib m) gcd ((Fib (m + 1)) * (Fib r)) by A11, EULER_1:9;
(Fib m) gcd (Fib (m + 1)) = 1 by Lm7;
then A13: (Fib k) gcd (Fib m) = (Fib m) gcd (Fib r) by A12, Th2;
r <> k by A8, A9;
then A14: r < k by A10, XXREAL_0:1;
k gcd m = m gcd r by A9, Th1;
hence S₁[k,m] by A2, A5, A13, A14; :: thesis:

end;