let n, m, k, t, k1, t1 be natural Number ; :: thesis: ( n = (m * k) + t & t < m & n = (m * k1) + t1 & t1 < m implies ( k = k1 & t = t1 ) )
assume that
A1: n = (m * k) + t and
A2: t < m and
A3: n = (m * k1) + t1 and
A4: t1 < m ; :: thesis: ( k = k1 & t = t1 )
A5: now :: thesis: ( k1 <= k implies ( k = k1 & t = t1 ) )
assume k1 <= k ; :: thesis: ( k = k1 & t = t1 )
then consider u being Nat such that
A6: k = k1 + u by Th10;
(m * (k1 + u)) + t = (m * k1) + ((m * u) + t) ;
then A7: (m * u) + t = t1 by A1, A3, A6, XCMPLX_1:2;
now :: thesis: for w being Nat holds not u = w + 1
given w being Nat such that A8: u = w + 1 ; :: thesis: contradiction
(m * u) + t = m + ((m * w) + t) by A8;
hence contradiction by A4, A7, Th11; :: thesis: verum
end;
then A9: u = 0 by Th6;
hence k = k1 by A6; :: thesis: t = t1
thus t = t1 by A1, A3, A6, A9, XCMPLX_1:2; :: thesis: verum
end;
now :: thesis: ( k <= k1 implies ( k = k1 & t = t1 ) )
assume k <= k1 ; :: thesis: ( k = k1 & t = t1 )
then consider u being Nat such that
A10: k1 = k + u by Th10;
(m * (k + u)) + t1 = (m * k) + ((m * u) + t1) ;
then A11: (m * u) + t1 = t by A1, A3, A10, XCMPLX_1:2;
now :: thesis: for w being Nat holds not u = w + 1
given w being Nat such that A12: u = w + 1 ; :: thesis: contradiction
(m * u) + t1 = m + ((m * w) + t1) by A12;
hence contradiction by A2, A11, Th11; :: thesis: verum
end;
then A13: u = 0 by Th6;
hence k = k1 by A10; :: thesis: t = t1
thus t = t1 by A1, A3, A10, A13, XCMPLX_1:2; :: thesis: verum
end;
hence ( k = k1 & t = t1 ) by A5; :: thesis: verum