let n, m, k, t, k1, t1 be Nat; :: thesis: ( n = (m * k) + t & t < m & n = (m * k1) + t1 & t1 < m implies ( k = k1 & t = t1 ) )
assume A1: ( n = (m * k) + t & t < m & n = (m * k1) + t1 & t1 < m ) ; :: thesis: ( k = k1 & t = t1 )

A2: now

assume k <= k1 ; :: thesis: ( k = k1 & t = t1 )
then consider u being Nat such that
A3: k1 = k + u by Th10;
(m * (k + u)) + t1 = (m * k) + ((m * u) + t1) ;
then A4: (m * u) + t1 = t by A1, A3, XCMPLX_1:2;

now

given w being Nat such that A5: u = w + 1 ; :: thesis: contradiction
(m * u) + t1 = m + ((m * w) + t1) by A5;
hence contradiction by A1, A4, Th11; :: thesis: verum

end;

then A6: u = 0 by Th6;
hence k = k1 by A3; :: thesis: t = t1
thus t = t1 by A1, A3, A6, XCMPLX_1:2; :: thesis: verum

end;

now

assume k1 <= k ; :: thesis: ( k = k1 & t = t1 )
then consider u being Nat such that
A7: k = k1 + u by Th10;
(m * (k1 + u)) + t = (m * k1) + ((m * u) + t) ;
then A8: (m * u) + t = t1 by A1, A7, XCMPLX_1:2;

now

given w being Nat such that A9: u = w + 1 ; :: thesis: contradiction
(m * u) + t = m + ((m * w) + t) by A9;
hence contradiction by A1, A8, Th11; :: thesis: verum

end;

then A10: u = 0 by Th6;
hence k = k1 by A7; :: thesis: t = t1
thus t = t1 by A1, A7, A10, XCMPLX_1:2; :: thesis: verum

end;

hence ( k = k1 & t = t1 ) by A2; :: thesis: verum