set cR = the carrier of R;
set ccs = NonZero R;
A1: not 1_ R in {(0. R)} by TARSKI:def 1;
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 consider a, b being set such that
A2: ( a in ccs & b in ccs ) and
A3: x = [a,b] by ZFMISC_1:def 2;
thus x in [:the carrier of R,the carrier of R:] by A2, A3, 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
A4: x in dom mcs and
A5: y = mcs . x by FUNCT_1:def 5;
A6: dom mcs = [:ccs,ccs:] by FUNCT_2:def 1;
then consider a, b being set such that
A7: ( a in ccs & b in ccs ) and
A8: x = [a,b] by A4, ZFMISC_1:def 2;
reconsider a = a, b = b as Element of the carrier of R by A7;
( not a in {(0. R)} & not b in {(0. R)} ) by A7, XBOOLE_0:def 5;
then ( a <> 0. R & b <> 0. R ) by TARSKI:def 1;
then a * b <> 0. R by VECTSP_2:47;
then A9: not a * b in {(0. R)} by TARSKI:def 1;
mcs . x = a * b by A4, A6, A8, FUNCT_1:72;
hence y in ccs by A5, A9, 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;

A10: 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 A11: ( 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 A11, FUNCT_1:72; :: thesis: verum

end;

A12: 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)
( x in the carrier of cs & y in the carrier of cs & z in the carrier of cs ) ;
then reconsider x' = x, y' = y, z' = z as Element of the carrier of R ;
A13: x' * y' = x * y by A10;
A14: y' * z' = y * z by A10;
thus (x * y) * z = (x' * y') * z' by A10, A13
.= x' * (y' * z') by GROUP_1:def 4
.= x * (y * z) by A10, A14 ; :: thesis: verum

end;

cs is Group-like

proof

reconsider e = 1_ R as Element of the carrier of cs by A1, 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 h' = h as Scalar of R ;
thus h * e = h' * (1_ R) by A10
.= 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) * h' by A10
.= 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 A15: h <> 0. R by TARSKI:def 1;
then h' " <> 0. R by VECTSP_2:48;
then not h' " in {(0. R)} by TARSKI:def 1;
then reconsider g = h' " as Element of the carrier of cs by XBOOLE_0:def 5;
take g ; :: thesis: ( h * g = e & g * h = e )
thus h * g = h' * (h' " ) by A10
.= e by A15, VECTSP_2:43 ; :: thesis: g * h = e
thus g * h = (h' " ) * h' by A10
.= e by A15, VECTSP_2:43 ; :: 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