let j, k be Nat; :: thesis: ( j <> 0 implies j divides (j + k) ! )
defpred S₁[ Nat] means for j being Nat st j <> 0 holds
j divides (j + $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: for j being Nat st j <> 0 holds
j divides (j + k) ! ; :: thesis: S₁[k + 1]
let j be Nat; :: thesis: ( j <> 0 implies j divides (j + (k + 1)) ! )
assume j <> 0 ; :: thesis: j divides (j + (k + 1)) !
then j divides ((j + k) !) * ((j + k) + 1) by A2, NAT_D:9;
hence j divides (j + (k + 1)) ! by Th15; :: thesis: verum

end;

A3: S₁[ 0 ] by Th35;
for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A1);
hence ( j <> 0 implies j divides (j + k) ! ) ; :: thesis: verum