defpred S₁[ Element of NAT ] means (Fib $1) gcd (Fib ($1 + 1)) = 1;
A1: S₁[ 0 ] by NEWTON:65, PRE_FF:1;

A2: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

thus (Fib (k + 1)) gcd (Fib ((k + 1) + 1)) = (Fib (k + 1)) gcd ((Fib (k + 1)) + (Fib k)) by PRE_FF:1
.= 1 by A3, Th1 ; :: thesis: verum

end;

end;

thus for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A1, A2); :: thesis: verum