let m be Nat; :: thesis: ( 0 < m implies for n being Nat ex k, t being Nat st
( n = (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 )
defpred S₁[ Nat] means ex k, t being Nat st
( $1 = (m * k) + t & t < m );
0 = (m * 0 ) + 0 ;
then A2: S₁[ 0 ] by A1;
A3: 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 A4: ( n = (m * k1) + t1 & t1 < m ) ; :: thesis: S₁[n + 1]
A5: t1 + 1 <= m by A4, Th13;
A6: ( t1 + 1 < m implies ex k, t being Nat st
( n + 1 = (m * k) + t & t < m ) )

proof

assume A7: 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 A4; :: thesis: t < m
thus t < m by A7; :: thesis: verum

end;

( 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 A4, A8; :: thesis: t < m
thus t < m by A1; :: thesis: verum

end;

hence S₁[n + 1] by A5, A6, XXREAL_0:1; :: thesis: verum

end;

thus for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3); :: thesis: verum