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 )

B1: ( v > 1 & v < n )

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

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

then reconsider u = u as positive Nat ;
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;hence u > 1 ; :: thesis: u < n

u <= n by A, INT_2:27;

hence u < n by A, XXREAL_0:1; :: thesis: verum

B1: ( v > 1 & v < n )

proof

then reconsider v = v as positive Nat ;
reconsider m = n as Complex ;

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;B2: now :: thesis: not v = n

not v = 0 & ... & not v = 1
by A, B;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;then (u * m) / m = 1 by B, XCMPLX_1:60;

hence contradiction by A, XCMPLX_1:89; :: thesis: verum

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

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