:: by Micha{\l} Muzalewski and Wojciech Skaba

::

:: Received July 10, 1990

:: Copyright (c) 1990-2021 Association of Mizar Users

theorem Th1: :: ALGSTR_1:1

for L being non empty addLoopStr

for a, b being Element of L st ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & a + b = 0. L holds

b + a = 0. L

for a, b being Element of L st ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & a + b = 0. L holds

b + a = 0. L

proof end;

theorem :: ALGSTR_1:2

for L being non empty addLoopStr

for a being Element of L st ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) holds

(0. L) + a = a + (0. L)

for a being Element of L st ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) holds

(0. L) + a = a + (0. L)

proof end;

theorem :: ALGSTR_1:3

for L being non empty addLoopStr st ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) holds

for a being Element of L ex x being Element of L st x + a = 0. L

for a being Element of L ex x being Element of L st x + a = 0. L

proof end;

theorem :: ALGSTR_1:5

Lm1: ( ( for a being Element of Trivial-addLoopStr holds a + (0. Trivial-addLoopStr) = a ) & ( for a being Element of Trivial-addLoopStr holds (0. Trivial-addLoopStr) + a = a ) )

by Th4;

Lm2: for a, b being Element of Trivial-addLoopStr ex x being Element of Trivial-addLoopStr st a + x = b

proof end;

Lm3: for a, b being Element of Trivial-addLoopStr ex x being Element of Trivial-addLoopStr st x + a = b

proof end;

Lm4: ( ( for a, x, y being Element of Trivial-addLoopStr st a + x = a + y holds

x = y ) & ( for a, x, y being Element of Trivial-addLoopStr st x + a = y + a holds

x = y ) )

by Th4;

:: deftheorem defines left_zeroed ALGSTR_1:def 2 :

for IT being non empty addLoopStr holds

( IT is left_zeroed iff for a being Element of IT holds (0. IT) + a = a );

for IT being non empty addLoopStr holds

( IT is left_zeroed iff for a being Element of IT holds (0. IT) + a = a );

definition

let L be non empty addLoopStr ;

end;
attr L is add-left-invertible means :Def3: :: ALGSTR_1:def 3

for a, b being Element of L ex x being Element of L st x + a = b;

for a, b being Element of L ex x being Element of L st x + a = b;

attr L is add-right-invertible means :Def4: :: ALGSTR_1:def 4

for a, b being Element of L ex x being Element of L st a + x = b;

for a, b being Element of L ex x being Element of L st a + x = b;

:: deftheorem Def3 defines add-left-invertible ALGSTR_1:def 3 :

for L being non empty addLoopStr holds

( L is add-left-invertible iff for a, b being Element of L ex x being Element of L st x + a = b );

for L being non empty addLoopStr holds

( L is add-left-invertible iff for a, b being Element of L ex x being Element of L st x + a = b );

:: deftheorem Def4 defines add-right-invertible ALGSTR_1:def 4 :

for L being non empty addLoopStr holds

( L is add-right-invertible iff for a, b being Element of L ex x being Element of L st a + x = b );

for L being non empty addLoopStr holds

( L is add-right-invertible iff for a, b being Element of L ex x being Element of L st a + x = b );

definition

let IT be non empty addLoopStr ;

end;
attr IT is Loop-like means :: ALGSTR_1:def 5

( IT is left_add-cancelable & IT is right_add-cancelable & IT is add-left-invertible & IT is add-right-invertible );

( IT is left_add-cancelable & IT is right_add-cancelable & IT is add-left-invertible & IT is add-right-invertible );

:: deftheorem defines Loop-like ALGSTR_1:def 5 :

for IT being non empty addLoopStr holds

( IT is Loop-like iff ( IT is left_add-cancelable & IT is right_add-cancelable & IT is add-left-invertible & IT is add-right-invertible ) );

for IT being non empty addLoopStr holds

( IT is Loop-like iff ( IT is left_add-cancelable & IT is right_add-cancelable & IT is add-left-invertible & IT is add-right-invertible ) );

registration

for b_{1} being non empty addLoopStr st b_{1} is Loop-like holds

( b_{1} is left_add-cancelable & b_{1} is right_add-cancelable & b_{1} is add-left-invertible & b_{1} is add-right-invertible )
;

