let j, k be Nat; :: thesis: ( j <> 0 implies j divides (j + k) ! )
defpred S1[ Nat] means for j being Nat st j <> 0 holds
j divides (j + $1) ! ;
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A2: for j being Nat st j <> 0 holds
j divides (j + k) ! ; :: thesis: S1[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: S1[ 0 ] by Th35;
for k being Nat holds S1[k] from NAT_1:sch 2(A3, A1);
 hence ( j <> 0 implies j divides (j + k) ! ) ; :: thesis: verum