set ccs = NonZero R;
set cR = the carrier of R;
reconsider ccs = NonZero R as non empty set ;
set mcs = the multF of R || ccs;
[:ccs,ccs:] c= [:the carrier of R,the carrier of R:]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [:ccs,ccs:] or x in [:the carrier of R,the carrier of R:] )
assume x in [:ccs,ccs:] ; :: thesis: x in [:the carrier of R,the carrier of R:]
then ex a, b being set st
( a in ccs & b in ccs & x = [a,b] ) by ZFMISC_1:def 2;
hence x in [:the carrier of R,the carrier of R:] by ZFMISC_1:def 2; :: thesis: verum

end;

then reconsider mcs = the multF of R || ccs as Function of [:ccs,ccs:],the carrier of R by FUNCT_2:38;
rng mcs c= ccs

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng mcs or y in ccs )
assume y in rng mcs ; :: thesis: y in ccs
then consider x being set such that
A1: x in dom mcs and
A2: y = mcs . x by FUNCT_1:def 5;
A3: dom mcs = [:ccs,ccs:] by FUNCT_2:def 1;
then consider a, b being set such that
A4: a in ccs and
A5: b in ccs and
A6: x = [a,b] by A1, ZFMISC_1:def 2;
reconsider a = a, b = b as Element of the carrier of R by A4, A5;
not b in {(0. R)} by A5, XBOOLE_0:def 5;
then A7: b <> 0. R by TARSKI:def 1;
not a in {(0. R)} by A4, XBOOLE_0:def 5;
then a <> 0. R by TARSKI:def 1;
then a * b <> 0. R by A7, VECTSP_2:47;
then A8: not a * b in {(0. R)} by TARSKI:def 1;
mcs . x = a * b by A1, A3, A6, FUNCT_1:72;
hence y in ccs by A2, A8, XBOOLE_0:def 5; :: thesis: verum

end;

then reconsider mcs = mcs as BinOp of ccs by FUNCT_2:8;
reconsider cs = multMagma(# ccs,mcs #) as non empty multMagma ;
set ccs1 = the carrier of cs;

A9: now

let a, b be Element of the carrier of R; :: thesis: for c, d being Element of the carrier of cs st a = c & b = d holds
a * b = c * d
let c, d be Element of the carrier of cs; :: thesis: ( a = c & b = d implies a * b = c * d )
assume A10: ( a = c & b = d ) ; :: thesis: a * b = c * d
[c,d] in [:ccs,ccs:] by ZFMISC_1:def 2;
hence a * b = c * d by A10, FUNCT_1:72; :: thesis: verum

end;

A11: not 1_ R in {(0. R)} by TARSKI:def 1;
A12: cs is Group-like

proof

reconsider e = 1_ R as Element of the carrier of cs by A11, XBOOLE_0:def 5;
take e ; :: according to GROUP_1:def 3 :: thesis: for b₁ being Element of the carrier of cs holds
( b₁ * e = b₁ & e * b₁ = b₁ & ex b₂ being Element of the carrier of cs st
( b₁ * b₂ = e & b₂ * b₁ = e ) )
let h be Element of the carrier of cs; :: thesis: ( h * e = h & e * h = h & ex b₁ being Element of the carrier of cs st
( h * b₁ = e & b₁ * h = e ) )
h in ccs ;
then reconsider h9 = h as Scalar of R ;
thus h * e = h9 * (1_ R) by A9
.= h by VECTSP_1:def 13 ; :: thesis: ( e * h = h & ex b₁ being Element of the carrier of cs st
( h * b₁ = e & b₁ * h = e ) )
thus e * h = (1_ R) * h9 by A9
.= h by VECTSP_1:def 19 ; :: thesis: ex b₁ being Element of the carrier of cs st
( h * b₁ = e & b₁ * h = e )
not h in {(0. R)} by XBOOLE_0:def 5;
then A13: h <> 0. R by TARSKI:def 1;
then h9 " <> 0. R by VECTSP_2:48;
then not h9 " in {(0. R)} by TARSKI:def 1;
then reconsider g = h9 " as Element of the carrier of cs by XBOOLE_0:def 5;
take g ; :: thesis: ( h * g = e & g * h = e )
thus h * g = h9 * (h9 " ) by A9
.= e by A13, VECTSP_2:43 ; :: thesis: g * h = e
thus g * h = (h9 " ) * h9 by A9
.= e by A13, VECTSP_2:43 ; :: thesis: verum

end;

cs is associative

proof

let x, y, z be Element of the carrier of cs; :: according to GROUP_1:def 4 :: thesis: (x * y) * z = x * (y * z)
A14: z in the carrier of cs ;
( x in the carrier of cs & y in the carrier of cs ) ;
then reconsider x9 = x, y9 = y, z9 = z as Element of the carrier of R by A14;
A15: y9 * z9 = y * z by A9;
x9 * y9 = x * y by A9;
hence (x * y) * z = (x9 * y9) * z9 by A9
.= x9 * (y9 * z9) by GROUP_1:def 4
.= x * (y * z) by A9, A15 ;
:: thesis: verum

end;

hence ex b₁ being strict Group st
( the carrier of b₁ = NonZero R & the multF of b₁ = the multF of R || the carrier of b₁ ) by A12; :: thesis: verum