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