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:]

rng mcs c= ccs

reconsider cs = multMagma(# ccs,mcs #) as non empty multMagma ;

set ccs1 = the carrier of cs;

A12: cs is Group-like_{1} being strict Group st

( the carrier of b_{1} = NonZero R & the multF of b_{1} = the multF of R || the carrier of b_{1} )
by A12; :: thesis: verum

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

then reconsider mcs = the multF of R || ccs as Function of [:ccs,ccs:], the carrier of R by FUNCT_2:32;
let x be object ; :: 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 object 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;assume x in [:ccs,ccs:] ; :: thesis: x in [: the carrier of R, the carrier of R:]

then ex a, b being object 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

rng mcs c= ccs

proof

then reconsider mcs = mcs as BinOp of ccs by FUNCT_2:6;
let y be object ; :: 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 object such that

A1: x in dom mcs and

A2: y = mcs . x by FUNCT_1:def 3;

A3: dom mcs = [:ccs,ccs:] by FUNCT_2:def 1;

then consider a, b being object 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:12;

then A8: not a * b in {(0. R)} by TARSKI:def 1;

mcs . x = a * b by A1, A3, A6, FUNCT_1:49;

hence y in ccs by A2, A8, XBOOLE_0:def 5; :: thesis: verum

end;assume y in rng mcs ; :: thesis: y in ccs

then consider x being object such that

A1: x in dom mcs and

A2: y = mcs . x by FUNCT_1:def 3;

A3: dom mcs = [:ccs,ccs:] by FUNCT_2:def 1;

then consider a, b being object 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:12;

then A8: not a * b in {(0. R)} by TARSKI:def 1;

mcs . x = a * b by A1, A3, A6, FUNCT_1:49;

hence y in ccs by A2, A8, XBOOLE_0:def 5; :: thesis: verum

reconsider cs = multMagma(# ccs,mcs #) as non empty multMagma ;

set ccs1 = the carrier of cs;

A9: now :: thesis: for a, b being Element of the carrier of R

for c, d being Element of the carrier of cs st a = c & b = d holds

a * b = c * d

A11:
not 1_ R in {(0. R)}
by TARSKI:def 1;for c, d being Element of the carrier of cs st a = c & b = d holds

a * b = c * d

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:49; :: thesis: verum

end;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:49; :: thesis: verum

A12: cs is Group-like

proof

cs is associative
reconsider e = 1_ R as Element of the carrier of cs by A11, XBOOLE_0:def 5;

take e ; :: according to GROUP_1:def 2 :: thesis: for b_{1} being Element of the carrier of cs holds

( b_{1} * e = b_{1} & e * b_{1} = b_{1} & ex b_{2} being Element of the carrier of cs st

( b_{1} * b_{2} = e & b_{2} * b_{1} = e ) )

let h be Element of the carrier of cs; :: thesis: ( h * e = h & e * h = h & ex b_{1} being Element of the carrier of cs st

( h * b_{1} = e & b_{1} * h = e ) )

h in ccs ;

then reconsider h9 = h as Scalar of R ;

thus h * e = h9 * (1_ R) by A9

.= h ; :: thesis: ( e * h = h & ex b_{1} being Element of the carrier of cs st

( h * b_{1} = e & b_{1} * h = e ) )

thus e * h = (1_ R) * h9 by A9

.= h ; :: thesis: ex b_{1} being Element of the carrier of cs st

( h * b_{1} = e & b_{1} * 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:13;

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:9 ; :: thesis: g * h = e

thus g * h = (h9 ") * h9 by A9

.= e by A13, VECTSP_2:9 ; :: thesis: verum

end;take e ; :: according to GROUP_1:def 2 :: thesis: for b

( b

( b

let h be Element of the carrier of cs; :: thesis: ( h * e = h & e * h = h & ex b

( h * b

h in ccs ;

then reconsider h9 = h as Scalar of R ;

thus h * e = h9 * (1_ R) by A9

.= h ; :: thesis: ( e * h = h & ex b

( h * b

thus e * h = (1_ R) * h9 by A9

.= h ; :: thesis: ex b

( h * b

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:13;

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:9 ; :: thesis: g * h = e

thus g * h = (h9 ") * h9 by A9

.= e by A13, VECTSP_2:9 ; :: thesis: verum

proof

hence
ex b
let x, y, z be Element of the carrier of cs; :: according to GROUP_1:def 3 :: 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 3

.= x * (y * z) by A9, A15 ;

:: thesis: verum

end;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 3

.= x * (y * z) by A9, A15 ;

:: thesis: verum

( the carrier of b