for b_{1} being non empty addLoopStr st b_{1} is left_add-cancelable & b_{1} is right_add-cancelable & b_{1} is add-left-invertible & b_{1} is add-right-invertible holds

b_{1} is Loop-like
;

end;

cluster non empty Loop-like -> non empty left_add-cancelable right_add-cancelable add-left-invertible add-right-invertible for addLoopStr ;

coherence for b

( b

cluster non empty left_add-cancelable right_add-cancelable add-left-invertible add-right-invertible -> non empty Loop-like for addLoopStr ;

coherence for b

b

theorem Th6: :: ALGSTR_1:6

for L being non empty addLoopStr holds

( L is Loop-like iff ( ( for a, b being Element of L ex x being Element of L st a + x = b ) & ( for a, b being Element of L ex x being Element of L st x + a = b ) & ( for a, x, y being Element of L st a + x = a + y holds

x = y ) & ( for a, x, y being Element of L st x + a = y + a holds

x = y ) ) )

( L is Loop-like iff ( ( for a, b being Element of L ex x being Element of L st a + x = b ) & ( for a, b being Element of L ex x being Element of L st x + a = b ) & ( for a, x, y being Element of L st a + x = a + y holds

x = y ) & ( for a, x, y being Element of L st x + a = y + a holds

x = y ) ) )

proof end;

Lm5: for a, b, c being Element of Trivial-addLoopStr holds (a + b) + c = a + (b + c)

by Th4;

Lm6: for a, b being Element of Trivial-addLoopStr holds a + b = b + a

by Th4;

registration

coherence

( Trivial-addLoopStr is add-associative & Trivial-addLoopStr is Loop-like & Trivial-addLoopStr is right_zeroed & Trivial-addLoopStr is left_zeroed ) by Lm1, Lm2, Lm3, Lm4, Lm5, Th6;

end;
( Trivial-addLoopStr is add-associative & Trivial-addLoopStr is Loop-like & Trivial-addLoopStr is right_zeroed & Trivial-addLoopStr is left_zeroed ) by Lm1, Lm2, Lm3, Lm4, Lm5, Th6;

registration

existence

ex b_{1} being non empty addLoopStr st

( b_{1} is strict & b_{1} is left_zeroed & b_{1} is right_zeroed & b_{1} is Loop-like )

end;
ex b

( b

proof end;

registration

ex b_{1} being Loop st

( b_{1} is strict & b_{1} is add-associative )
end;

cluster non empty left_add-cancelable right_add-cancelable add-cancelable strict add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like for addLoopStr ;

existence ex b

( b

proof end;

registration

coherence

for b_{1} being non empty addLoopStr st b_{1} is Loop-like holds

b_{1} is add-left-invertible
;

for b_{1} being non empty addLoopStr st b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable holds

( b_{1} is left_zeroed & b_{1} is Loop-like )

end;
for b

b

cluster non empty right_complementable add-associative right_zeroed -> non empty left_zeroed Loop-like for addLoopStr ;

coherence for b

( b

proof end;

theorem Th7: :: ALGSTR_1:7

for L being non empty addLoopStr holds

( L is AddGroup iff ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) ) )

( L is AddGroup iff ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) ) )

proof end;

registration
end;

registration

ex b_{1} being AddGroup st

( b_{1} is strict & b_{1} is Abelian )
end;

cluster non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like for addLoopStr ;

existence ex b

( b

proof end;

theorem :: ALGSTR_1:8

for L being non empty addLoopStr holds

( L is Abelian AddGroup iff ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) ) ) by Th7, RLVECT_1:def 2;

( L is Abelian AddGroup iff ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) ) ) by Th7, RLVECT_1:def 2;

registration
end;

theorem :: ALGSTR_1:10

Lm7: ( ( for a being Element of Trivial-multLoopStr holds a * (1. Trivial-multLoopStr) = a ) & ( for a being Element of Trivial-multLoopStr holds (1. Trivial-multLoopStr) * a = a ) )

by Th9;

Lm8: for a, b being Element of Trivial-multLoopStr ex x being Element of Trivial-multLoopStr st a * x = b

proof end;

Lm9: for a, b being Element of Trivial-multLoopStr ex x being Element of Trivial-multLoopStr st x * a = b

proof end;

