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 ;
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 ;
hence u > 1 ; :: thesis: u < n
u <= n by ;
hence u < n by ; :: 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 ;
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 ;
hence v < n by ; :: 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
.= (u '*' (1. (Z/ n))) * (v '*' (1. (Z/ n))) by RING_3:67 ;
D: u '*' (1. (Z/ n)) <> 0. (Z/ n) by ;
v '*' (1. (Z/ n)) <> 0. (Z/ n) by ;
hence not Z/ n is domRing-like by ; :: thesis: verum