let m be Nat; :: thesis: ( 0 < m implies for n being Nat ex k, t being Nat st
( n = (m * k) + t & t < m ) )
defpred S₁[ Nat] means ex k, t being Nat st
( $1 = (m * k) + t & t < m );
assume A1: 0 < m ; :: thesis: for n being Nat ex k, t being Nat st
( n = (m * k) + t & t < m )
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
given k1, t1 being Nat such that A3: n = (m * k1) + t1 and
A4: t1 < m ; :: thesis: S₁[n + 1]
A5: ( t1 + 1 < m implies ex k, t being Nat st
( n + 1 = (m * k) + t & t < m ) )

proof

assume A6: t1 + 1 < m ; :: thesis: ex k, t being Nat st
( n + 1 = (m * k) + t & t < m )
take k = k1; :: thesis: ex t being Nat st
( n + 1 = (m * k) + t & t < m )
take t = t1 + 1; :: thesis: ( n + 1 = (m * k) + t & t < m )
thus n + 1 = (m * k) + t by A3; :: thesis: t < m
thus t < m by A6; :: thesis: verum

end;

A7: ( t1 + 1 = m implies ex k, t being Nat st
( n + 1 = (m * k) + t & t < m ) )

proof

assume A8: t1 + 1 = m ; :: thesis: ex k, t being Nat st
( n + 1 = (m * k) + t & t < m )
take k = k1 + 1; :: thesis: ex t being Nat st
( n + 1 = (m * k) + t & t < m )
take t = 0 ; :: thesis: ( n + 1 = (m * k) + t & t < m )
thus n + 1 = (m * k) + t by A3, A8; :: thesis: t < m
thus t < m by A1; :: thesis: verum

end;

t1 + 1 <= m by A4, Th13;
hence S₁[n + 1] by A5, A7, XXREAL_0:1; :: thesis: verum

end;

0 = (m * 0 ) + 0 ;
then A9: S₁[ 0 ] by A1;
thus for n being Nat holds S₁[n] from NAT_1:sch 2(A9, A2); :: thesis: verum