set X = FQ_Ring z;
thus FQ_Ring z is domRing-like :: thesis: ( FQ_Ring z is commutative & not FQ_Ring z is degenerated )

proof

for x, y being Element of (FQ_Ring z) holds
( not x * y = 0. (FQ_Ring z) or x = 0. (FQ_Ring z) or y = 0. (FQ_Ring z) )

proof

let x, y be Element of (FQ_Ring z); :: thesis: ( not x * y = 0. (FQ_Ring z) or x = 0. (FQ_Ring z) or y = 0. (FQ_Ring z) )
( x in F_Complex & y in F_Complex ) by Lm45;
then reconsider x1 = x, y1 = y as Element of F_Complex ;
assume A1: x * y = 0. (FQ_Ring z) ; :: thesis: ( x = 0. (FQ_Ring z) or y = 0. (FQ_Ring z) )
A2: 0. (FQ_Ring z) = 0. F_Complex by Lm48, Lm7, SUBSET_1:def 8;
then x1 * y1 = 0. F_Complex by A1, Th50;
hence ( x = 0. (FQ_Ring z) or y = 0. (FQ_Ring z) ) by A2, VECTSP_1:12; :: thesis: verum

end;

hence FQ_Ring z is domRing-like by VECTSP_2:def 1; :: thesis: verum

end;

A3: 0. (FQ_Ring z) = 0. F_Complex by Lm48, Lm7, SUBSET_1:def 8;
thus FQ_Ring z is commutative :: thesis: not FQ_Ring z is degenerated

proof

let v, w be Element of (FQ_Ring z); :: according to GROUP_1:def 12 :: thesis: v * w = w * v
( v in F_Complex & w in F_Complex ) by Lm45;
then reconsider v1 = v, w1 = w as Element of F_Complex ;
thus v * w = v1 * w1 by Th50
.= w * v by Th50 ; :: thesis: verum

end;

thus not FQ_Ring z is degenerated by Lm52, A3; :: thesis: verum