:: ALGSTR_1 semantic presentation
begin
theorem
:: ALGSTR_1:1
for
L
being ( ( non
empty
) ( non
empty
)
addLoopStr
)
for
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st ( for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
(
0.
L
: ( ( non
empty
) ( non
empty
)
addLoopStr
)
)
: ( ( ) (
V51
(
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) & ( for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ex
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
0.
L
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) (
V51
(
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) ) & ( for
a
,
b
,
c
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) )
+
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
(
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) ) &
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
0.
L
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) (
V51
(
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) holds
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
0.
L
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) (
V51
(
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: ALGSTR_1:2
for
L
being ( ( non
empty
) ( non
empty
)
addLoopStr
)
for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st ( for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
(
0.
L
: ( ( non
empty
) ( non
empty
)
addLoopStr
)
)
: ( ( ) (
V51
(
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) & ( for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ex
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
0.
L
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) (
V51
(
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) ) & ( for
a
,
b
,
c
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) )
+
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
(
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) ) holds
(
0.
L
: ( ( non
empty
) ( non
empty
)
addLoopStr
)
)
: ( ( ) (
V51
(
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) )
+
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
(
0.
L
: ( ( non
empty
) ( non
empty
)
addLoopStr
)
)
: ( ( ) (
V51
(
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: ALGSTR_1:3
for
L
being ( ( non
empty
) ( non
empty
)
addLoopStr
) st ( for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
(
0.
L
: ( ( non
empty
) ( non
empty
)
addLoopStr
)
)
: ( ( ) (
V51
(
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) & ( for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ex
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
0.
L
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) (
V51
(
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) ) & ( for
a
,
b
,
c
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) )
+
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
(
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) ) holds
for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ex
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
0.
L
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) (
V51
(
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) ;
definition
let
x
be ( ( ) ( )
set
) ;
func
Extract
x
->
( ( ) ( )
Element
of
{
x
: ( ( ) ( )
RLSStruct
)
}
: ( ( ) ( non
empty
trivial
V42
(1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) ) ) )
set
) )
equals
:: ALGSTR_1:def 1
x
: ( ( ) ( )
RLSStruct
) ;
end;
theorem
:: ALGSTR_1:4
for
a
,
b
being ( ( ) (
left_add-cancelable
right_add-cancelable
add-cancelable
left_complementable
right_complementable
complementable
)
Element
of ( ( ) ( non
empty
trivial
V35
()
V42
(1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) ) ) )
set
) ) holds
a
: ( ( ) (
left_add-cancelable
right_add-cancelable
add-cancelable
left_complementable
right_complementable
complementable
)
Element
of ( ( ) ( non
empty
trivial
V35
()
V42
(1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) ) ) )
set
) )
=
b
: ( ( ) (
left_add-cancelable
right_add-cancelable
add-cancelable
left_complementable
right_complementable
complementable
)
Element
of ( ( ) ( non
empty
trivial
V35
()
V42
(1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) ) ) )
set
) ) ;
theorem
:: ALGSTR_1:5
for
a
,
b
being ( ( ) (
left_add-cancelable
right_add-cancelable
add-cancelable
left_complementable
right_complementable
complementable
)
Element
of ( ( ) ( non
empty
trivial
V35
()
V42
(1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) ) ) )
set
) ) holds
a
: ( ( ) (
left_add-cancelable
right_add-cancelable
add-cancelable
left_complementable
right_complementable
complementable
)
Element
of ( ( ) ( non
empty
trivial
V35
()
V42
(1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) ) ) )
set
) )
+
b
: ( ( ) (
left_add-cancelable
right_add-cancelable
add-cancelable
left_complementable
right_complementable
complementable
)
Element
of ( ( ) ( non
empty
trivial
V35
()
V42
(1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) ) ) )
set
) ) : ( ( ) (
left_add-cancelable
right_add-cancelable
add-cancelable
left_complementable
right_complementable
complementable
)
Element
of the
carrier
of
Trivial-addLoopStr
: ( ( ) ( non
empty
trivial
V50
() 1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) )
-element
left_add-cancelable
right_add-cancelable
add-cancelable
strict
left_complementable
right_complementable
complementable
)
addLoopStr
) : ( ( ) ( non
empty
trivial
V35
()
V42
(1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) ) ) )
set
) )
=
0.
Trivial-addLoopStr
: ( ( ) ( non
empty
trivial
V50
() 1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) )
-element
left_add-cancelable
right_add-cancelable
add-cancelable
strict
left_complementable
right_complementable
complementable
)
addLoopStr
) : ( ( ) (
V51
(
Trivial-addLoopStr
: ( ( ) ( non
empty
trivial
V50
() 1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) )
-element
left_add-cancelable
right_add-cancelable
add-cancelable
strict
left_complementable
right_complementable
complementable
)
addLoopStr
) )
left_add-cancelable
right_add-cancelable
add-cancelable
left_complementable
right_complementable
complementable
)
Element
of the
carrier
of
Trivial-addLoopStr
: ( ( ) ( non
empty
trivial
V50
() 1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) )
-element
left_add-cancelable
right_add-cancelable
add-cancelable
strict
left_complementable
right_complementable
complementable
)
addLoopStr
) : ( ( ) ( non
empty
trivial
V35
()
V42
(1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) ) ) )
set
) ) ;
definition
let
IT
be ( ( non
empty
) ( non
empty
)
addLoopStr
) ;
attr
IT
is
left_zeroed
means
:: ALGSTR_1:def 2
for
a
being ( ( ) ( )
Element
of ( ( ) ( )
set
) ) holds
(
0.
IT
: ( ( ) ( )
RLSStruct
)
)
: ( ( ) (
V51
(
IT
: ( ( ) ( )
RLSStruct
) ) )
Element
of the
carrier
of
IT
: ( ( ) ( )
RLSStruct
) : ( ( ) ( )
set
) )
+
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
IT
: ( ( ) ( )
RLSStruct
) : ( ( ) ( )
set
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
end;
definition
let
L
be ( ( non
empty
) ( non
empty
)
addLoopStr
) ;
attr
L
is
add-left-invertible
means
:: ALGSTR_1:def 3
for
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( )
set
) ) ex
x
being ( ( ) ( )
Element
of ( ( ) ( )
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
L
: ( ( ) ( )
RLSStruct
) : ( ( ) ( )
set
) )
=
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
attr
L
is
add-right-invertible
means
:: ALGSTR_1:def 4
for
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( )
set
) ) ex
x
being ( ( ) ( )
Element
of ( ( ) ( )
set
) ) st
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
L
: ( ( ) ( )
RLSStruct
) : ( ( ) ( )
set
) )
=
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
end;
definition
let
IT
be ( ( non
empty
) ( non
empty
)
addLoopStr
) ;
attr
IT
is
Loop-like
means
:: ALGSTR_1:def 5
(
IT
: ( ( ) ( )
RLSStruct
) is
left_add-cancelable
&
IT
: ( ( ) ( )
RLSStruct
) is
right_add-cancelable
&
IT
: ( ( ) ( )
RLSStruct
) is
add-left-invertible
&
IT
: ( ( ) ( )
RLSStruct
) is
add-right-invertible
);
end;
registration
cluster
non
empty
Loop-like
->
non
empty
left_add-cancelable
right_add-cancelable
add-left-invertible
add-right-invertible
for ( ( ) ( )
addLoopStr
) ;
cluster
non
empty
left_add-cancelable
right_add-cancelable
add-left-invertible
add-right-invertible
->
non
empty
Loop-like
for ( ( ) ( )
addLoopStr
) ;
end;
theorem
:: ALGSTR_1:6
for
L
being ( ( non
empty
) ( non
empty
)
addLoopStr
) holds
(
L
: ( ( non
empty
) ( non
empty
)
addLoopStr
) is
Loop-like
iff ( ( for
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ex
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) & ( for
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ex
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) & ( for
a
,
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) & ( for
a
,
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ) ) ;
registration
cluster
Trivial-addLoopStr
: ( ( ) ( non
empty
trivial
V50
() 1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) )
-element
left_add-cancelable
right_add-cancelable
add-cancelable
strict
left_complementable
right_complementable
complementable
)
addLoopStr
)
->
add-associative
right_zeroed
left_zeroed
Loop-like
;
end;
registration
cluster
non
empty
strict
right_zeroed
left_zeroed
Loop-like
for ( ( ) ( )
addLoopStr
) ;
end;
definition
mode
Loop
is
( ( non
empty
right_zeroed
left_zeroed
Loop-like
) ( non
empty
left_add-cancelable
right_add-cancelable
add-cancelable
right_zeroed
left_zeroed
add-left-invertible
add-right-invertible
Loop-like
)
addLoopStr
) ;
end;
registration
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
) ;
end;
registration
cluster
non
empty
Loop-like
->
non
empty
add-left-invertible
for ( ( ) ( )
addLoopStr
) ;
cluster
non
empty
right_complementable
add-associative
right_zeroed
->
non
empty
left_zeroed
Loop-like
for ( ( ) ( )
addLoopStr
) ;
end;
theorem
:: ALGSTR_1:7
for
L
being ( ( non
empty
) ( non
empty
)
addLoopStr
) holds
(
L
: ( ( non
empty
) ( non
empty
)
addLoopStr
) is ( ( non
empty
right_complementable
add-associative
right_zeroed
) ( non
empty
left_add-cancelable
right_add-cancelable
add-cancelable
right_complementable
add-associative
right_zeroed
left_zeroed
add-left-invertible
add-right-invertible
Loop-like
)
AddGroup
) iff ( ( for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
(
0.
L
: ( ( non
empty
) ( non
empty
)
addLoopStr
)
)
: ( ( ) (
V51
(
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) & ( for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ex
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
0.
L
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) (
V51
(
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) ) & ( for
a
,
b
,
c
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) )
+
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
(
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) ) ) ) ;
registration
cluster
Trivial-addLoopStr
: ( ( ) ( non
empty
trivial
V50
() 1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) )
-element
left_add-cancelable
right_add-cancelable
add-cancelable
strict
left_complementable
right_complementable
complementable
add-associative
right_zeroed
left_zeroed
add-left-invertible
add-right-invertible
Loop-like
)
addLoopStr
)
->
Abelian
;
end;
registration
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
) ;
end;
theorem
:: ALGSTR_1:8
for
L
being ( ( non
empty
) ( non
empty
)
addLoopStr
) holds
(
L
: ( ( non
empty
) ( non
empty
)
addLoopStr
) is ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_add-cancelable
right_add-cancelable
add-cancelable
right_complementable
Abelian
add-associative
right_zeroed
left_zeroed
add-left-invertible
add-right-invertible
Loop-like
)
AddGroup
) iff ( ( for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
(
0.
L
: ( ( non
empty
) ( non
empty
)
addLoopStr
)
)
: ( ( ) (
V51
(
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) & ( for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ex
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
0.
L
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) (
V51
(
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) ) & ( for
a
,
b
,
c
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) )
+
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
(
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) ) & ( for
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) ) ) ) ;
registration
cluster
Trivial-multLoopStr
: ( ( ) ( non
empty
trivial
V50
() 1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) )
-element
left_mult-cancelable
right_mult-cancelable
cancelable
strict
left_invertible
right_invertible
invertible
)
multLoopStr
)
->
non
empty
;
end;
theorem
:: ALGSTR_1:9
for
a
,
b
being ( ( ) (
left_mult-cancelable
right_mult-cancelable
mult-cancelable
left_invertible
right_invertible
invertible
)
Element
of ( ( ) ( non
empty
trivial
V35
()
V42
(1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) ) ) )
set
) ) holds
a
: ( ( ) (
left_mult-cancelable
right_mult-cancelable
mult-cancelable
left_invertible
right_invertible
invertible
)
Element
of ( ( ) ( non
empty
trivial
V35
()
V42
(1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) ) ) )
set
) )
=
b
: ( ( ) (
left_mult-cancelable
right_mult-cancelable
mult-cancelable
left_invertible
right_invertible
invertible
)
Element
of ( ( ) ( non
empty
trivial
V35
()
V42
(1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) ) ) )
set
) ) ;
theorem
:: ALGSTR_1:10
for
a
,
b
being ( ( ) (
left_mult-cancelable
right_mult-cancelable
mult-cancelable
left_invertible
right_invertible
invertible
)
Element
of ( ( ) ( non
empty
trivial
V35
()
V42
(1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) ) ) )
set
) ) holds
a
: ( ( ) (
left_mult-cancelable
right_mult-cancelable
mult-cancelable
left_invertible
right_invertible
invertible
)
Element
of ( ( ) ( non
empty
trivial
V35
()
V42
(1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) ) ) )
set
) )
*
b
: ( ( ) (
left_mult-cancelable
right_mult-cancelable
mult-cancelable
left_invertible
right_invertible
invertible
)
Element
of ( ( ) ( non
empty
trivial
V35
()
V42
(1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) ) ) )
set
) ) : ( ( ) (
left_mult-cancelable
right_mult-cancelable
mult-cancelable
left_invertible
right_invertible
invertible
)
Element
of the
carrier
of
Trivial-multLoopStr
: ( ( ) ( non
empty
trivial
V50
() 1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) )
-element
left_mult-cancelable
right_mult-cancelable
cancelable
strict
left_invertible
right_invertible
invertible
)
multLoopStr
) : ( ( ) ( non
empty
trivial
V35
()
V42
(1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) ) ) )
set
) )
=
1.
Trivial-multLoopStr
: ( ( ) ( non
empty
trivial
V50
() 1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) )
-element
left_mult-cancelable
right_mult-cancelable
cancelable
strict
left_invertible
right_invertible
invertible
)
multLoopStr
) : ( ( ) (
left_mult-cancelable
right_mult-cancelable
mult-cancelable
left_invertible
right_invertible
invertible
)
Element
of the
carrier
of
Trivial-multLoopStr
: ( ( ) ( non
empty
trivial
V50
() 1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) )
-element
left_mult-cancelable
right_mult-cancelable
cancelable
strict
left_invertible
right_invertible
invertible
)
multLoopStr
) : ( ( ) ( non
empty
trivial
V35
()
V42
(1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) ) ) )
set
) ) ;
definition
let
IT
be ( ( non
empty
) ( non
empty
)
multLoopStr
) ;
attr
IT
is
invertible
means
:: ALGSTR_1:def 6
( ( for
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( )
set
) ) ex
x
being ( ( ) ( )
Element
of ( ( ) ( )
set
) ) st
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
IT
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) : ( ( ) ( )
set
) )
=
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) & ( for
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( )
set
) ) ex
x
being ( ( ) ( )
Element
of ( ( ) ( )
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
IT
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) : ( ( ) ( )
set
) )
=
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) );
end;
notation
let
L
be ( ( non
empty
) ( non
empty
)
multLoopStr
) ;
synonym
cancelable
L
for
mult-cancelable
;
end;
registration
cluster
non
empty
cancelable
strict
well-unital
invertible
for ( ( ) ( )
multLoopStr
) ;
end;
definition
mode
multLoop
is
( ( non
empty
cancelable
well-unital
invertible
) ( non
empty
left_mult-cancelable
right_mult-cancelable
cancelable
unital
right_unital
well-unital
left_unital
invertible
)
multLoopStr
) ;
end;
registration
cluster
Trivial-multLoopStr
: ( ( ) ( non
empty
trivial
V50
() 1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) )
-element
left_mult-cancelable
right_mult-cancelable
cancelable
strict
left_invertible
right_invertible
invertible
)
multLoopStr
)
->
cancelable
well-unital
invertible
;
end;
registration
cluster
non
empty
left_mult-cancelable
right_mult-cancelable
cancelable
strict
unital
associative
right_unital
well-unital
left_unital
invertible
for ( ( ) ( )
multLoopStr
) ;
end;
definition
mode
multGroup
is
( ( non
empty
cancelable
associative
well-unital
invertible
) ( non
empty
left_mult-cancelable
right_mult-cancelable
cancelable
unital
associative
right_unital
well-unital
left_unital
invertible
)
multLoop
) ;
end;
theorem
:: ALGSTR_1:11
for
L
being ( ( non
empty
) ( non
empty
)
multLoopStr
) holds
(
L
: ( ( non
empty
) ( non
empty
)
multLoopStr
) is ( ( non
empty
cancelable
associative
well-unital
invertible
) ( non
empty
left_mult-cancelable
right_mult-cancelable
cancelable
unital
associative
right_unital
well-unital
left_unital
invertible
)
multGroup
) iff ( ( for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
(
1.
L
: ( ( non
empty
) ( non
empty
)
multLoopStr
)
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) & ( for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ex
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
1.
L
: ( ( non
empty
) ( non
empty
)
multLoopStr
) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr
) : ( ( ) ( non
empty
)
set
) ) ) & ( for
a
,
b
,
c
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr
) : ( ( ) ( non
empty
)
set
) )
*
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
(
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr
) : ( ( ) ( non
empty
)
set
) ) ) ) ) ;
registration
cluster
Trivial-multLoopStr
: ( ( ) ( non
empty
trivial
V50
() 1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) )
-element
left_mult-cancelable
right_mult-cancelable
cancelable
strict
left_invertible
right_invertible
invertible
unital
right_unital
well-unital
left_unital
invertible
)
multLoopStr
)
->
associative
;
end;
registration
cluster
non
empty
left_mult-cancelable
right_mult-cancelable
cancelable
strict
unital
associative
commutative
right_unital
well-unital
left_unital
invertible
for ( ( ) ( )
multLoopStr
) ;
end;
theorem
:: ALGSTR_1:12
for
L
being ( ( non
empty
) ( non
empty
)
multLoopStr
) holds
(
L
: ( ( non
empty
) ( non
empty
)
multLoopStr
) is ( ( non
empty
cancelable
associative
commutative
well-unital
invertible
) ( non
empty
left_mult-cancelable
right_mult-cancelable
cancelable
unital
associative
commutative
right_unital
well-unital
left_unital
invertible
)
multGroup
) iff ( ( for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
(
1.
L
: ( ( non
empty
) ( non
empty
)
multLoopStr
)
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) & ( for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ex
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
1.
L
: ( ( non
empty
) ( non
empty
)
multLoopStr
) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr
) : ( ( ) ( non
empty
)
set
) ) ) & ( for
a
,
b
,
c
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr
) : ( ( ) ( non
empty
)
set
) )
*
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
(
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
c
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr
) : ( ( ) ( non
empty
)
set
) ) ) & ( for
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr
) : ( ( ) ( non
empty
)
set
) )
=
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr
) : ( ( ) ( non
empty
)
set
) ) ) ) ) ;
notation
let
L
be ( ( non
empty
cancelable
invertible
) ( non
empty
left_mult-cancelable
right_mult-cancelable
cancelable
invertible
)
multLoopStr
) ;
let
x
be ( ( ) (
left_mult-cancelable
right_mult-cancelable
mult-cancelable
)
Element
of ( ( ) ( non
empty
)
set
) ) ;
synonym
x
"
for
/
x
;
end;
registration
let
L
be ( ( non
empty
cancelable
invertible
) ( non
empty
left_mult-cancelable
right_mult-cancelable
cancelable
invertible
)
multLoopStr
) ;
cluster
->
left_invertible
for ( ( ) ( )
Element
of the
carrier
of
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) : ( ( ) ( )
set
) ) ;
end;
theorem
:: ALGSTR_1:13
for
G
being ( ( non
empty
cancelable
associative
well-unital
invertible
) ( non
empty
left_mult-cancelable
right_mult-cancelable
cancelable
unital
associative
right_unital
well-unital
left_unital
invertible
)
multGroup
)
for
a
being ( ( ) (
left_mult-cancelable
right_mult-cancelable
mult-cancelable
left_invertible
)
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
(
a
: ( ( ) (
left_mult-cancelable
right_mult-cancelable
mult-cancelable
left_invertible
)
Element
of ( ( ) ( non
empty
)
set
) )
"
)
: ( ( ) (
left_mult-cancelable
right_mult-cancelable
mult-cancelable
left_invertible
)
Element
of the
carrier
of
b
1
: ( ( non
empty
cancelable
associative
well-unital
invertible
) ( non
empty
left_mult-cancelable
right_mult-cancelable
cancelable
unital
associative
right_unital
well-unital
left_unital
invertible
)
multGroup
) : ( ( ) ( non
empty
)
set
) )
*
a
: ( ( ) (
left_mult-cancelable
right_mult-cancelable
mult-cancelable
left_invertible
)
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
left_mult-cancelable
right_mult-cancelable
mult-cancelable
left_invertible
)
Element
of the
carrier
of
b
1
: ( ( non
empty
cancelable
associative
well-unital
invertible
) ( non
empty
left_mult-cancelable
right_mult-cancelable
cancelable
unital
associative
right_unital
well-unital
left_unital
invertible
)
multGroup
) : ( ( ) ( non
empty
)
set
) )
=
1.
G
: ( ( non
empty
cancelable
associative
well-unital
invertible
) ( non
empty
left_mult-cancelable
right_mult-cancelable
cancelable
unital
associative
right_unital
well-unital
left_unital
invertible
)
multGroup
) : ( ( ) (
left_mult-cancelable
right_mult-cancelable
mult-cancelable
left_invertible
)
Element
of the
carrier
of
b
1
: ( ( non
empty
cancelable
associative
well-unital
invertible
) ( non
empty
left_mult-cancelable
right_mult-cancelable
cancelable
unital
associative
right_unital
well-unital
left_unital
invertible
)
multGroup
) : ( ( ) ( non
empty
)
set
) ) &
a
: ( ( ) (
left_mult-cancelable
right_mult-cancelable
mult-cancelable
left_invertible
)
Element
of ( ( ) ( non
empty
)
set
) )
*
(
a
: ( ( ) (
left_mult-cancelable
right_mult-cancelable
mult-cancelable
left_invertible
)
Element
of ( ( ) ( non
empty
)
set
) )
"
)
: ( ( ) (
left_mult-cancelable
right_mult-cancelable
mult-cancelable
left_invertible
)
Element
of the
carrier
of
b
1
: ( ( non
empty
cancelable
associative
well-unital
invertible
) ( non
empty
left_mult-cancelable
right_mult-cancelable
cancelable
unital
associative
right_unital
well-unital
left_unital
invertible
)
multGroup
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
left_mult-cancelable
right_mult-cancelable
mult-cancelable
left_invertible
)
Element
of the
carrier
of
b
1
: ( ( non
empty
cancelable
associative
well-unital
invertible
) ( non
empty
left_mult-cancelable
right_mult-cancelable
cancelable
unital
associative
right_unital
well-unital
left_unital
invertible
)
multGroup
) : ( ( ) ( non
empty
)
set
) )
=
1.
G
: ( ( non
empty
cancelable
associative
well-unital
invertible
) ( non
empty
left_mult-cancelable
right_mult-cancelable
cancelable
unital
associative
right_unital
well-unital
left_unital
invertible
)
multGroup
) : ( ( ) (
left_mult-cancelable
right_mult-cancelable
mult-cancelable
left_invertible
)
Element
of the
carrier
of
b
1
: ( ( non
empty
cancelable
associative
well-unital
invertible
) ( non
empty
left_mult-cancelable
right_mult-cancelable
cancelable
unital
associative
right_unital
well-unital
left_unital
invertible
)
multGroup
) : ( ( ) ( non
empty
)
set
) ) ) ;
definition
let
L
be ( ( non
empty
cancelable
invertible
) ( non
empty
left_mult-cancelable
right_mult-cancelable
cancelable
invertible
)
multLoopStr
) ;
let
a
,
b
be ( ( ) (
left_mult-cancelable
right_mult-cancelable
mult-cancelable
left_invertible
)
Element
of ( ( ) ( non
empty
)
set
) ) ;
func
a
/
b
->
( ( ) (
left_mult-cancelable
right_mult-cancelable
mult-cancelable
left_invertible
)
Element
of ( ( ) ( )
set
) )
equals
:: ALGSTR_1:def 7
a
: ( ( ) ( )
VectSpStr
over
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) )
*
(
b
: ( (
V6
()
V18
(
K20
(
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) ,
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) ) : ( ( ) ( )
set
) ,
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) ) ) (
V6
()
V18
(
K20
(
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) ,
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) ) : ( ( ) ( )
set
) ,
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) ) )
Element
of
K19
(
K20
(
K20
(
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) ,
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) ) : ( ( ) ( )
set
) ,
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
"
)
: ( ( ) ( )
Element
of the
carrier
of
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of the
carrier
of
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) : ( ( ) ( )
set
) ) ;
end;
definition
func
multEX_0
->
( (
strict
) (
strict
)
multLoopStr_0
)
equals
:: ALGSTR_1:def 8
multLoopStr_0
(#
REAL
: ( ( ) ( non
empty
V35
() )
set
) ,
multreal
: ( (
V6
()
V18
(
K20
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ,
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ,
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) ) (
V6
()
V18
(
K20
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ,
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ,
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) )
Element
of
K19
(
K20
(
K20
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ,
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ,
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) ,
0
: ( ( ) (
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) ) ,1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) ) #) : ( (
strict
) ( non
empty
strict
)
multLoopStr_0
) ;
end;
registration
cluster
multEX_0
: ( (
strict
) (
strict
)
multLoopStr_0
)
->
non
empty
strict
;
end;
registration
cluster
multEX_0
: ( (
strict
) ( non
empty
strict
)
multLoopStr_0
)
->
strict
well-unital
;
end;
theorem
:: ALGSTR_1:14
for
q
,
p
being ( ( ) (
V24
()
V32
()
V125
() )
Real
) st
q
: ( ( ) (
V24
()
V32
()
V125
() )
Real
)
<>
0
: ( ( ) (
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) ) holds
ex
y
being ( ( ) (
V24
()
V32
()
V125
() )
Real
) st
p
: ( ( ) (
V24
()
V32
()
V125
() )
Real
)
=
q
: ( ( ) (
V24
()
V32
()
V125
() )
Real
)
*
y
: ( ( ) (
V24
()
V32
()
V125
() )
Real
) : ( ( ) (
V24
()
V32
()
V125
() )
Element
of
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) ;
theorem
:: ALGSTR_1:15
for
q
,
p
being ( ( ) (
V24
()
V32
()
V125
() )
Real
) st
q
: ( ( ) (
V24
()
V32
()
V125
() )
Real
)
<>
0
: ( ( ) (
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) ) holds
ex
y
being ( ( ) (
V24
()
V32
()
V125
() )
Real
) st
p
: ( ( ) (
V24
()
V32
()
V125
() )
Real
)
=
y
: ( ( ) (
V24
()
V32
()
V125
() )
Real
)
*
q
: ( ( ) (
V24
()
V32
()
V125
() )
Real
) : ( ( ) (
V24
()
V32
()
V125
() )
Element
of
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) ;
definition
let
IT
be ( ( non
empty
) ( non
empty
)
multLoopStr_0
) ;
attr
IT
is
almost_invertible
means
:: ALGSTR_1:def 9
( ( for
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( )
set
) ) st
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<>
0.
IT
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) : ( ( ) ( )
Element
of the
carrier
of
IT
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) : ( ( ) ( )
set
) ) holds
ex
x
being ( ( ) ( )
Element
of ( ( ) ( )
set
) ) st
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
IT
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) : ( ( ) ( )
set
) )
=
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) & ( for
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( )
set
) ) st
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<>
0.
IT
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) : ( ( ) ( )
Element
of the
carrier
of
IT
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) : ( ( ) ( )
set
) ) holds
ex
x
being ( ( ) ( )
Element
of ( ( ) ( )
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
IT
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) : ( ( ) ( )
set
) )
=
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) );
end;
definition
let
IT
be ( ( non
empty
) ( non
empty
)
multLoopStr_0
) ;
attr
IT
is
multLoop_0-like
means
:: ALGSTR_1:def 10
(
IT
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) is
almost_invertible
&
IT
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) is
almost_cancelable
& ( for
a
being ( ( ) ( )
Element
of ( ( ) ( )
set
) ) holds
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
(
0.
IT
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
)
)
: ( ( ) ( )
Element
of the
carrier
of
IT
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of the
carrier
of
IT
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) : ( ( ) ( )
set
) )
=
0.
IT
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) : ( ( ) ( )
Element
of the
carrier
of
IT
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) : ( ( ) ( )
set
) ) ) & ( for
a
being ( ( ) ( )
Element
of ( ( ) ( )
set
) ) holds
(
0.
IT
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
)
)
: ( ( ) ( )
Element
of the
carrier
of
IT
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) : ( ( ) ( )
set
) )
*
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
IT
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) : ( ( ) ( )
set
) )
=
0.
IT
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) : ( ( ) ( )
Element
of the
carrier
of
IT
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) : ( ( ) ( )
set
) ) ) );
end;
theorem
:: ALGSTR_1:16
for
L
being ( ( non
empty
) ( non
empty
)
multLoopStr_0
) holds
(
L
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) is
multLoop_0-like
iff ( ( for
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<>
0.
L
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) : ( ( ) (
V51
(
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) : ( ( ) ( non
empty
)
set
) ) holds
ex
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) : ( ( ) ( non
empty
)
set
) )
=
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) & ( for
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<>
0.
L
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) : ( ( ) (
V51
(
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) : ( ( ) ( non
empty
)
set
) ) holds
ex
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) : ( ( ) ( non
empty
)
set
) )
=
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) & ( for
a
,
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<>
0.
L
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) : ( ( ) (
V51
(
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) : ( ( ) ( non
empty
)
set
) ) &
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) : ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) : ( ( ) ( non
empty
)
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) & ( for
a
,
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<>
0.
L
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) : ( ( ) (
V51
(
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) : ( ( ) ( non
empty
)
set
) ) &
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) : ( ( ) ( non
empty
)
set
) )
=
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) : ( ( ) ( non
empty
)
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) & ( for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
(
0.
L
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
)
)
: ( ( ) (
V51
(
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) : ( ( ) ( non
empty
)
set
) )
=
0.
L
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) : ( ( ) (
V51
(
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) : ( ( ) ( non
empty
)
set
) ) ) & ( for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
0.
L
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
)
)
: ( ( ) (
V51
(
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) : ( ( ) ( non
empty
)
set
) )
*
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) : ( ( ) ( non
empty
)
set
) )
=
0.
L
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) : ( ( ) (
V51
(
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multLoopStr_0
) : ( ( ) ( non
empty
)
set
) ) ) ) ) ;
registration
cluster
non
empty
multLoop_0-like
->
non
empty
almost_cancelable
almost_invertible
for ( ( ) ( )
multLoopStr_0
) ;
end;
registration
cluster
non
empty
non
degenerated
strict
well-unital
multLoop_0-like
for ( ( ) ( )
multLoopStr_0
) ;
end;
definition
mode
multLoop_0
is
( ( non
empty
non
degenerated
well-unital
multLoop_0-like
) ( non
empty
non
degenerated
non
trivial
almost_left_cancelable
almost_right_cancelable
almost_cancelable
unital
right_unital
well-unital
left_unital
almost_invertible
multLoop_0-like
)
multLoopStr_0
) ;
end;
registration
cluster
multEX_0
: ( (
strict
) ( non
empty
strict
unital
right_unital
well-unital
left_unital
)
multLoopStr_0
)
->
strict
well-unital
multLoop_0-like
;
end;
registration
cluster
non
empty
non
degenerated
non
trivial
strict
almost_left_cancelable
almost_right_cancelable
almost_cancelable
unital
associative
right_unital
well-unital
left_unital
almost_invertible
multLoop_0-like
for ( ( ) ( )
multLoopStr_0
) ;
end;
definition
mode
multGroup_0
is
( ( non
empty
non
degenerated
associative
well-unital
multLoop_0-like
) ( non
empty
non
degenerated
non
trivial
almost_left_cancelable
almost_right_cancelable
almost_cancelable
unital
associative
right_unital
well-unital
left_unital
almost_invertible
multLoop_0-like
)
multLoop_0
) ;
end;
registration
cluster
multEX_0
: ( (
strict
) ( non
empty
strict
almost_left_cancelable
almost_right_cancelable
almost_cancelable
unital
right_unital
well-unital
left_unital
almost_invertible
multLoop_0-like
)
multLoopStr_0
)
->
strict
associative
;
end;
registration
cluster
non
empty
non
degenerated
non
trivial
strict
almost_left_cancelable
almost_right_cancelable
almost_cancelable
unital
associative
commutative
right_unital
well-unital
left_unital
almost_invertible
multLoop_0-like
for ( ( ) ( )
multLoopStr_0
) ;
end;
definition
let
L
be ( ( non
empty
almost_cancelable
almost_invertible
) ( non
empty
almost_left_cancelable
almost_right_cancelable
almost_cancelable
almost_invertible
)
multLoopStr_0
) ;
let
x
be ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
assume
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<>
0.
L
: ( ( non
empty
almost_cancelable
almost_invertible
) ( non
empty
almost_left_cancelable
almost_right_cancelable
almost_cancelable
almost_invertible
)
multLoopStr_0
) : ( ( ) (
V51
(
L
: ( ( non
empty
almost_cancelable
almost_invertible
) ( non
empty
almost_left_cancelable
almost_right_cancelable
almost_cancelable
almost_invertible
)
multLoopStr_0
) ) )
Element
of the
carrier
of
L
: ( ( non
empty
almost_cancelable
almost_invertible
) ( non
empty
almost_left_cancelable
almost_right_cancelable
almost_cancelable
almost_invertible
)
multLoopStr_0
) : ( ( ) ( non
empty
)
set
) ) ;
redefine
func
x
"
means
:: ALGSTR_1:def 11
it
: ( (
V6
()
V18
(
K20
(
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) ,
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) ) : ( ( ) ( )
set
) ,
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) ) ) (
V6
()
V18
(
K20
(
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) ,
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) ) : ( ( ) ( )
set
) ,
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) ) )
Element
of
K19
(
K20
(
K20
(
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) ,
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) ) : ( ( ) ( )
set
) ,
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
*
x
: ( ( ) ( )
VectSpStr
over
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) ) : ( ( ) ( )
Element
of the
carrier
of
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) : ( ( ) ( )
set
) )
=
1.
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) : ( ( ) ( )
Element
of the
carrier
of
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) : ( ( ) ( )
set
) ) ;
end;
theorem
:: ALGSTR_1:17
for
G
being ( ( non
empty
almost_cancelable
associative
well-unital
almost_invertible
) ( non
empty
almost_left_cancelable
almost_right_cancelable
almost_cancelable
unital
associative
right_unital
well-unital
left_unital
almost_invertible
)
multLoopStr_0
)
for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<>
0.
G
: ( ( non
empty
almost_cancelable
associative
well-unital
almost_invertible
) ( non
empty
almost_left_cancelable
almost_right_cancelable
almost_cancelable
unital
associative
right_unital
well-unital
left_unital
almost_invertible
)
multLoopStr_0
) : ( ( ) (
V51
(
b
1
: ( ( non
empty
almost_cancelable
associative
well-unital
almost_invertible
) ( non
empty
almost_left_cancelable
almost_right_cancelable
almost_cancelable
unital
associative
right_unital
well-unital
left_unital
almost_invertible
)
multLoopStr_0
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
almost_cancelable
associative
well-unital
almost_invertible
) ( non
empty
almost_left_cancelable
almost_right_cancelable
almost_cancelable
unital
associative
right_unital
well-unital
left_unital
almost_invertible
)
multLoopStr_0
) : ( ( ) ( non
empty
)
set
) ) holds
(
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
almost_cancelable
associative
well-unital
almost_invertible
) ( non
empty
almost_left_cancelable
almost_right_cancelable
almost_cancelable
unital
associative
right_unital
well-unital
left_unital
almost_invertible
)
multLoopStr_0
) : ( ( ) ( non
empty
)
set
) )
*
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
almost_cancelable
associative
well-unital
almost_invertible
) ( non
empty
almost_left_cancelable
almost_right_cancelable
almost_cancelable
unital
associative
right_unital
well-unital
left_unital
almost_invertible
)
multLoopStr_0
) : ( ( ) ( non
empty
)
set
) )
=
1.
G
: ( ( non
empty
almost_cancelable
associative
well-unital
almost_invertible
) ( non
empty
almost_left_cancelable
almost_right_cancelable
almost_cancelable
unital
associative
right_unital
well-unital
left_unital
almost_invertible
)
multLoopStr_0
) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
almost_cancelable
associative
well-unital
almost_invertible
) ( non
empty
almost_left_cancelable
almost_right_cancelable
almost_cancelable
unital
associative
right_unital
well-unital
left_unital
almost_invertible
)
multLoopStr_0
) : ( ( ) ( non
empty
)
set
) ) &
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
almost_cancelable
associative
well-unital
almost_invertible
) ( non
empty
almost_left_cancelable
almost_right_cancelable
almost_cancelable
unital
associative
right_unital
well-unital
left_unital
almost_invertible
)
multLoopStr_0
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
almost_cancelable
associative
well-unital
almost_invertible
) ( non
empty
almost_left_cancelable
almost_right_cancelable
almost_cancelable
unital
associative
right_unital
well-unital
left_unital
almost_invertible
)
multLoopStr_0
) : ( ( ) ( non
empty
)
set
) )
=
1.
G
: ( ( non
empty
almost_cancelable
associative
well-unital
almost_invertible
) ( non
empty
almost_left_cancelable
almost_right_cancelable
almost_cancelable
unital
associative
right_unital
well-unital
left_unital
almost_invertible
)
multLoopStr_0
) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
almost_cancelable
associative
well-unital
almost_invertible
) ( non
empty
almost_left_cancelable
almost_right_cancelable
almost_cancelable
unital
associative
right_unital
well-unital
left_unital
almost_invertible
)
multLoopStr_0
) : ( ( ) ( non
empty
)
set
) ) ) ;
definition
let
L
be ( ( non
empty
almost_cancelable
almost_invertible
) ( non
empty
almost_left_cancelable
almost_right_cancelable
almost_cancelable
almost_invertible
)
multLoopStr_0
) ;
let
a
,
b
be ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
func
a
/
b
->
( ( ) ( )
Element
of ( ( ) ( )
set
) )
equals
:: ALGSTR_1:def 12
a
: ( ( ) ( )
VectSpStr
over
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) )
*
(
b
: ( (
V6
()
V18
(
K20
(
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) ,
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) ) : ( ( ) ( )
set
) ,
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) ) ) (
V6
()
V18
(
K20
(
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) ,
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) ) : ( ( ) ( )
set
) ,
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) ) )
Element
of
K19
(
K20
(
K20
(
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) ,
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) ) : ( ( ) ( )
set
) ,
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
"
)
: ( ( ) ( )
Element
of the
carrier
of
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of the
carrier
of
L
: ( (
V40
() ) (
V25
()
V26
()
V27
()
V40
() )
set
) : ( ( ) ( )
set
) ) ;
end;
registration
cluster
1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) )
-element
->
1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) )
-element
right_complementable
Abelian
add-associative
right_zeroed
for ( ( ) ( )
addLoopStr
) ;
cluster
non
empty
trivial
->
non
empty
right-distributive
well-unital
for ( ( ) ( )
doubleLoopStr
) ;
end;
registration
cluster
1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) )
-element
->
1 : ( ( ) ( non
empty
V24
()
V25
()
V26
()
V27
()
V31
()
V32
()
V35
()
V40
()
V125
()
V127
() )
Element
of
NAT
: ( ( ) ( non
empty
V25
()
V26
()
V27
()
V35
()
V40
()
V41
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V35
() )
set
) ) : ( ( ) (
V35
() )
set
) ) )
-element
Group-like
associative
commutative
for ( ( ) ( )
multMagma
) ;
end;