:: deftheorem Def6 defines invertible ALGSTR_1:def 6 :

for IT being non empty multLoopStr holds

( IT is invertible iff ( ( for a, b being Element of IT ex x being Element of IT st a * x = b ) & ( for a, b being Element of IT ex x being Element of IT st x * a = b ) ) );

for IT being non empty multLoopStr holds

( IT is invertible iff ( ( for a, b being Element of IT ex x being Element of IT st a * x = b ) & ( for a, b being Element of IT ex x being Element of IT st x * a = b ) ) );

registration

existence

ex b_{1} being non empty multLoopStr st

( b_{1} is strict & b_{1} is well-unital & b_{1} is invertible & b_{1} is cancelable )

end;
ex b

( b

proof end;

registration

coherence

( Trivial-multLoopStr is well-unital & Trivial-multLoopStr is invertible & Trivial-multLoopStr is cancelable ) by Lm7, Lm8, Lm9;

end;
( Trivial-multLoopStr is well-unital & Trivial-multLoopStr is invertible & Trivial-multLoopStr is cancelable ) by Lm7, Lm8, Lm9;

Lm10: for a, b, c being Element of Trivial-multLoopStr holds (a * b) * c = a * (b * c)

by Th9;

registration

ex b_{1} being multLoop st

( b_{1} is strict & b_{1} is associative )
end;

cluster non empty left_mult-cancelable right_mult-cancelable cancelable strict right_unital well-unital left_unital unital associative invertible for multLoopStr ;

existence ex b

( b

proof end;

Lm11: for L being non empty multLoopStr

for a, b being Element of L st ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & a * b = 1. L holds

b * a = 1. L

proof end;

Lm12: for L being non empty multLoopStr

for a being Element of L st ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) holds

(1. L) * a = a * (1. L)

proof end;

Lm13: for L being non empty multLoopStr st ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) holds

for a being Element of L ex x being Element of L st x * a = 1. L

proof end;

theorem Th11: :: ALGSTR_1:11

for L being non empty multLoopStr holds

( L is multGroup iff ( ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) ) )

( L is multGroup iff ( ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) ) )

proof end;

registration
end;

Lm14: for a, b being Element of Trivial-multLoopStr holds a * b = b * a

by Th9;

registration

ex b_{1} being multGroup st

( b_{1} is strict & b_{1} is commutative )
end;

cluster non empty left_mult-cancelable right_mult-cancelable cancelable strict right_unital well-unital left_unital unital associative commutative invertible for multLoopStr ;

existence ex b

( b

proof end;

theorem :: ALGSTR_1:12

for L being non empty multLoopStr holds

( L is commutative multGroup iff ( ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a, b being Element of L holds a * b = b * a ) ) ) by Th11, GROUP_1:def 12;

( L is commutative multGroup iff ( ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a, b being Element of L holds a * b = b * a ) ) ) by Th11, GROUP_1:def 12;

notation
end;

registration

let L be non empty cancelable invertible multLoopStr ;

coherence

for b_{1} being Element of L holds b_{1} is left_invertible
by Def6;

end;
coherence

for b

canceled;

definition

coherence

