set R = Z/ n;
not n = 0 & ... & not n = 1 by NAT_2:def 1;
then n > 1 ;
then consider u being Nat such that
A: ( u divides n & u <> 1 & u <> n ) by INT_2:def 4;
consider v being Integer such that
B: u * v = n by A, INT_1:def 3;
v >= 0 by B;
then v in NAT by INT_1:3;
then reconsider v = v as Nat ;
A1: ( u > 1 & u < n )
proof
not u = 0 & ... & not u = 1 by A, INT_2:3;
hence u > 1 ; :: thesis: u < n
u <= n by A, INT_2:27;
hence u < n by A, XXREAL_0:1; :: thesis: verum
end;
then reconsider u = u as positive Nat ;
B1: ( v > 1 & v < n )
proof
reconsider m = n as Complex ;
B2: now :: thesis: not v = n
assume v = n ; :: thesis: contradiction
then (u * m) / m = 1 by B, XCMPLX_1:60;
hence contradiction by A, XCMPLX_1:89; :: thesis: verum
end;
not v = 0 & ... & not v = 1 by A, B;
hence v > 1 ; :: thesis: v < n
v <= n by B, INT_1:def 3, INT_2:27;
hence v < n by B2, XXREAL_0:1; :: thesis: verum
end;
then reconsider v = v as positive Nat ;
V: Char (Z/ n) = n by RING_3:def 6;
then C: 0. (Z/ n) = (u * v) '*' (1. (Z/ n)) by B, RING_3:def 5
.= (u '*' (1. (Z/ n))) * (v '*' (1. (Z/ n))) by RING_3:67 ;
D: u '*' (1. (Z/ n)) <> 0. (Z/ n) by V, A1, RING_3:def 5;
v '*' (1. (Z/ n)) <> 0. (Z/ n) by V, B1, RING_3:def 5;
hence not Z/ n is domRing-like by C, D, VECTSP_2:def 1; :: thesis: verum