let m, n, a be Nat; :: thesis: ( (modSeq m,n) . a = 0 implies (divSeq m,n) . (a + 1) = 0 )
set fd = divSeq m,n;
set fm = modSeq m,n;
defpred S₁[ Nat] means ( (modSeq m,n) . $1 = 0 implies (divSeq m,n) . ($1 + 1) = 0 );
A1: for b being Nat st S₁[b] holds
S₁[b + 1]

proof

let b be Nat; :: thesis: ( S₁[b] implies S₁[b + 1] )
assume that
S₁[b] and
A2: (modSeq m,n) . (b + 1) = 0 ; :: thesis: (divSeq m,n) . ((b + 1) + 1) = 0
thus (divSeq m,n) . ((b + 1) + 1) = (divSeq m,n) . (b + (1 + 1))
.= ((modSeq m,n) . b) div ((modSeq m,n) . (b + 1)) by Def3
.= 0 by A2 ; :: thesis: verum

end;

A3: S₁[ 0 ]

proof

assume A4: (modSeq m,n) . 0 = 0 ; :: thesis: (divSeq m,n) . (0 + 1) = 0
thus (divSeq m,n) . (0 + 1) = n div ((modSeq m,n) . 0 ) by Th12
.= 0 by A4 ; :: thesis: verum

end;

for b being Nat holds S₁[b] from NAT_1:sch 2(A3, A1);
hence ( (modSeq m,n) . a = 0 implies (divSeq m,n) . (a + 1) = 0 ) ; :: thesis: verum