multLoopStr_0(# REAL,multreal,(In (0,REAL)),(In (1,REAL)) #) is strict multLoopStr_0 ;

;

end;

func multEX_0 -> strict multLoopStr_0 equals :: ALGSTR_1:def 7

multLoopStr_0(# REAL,multreal,(In (0,REAL)),(In (1,REAL)) #);

correctness multLoopStr_0(# REAL,multreal,(In (0,REAL)),(In (1,REAL)) #);

coherence

multLoopStr_0(# REAL,multreal,(In (0,REAL)),(In (1,REAL)) #) is strict multLoopStr_0 ;

;

:: deftheorem defines multEX_0 ALGSTR_1:def 7 :

multEX_0 = multLoopStr_0(# REAL,multreal,(In (0,REAL)),(In (1,REAL)) #);

multEX_0 = multLoopStr_0(# REAL,multreal,(In (0,REAL)),(In (1,REAL)) #);

Lm15: now :: thesis: for x, e being Element of multEX_0 st e = 1 holds

( x * e = x & e * x = x )

( x * e = x & e * x = x )

let x, e be Element of multEX_0; :: thesis: ( e = 1 implies ( x * e = x & e * x = x ) )

reconsider a = x as Real ;

assume A1: e = 1 ; :: thesis: ( x * e = x & e * x = x )

hence x * e = a * 1 by BINOP_2:def 11

.= x ;

:: thesis: e * x = x

thus e * x = 1 * a by A1, BINOP_2:def 11

.= x ; :: thesis: verum

end;
reconsider a = x as Real ;

assume A1: e = 1 ; :: thesis: ( x * e = x & e * x = x )

hence x * e = a * 1 by BINOP_2:def 11

.= x ;

:: thesis: e * x = x

thus e * x = 1 * a by A1, BINOP_2:def 11

.= x ; :: thesis: verum

registration
end;

Lm16: for a, b being Element of multEX_0 st a <> 0. multEX_0 holds

ex x being Element of multEX_0 st a * x = b

proof end;

Lm17: for a, b being Element of multEX_0 st a <> 0. multEX_0 holds

ex x being Element of multEX_0 st x * a = b

proof end;

Lm18: for a, x, y being Element of multEX_0 st a <> 0. multEX_0 & a * x = a * y holds

x = y

proof end;

Lm19: for a, x, y being Element of multEX_0 st a <> 0. multEX_0 & x * a = y * a holds

x = y

proof end;

Lm20: for a being Element of multEX_0 holds a * (0. multEX_0) = 0. multEX_0

proof end;

Lm21: for a being Element of multEX_0 holds (0. multEX_0) * a = 0. multEX_0

proof end;

:: deftheorem Def8 defines almost_invertible ALGSTR_1:def 8 :

for IT being non empty multLoopStr_0 holds

( IT is almost_invertible iff ( ( for a, b being Element of IT st a <> 0. IT holds

ex x being Element of IT st a * x = b ) & ( for a, b being Element of IT st a <> 0. IT holds

ex x being Element of IT st x * a = b ) ) );

for IT being non empty multLoopStr_0 holds

( IT is almost_invertible iff ( ( for a, b being Element of IT st a <> 0. IT holds

ex x being Element of IT st a * x = b ) & ( for a, b being Element of IT st a <> 0. IT holds

ex x being Element of IT st x * a = b ) ) );

definition

let IT be non empty multLoopStr_0 ;

end;
attr IT is multLoop_0-like means :: ALGSTR_1:def 9

( IT is almost_invertible & IT is almost_cancelable & ( for a being Element of IT holds a * (0. IT) = 0. IT ) & ( for a being Element of IT holds (0. IT) * a = 0. IT ) );

( IT is almost_invertible & IT is almost_cancelable & ( for a being Element of IT holds a * (0. IT) = 0. IT ) & ( for a being Element of IT holds (0. IT) * a = 0. IT ) );

:: deftheorem defines multLoop_0-like ALGSTR_1:def 9 :

for IT being non empty multLoopStr_0 holds

( IT is multLoop_0-like iff ( IT is almost_invertible & IT is almost_cancelable & ( for a being Element of IT holds a * (0. IT) = 0. IT ) & ( for a being Element of IT holds (0. IT) * a = 0. IT ) ) );

for IT being non empty multLoopStr_0 holds

( IT is multLoop_0-like iff ( IT is almost_invertible & IT is almost_cancelable & ( for a being Element of IT holds a * (0. IT) = 0. IT ) & ( for a being Element of IT holds (0. IT) * a = 0. IT ) ) );

::$CT 2

theorem Th14: :: ALGSTR_1:16

for L being non empty multLoopStr_0 holds

( L is multLoop_0-like iff ( ( for a, b being Element of L st a <> 0. L holds

ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds

ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds

x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds

x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) ) )

( L is multLoop_0-like iff ( ( for a, b being Element of L st a <> 0. L holds

ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds

ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds

x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds

x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) ) )

proof end;

registration

for b_{1} being non empty multLoopStr_0 st b_{1} is multLoop_0-like holds

( b_{1} is almost_invertible & b_{1} is almost_cancelable )
;

end;

cluster non empty multLoop_0-like -> non empty almost_cancelable almost_invertible for multLoopStr_0 ;

coherence for b

( b

registration

existence

ex b_{1} being non empty multLoopStr_0 st

( b_{1} is strict & b_{1} is well-unital & b_{1} is multLoop_0-like & not b_{1} is degenerated )

end;
ex b

( b

proof end;

definition
end;

registration

coherence

( multEX_0 is well-unital & multEX_0 is multLoop_0-like ) by Lm16, Lm17, Lm18, Lm19, Lm20, Lm21, Th14;

end;
( multEX_0 is well-unital & multEX_0 is multLoop_0-like ) by Lm16, Lm17, Lm18, Lm19, Lm20, Lm21, Th14;

Lm22: for a, b, c being Element of multEX_0 holds (a * b) * c = a * (b * c)

proof end;

registration

ex b_{1} being multLoop_0 st

( b_{1} is strict & b_{1} is associative & not b_{1} is degenerated )
end;

cluster non empty non degenerated non trivial strict almost_left_cancelable almost_right_cancelable almost_cancelable right_unital well-unital left_unital unital associative almost_invertible multLoop_0-like for multLoopStr_0 ;

existence ex b

( b

proof end;

registration
end;

Lm23: for a, b being Element of multEX_0 holds a * b = b * a

proof end;

registration

ex b_{1} being multGroup_0 st

( b_{1} is strict & b_{1} is commutative )
end;

cluster non empty non degenerated non trivial strict almost_left_cancelable almost_right_cancelable almost_cancelable right_unital well-unital left_unital unital associative commutative almost_invertible multLoop_0-like for multLoopStr_0 ;

existence ex b

( b

proof end;

notation

let L be non empty almost_cancelable almost_invertible multLoopStr_0 ;

let x be Element of L;

synonym x " for / x;

end;
let x be Element of L;

synonym x " for / x;

definition

let L be non empty almost_cancelable almost_invertible multLoopStr_0 ;

let x be Element of L;

assume A1: x <> 0. L ;

compatibility

for b_{1} being Element of the carrier of L holds

( b_{1} = x " iff b_{1} * x = 1. L )

end;
let x be Element of L;

assume A1: x <> 0. L ;

compatibility

for b

( b

proof end;

:: deftheorem Def10 defines " ALGSTR_1:def 10 :

for L being non empty almost_cancelable almost_invertible multLoopStr_0

for x being Element of L st x <> 0. L holds

for b_{3} being Element of the carrier of L holds

( b_{3} = x " iff b_{3} * x = 1. L );

for L being non empty almost_cancelable almost_invertible multLoopStr_0

for x being Element of L st x <> 0. L holds

for b

( b

theorem :: ALGSTR_1:17

for G being non empty almost_cancelable well-unital associative almost_invertible multLoopStr_0

for a being Element of G st a <> 0. G holds

( (a ") * a = 1. G & a * (a ") = 1. G )

for a being Element of G st a <> 0. G holds

( (a ") * a = 1. G & a * (a ") = 1. G )

proof end;

definition

let L be non empty almost_cancelable almost_invertible multLoopStr_0 ;

let a, b be Element of L;

correctness

coherence

a * (b ") is Element of L;

;

end;
let a, b be Element of L;

correctness

coherence

a * (b ") is Element of L;

;

:: deftheorem defines / ALGSTR_1:def 11 :

for L being non empty almost_cancelable almost_invertible multLoopStr_0

for a, b being Element of L holds a / b = a * (b ");

for L being non empty almost_cancelable almost_invertible multLoopStr_0

for a, b being Element of L holds a / b = a * (b ");

:: from SCMRING1, 2010,02.06, A.T.

registration

for b_{1} being 1 -element addLoopStr holds

( b_{1} is Abelian & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable )

for b_{1} being non empty doubleLoopStr st b_{1} is trivial holds

( b_{1} is well-unital & b_{1} is right-distributive )
;

end;

cluster 1 -element -> 1 -element right_complementable Abelian add-associative right_zeroed for addLoopStr ;

coherence for b

( b

proof end;

coherence for b

( b

registration

coherence

for b_{1} being 1 -element multMagma holds

( b_{1} is Group-like & b_{1} is associative & b_{1} is commutative )

end;
for b

( b

proof end;

:: let L be invertible cancelable non empty multLoopStr;

:: let a, b be Element of L;

:: func a/b -> Element of L equals

:: a*(b");

:: correctness;

:: end;

::$CD