let S be R -isomorphic Ring; :: thesis: ( not S is degenerated & S is domRing-like )
set f = the Isomorphism of R,S;
reconsider g = the Isomorphism of R,S " as Isomorphism of S,R by Lm7;
A1: g " = the Isomorphism of R,S ;

now :: thesis: not S is degenerated

assume A2: S is degenerated ; :: thesis: contradiction
1. R = ( the Isomorphism of R,S ") . ( the Isomorphism of R,S . (1_ R)) by FUNCT_2:26
.= ( the Isomorphism of R,S ") . (1_ S) by GROUP_1:def 13
.= ( the Isomorphism of R,S ") . ( the Isomorphism of R,S . (0. R)) by A2, RING_2:6
.= 0. R by FUNCT_2:26 ;
hence contradiction ; :: thesis: verum

end;

hence not S is degenerated ; :: thesis: S is domRing-like

now :: thesis: for x, y being Element of S holds
( not x * y = 0. S or x = 0. S or y = 0. S )

let x, y be Element of S; :: thesis: ( not x * y = 0. S or b₁ = 0. S or b₂ = 0. S )
assume A3: x * y = 0. S ; :: thesis: ( b₁ = 0. S or b₂ = 0. S )
A4: 0. R = g . (0. S) by RING_2:6
.= (g . x) * (g . y) by A3, GROUP_6:def 6 ;

per cases ( g . x = 0. R or g . y = 0. R ) by A4, VECTSP_2:def 1;

suppose g . x = 0. R ; :: thesis: ( b₁ = 0. S or b₂ = 0. S )

then 0. S = the Isomorphism of R,S . (g . x) by RING_2:6
.= x by A1, FUNCT_2:26 ;
hence ( x = 0. S or y = 0. S ) ; :: thesis: verum

end;

suppose g . y = 0. R ; :: thesis: ( b₁ = 0. S or b₂ = 0. S )

then 0. S = the Isomorphism of R,S . (g . y) by RING_2:6
.= y by A1, FUNCT_2:26 ;
hence ( x = 0. S or y = 0. S ) ; :: thesis: verum

end;

end;

end;

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