begin
definition
let I be ( ( non
empty ) ( non
empty )
set ) ;
let F be ( (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
I : ( ( non
empty ) ( non
empty )
set ) ) ;
let i be ( ( ) ( )
Element of
I : ( ( non
empty ) ( non
empty )
set ) ) ;
func 1ProdHom (
F,
i)
-> ( (
Function-like quasi_total V99(
F : ( ( ) ( )
set )
. i : ( ( ) ( )
Element of
I : ( ( ) ( )
set ) ) : ( ( non
empty ) ( non
empty )
multMagma ) ,
ProjGroup (
F : ( ( ) ( )
set ) ,
i : ( ( ) ( )
Element of
I : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V153()
V154()
V155()
V156()
V157()
V158() )
Subgroup of
product F : ( ( ) ( )
set ) : ( (
strict ) (
strict )
multMagma ) ) ) ) (
Relation-like the
carrier of
(F : ( ( ) ( ) set ) . i : ( ( ) ( ) Element of I : ( ( ) ( ) set ) ) ) : ( ( non
empty ) ( non
empty )
multMagma ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
(ProjGroup (F : ( ( ) ( ) set ) ,i : ( ( ) ( ) Element of I : ( ( ) ( ) set ) ) )) : ( (
strict ) ( non
empty strict unital Group-like associative V153()
V154()
V155()
V156()
V157()
V158() )
Subgroup of
product F : ( ( ) ( )
set ) : ( (
strict ) (
strict )
multMagma ) ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total V99(
F : ( ( ) ( )
set )
. i : ( ( ) ( )
Element of
I : ( ( ) ( )
set ) ) : ( ( non
empty ) ( non
empty )
multMagma ) ,
ProjGroup (
F : ( ( ) ( )
set ) ,
i : ( ( ) ( )
Element of
I : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V153()
V154()
V155()
V156()
V157()
V158() )
Subgroup of
product F : ( ( ) ( )
set ) : ( (
strict ) (
strict )
multMagma ) ) ) )
Homomorphism of
F : ( ( ) ( )
set )
. i : ( ( ) ( )
Element of
I : ( ( ) ( )
set ) ) : ( ( non
empty ) ( non
empty )
multMagma ) ,
ProjGroup (
F : ( ( ) ( )
set ) ,
i : ( ( ) ( )
Element of
I : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V153()
V154()
V155()
V156()
V157()
V158() )
Subgroup of
product F : ( ( ) ( )
set ) : ( (
strict ) (
strict )
multMagma ) ) )
means
for
x being ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) holds
it : ( ( ) ( )
Element of
I : ( ( ) ( )
set ) )
. x : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
(ProjGroup (F : ( ( ) ( ) set ) ,i : ( ( ) ( ) Element of I : ( ( ) ( ) set ) ) )) : ( (
strict ) ( non
empty strict unital Group-like associative V153()
V154()
V155()
V156()
V157()
V158() )
Subgroup of
product F : ( ( ) ( )
set ) : ( (
strict ) (
strict )
multMagma ) ) : ( ( ) ( non
empty )
set ) )
= (1_ (product F : ( ( ) ( ) set ) ) : ( ( strict ) ( strict ) multMagma ) ) : ( ( ) ( )
Element of the
carrier of
(product F : ( ( ) ( ) set ) ) : ( (
strict ) (
strict )
multMagma ) : ( ( ) ( )
set ) )
+* (
i : ( ( ) ( )
Element of
I : ( ( ) ( )
set ) ) ,
x : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) ) : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) ;
end;
registration
let I be ( ( non
empty ) ( non
empty )
set ) ;
let F be ( (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
I : ( ( non
empty ) ( non
empty )
set ) ) ;
let i be ( ( ) ( )
Element of
I : ( ( non
empty ) ( non
empty )
set ) ) ;
cluster 1ProdHom (
F : ( (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
set ) ,
i : ( ( ) ( )
Element of
I : ( ( non
empty ) ( non
empty )
set ) ) ) : ( (
Function-like quasi_total V99(
F : ( (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
set )
. i : ( ( ) ( )
Element of
I : ( ( non
empty ) ( non
empty )
set ) ) : ( ( non
empty ) ( non
empty unital Group-like associative V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
ProjGroup (
F : ( (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
set ) ,
i : ( ( ) ( )
Element of
I : ( ( non
empty ) ( non
empty )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V153()
V154()
V155()
V156()
V157()
V158() )
Subgroup of
product F : ( (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
set ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ) ) ) (
Relation-like the
carrier of
(F : ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like total V178() multMagma-yielding Group-like associative ) set ) . i : ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non
empty ) ( non
empty unital Group-like associative V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
(ProjGroup (F : ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like total V178() multMagma-yielding Group-like associative ) set ) ,i : ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) )) : ( (
strict ) ( non
empty strict unital Group-like associative V153()
V154()
V155()
V156()
V157()
V158() )
Subgroup of
product F : ( (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
set ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total V99(
F : ( (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
set )
. i : ( ( ) ( )
Element of
I : ( ( non
empty ) ( non
empty )
set ) ) : ( ( non
empty ) ( non
empty unital Group-like associative V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
ProjGroup (
F : ( (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
set ) ,
i : ( ( ) ( )
Element of
I : ( ( non
empty ) ( non
empty )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V153()
V154()
V155()
V156()
V157()
V158() )
Subgroup of
product F : ( (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
set ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ) ) )
Homomorphism of
F : ( (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
set )
. i : ( ( ) ( )
Element of
I : ( ( non
empty ) ( non
empty )
set ) ) : ( ( non
empty ) ( non
empty unital Group-like associative V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
ProjGroup (
F : ( (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
set ) ,
i : ( ( ) ( )
Element of
I : ( ( non
empty ) ( non
empty )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V153()
V154()
V155()
V156()
V157()
V158() )
Subgroup of
product F : ( (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
set ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ) )
-> Function-like quasi_total bijective V99(
F : ( (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
set )
. i : ( ( ) ( )
Element of
I : ( ( non
empty ) ( non
empty )
set ) ) : ( ( non
empty ) ( non
empty unital Group-like associative V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
ProjGroup (
F : ( (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
set ) ,
i : ( ( ) ( )
Element of
I : ( ( non
empty ) ( non
empty )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V153()
V154()
V155()
V156()
V157()
V158() )
Subgroup of
product F : ( (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
set ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ) ) ;
end;
theorem
for
n being ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat)
for
G being ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group)
for
F being ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg n : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) st ( for
i being ( ( ) ( )
Element of
Seg n : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) holds
F : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) )
. i : ( (
Function-like quasi_total V99(
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) ) ) (
Relation-like the
carrier of
(product b3 : ( ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total V178() multMagma-yielding Group-like associative ) multMagma-Family of Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total V99(
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) ) )
Homomorphism of
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) ) : ( ( non
empty ) ( non
empty )
multMagma ) is ( ( ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Subgroup of
G : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) ) ) & ( for
x being ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) ex
s being ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like V33()
FinSequence-like FinSubsequence-like countable )
FinSequence of ( ( ) ( non
empty )
set ) ) st
(
len s : ( ( ) (
Relation-like Function-like )
Element of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real non
negative countable )
Element of
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) )
= n : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) & ( for
k being ( ( ) ( )
Element of
Seg n : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) holds
s : ( ( ) (
Relation-like Function-like )
Element of ( ( ) ( non
empty )
set ) )
. k : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like V33()
FinSequence-like FinSubsequence-like countable )
FinSequence of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set )
in F : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) )
. k : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like V33()
FinSequence-like FinSubsequence-like countable )
FinSequence of ( ( ) ( non
empty )
set ) ) : ( ( non
empty ) ( non
empty )
multMagma ) ) &
x : ( (
Function-like quasi_total V99(
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) ) ) (
Relation-like the
carrier of
(product b3 : ( ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total V178() multMagma-yielding Group-like associative ) multMagma-Family of Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total V99(
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) ) )
Homomorphism of
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) )
= Product s : ( ( ) (
Relation-like Function-like )
Element of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) : ( ( ) ( non
empty )
set ) ) ) ) & ( for
s,
t being ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like V33()
FinSequence-like FinSubsequence-like countable )
FinSequence of ( ( ) ( non
empty )
set ) ) st
len s : ( (
Function-like quasi_total V99(
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) ) ) (
Relation-like the
carrier of
(product b3 : ( ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total V178() multMagma-yielding Group-like associative ) multMagma-Family of Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total V99(
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) ) )
Homomorphism of
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) ) : ( ( ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Element of
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) )
= n : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) & ( for
k being ( ( ) ( )
Element of
Seg n : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) holds
s : ( (
Function-like quasi_total V99(
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) ) ) (
Relation-like the
carrier of
(product b3 : ( ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total V178() multMagma-yielding Group-like associative ) multMagma-Family of Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total V99(
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) ) )
Homomorphism of
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) )
. k : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like V33()
FinSequence-like FinSubsequence-like countable )
FinSequence of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set )
in F : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) )
. k : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like V33()
FinSequence-like FinSubsequence-like countable )
FinSequence of ( ( ) ( non
empty )
set ) ) : ( ( non
empty ) ( non
empty )
multMagma ) ) &
len t : ( ( ) (
Relation-like Function-like )
Element of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real non
negative countable )
Element of
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) )
= n : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) & ( for
k being ( ( ) ( )
Element of
Seg n : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) holds
t : ( ( ) (
Relation-like Function-like )
Element of ( ( ) ( non
empty )
set ) )
. k : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like V33()
FinSequence-like FinSubsequence-like countable )
FinSequence of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set )
in F : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) )
. k : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like V33()
FinSequence-like FinSubsequence-like countable )
FinSequence of ( ( ) ( non
empty )
set ) ) : ( ( non
empty ) ( non
empty )
multMagma ) ) &
Product s : ( (
Function-like quasi_total V99(
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) ) ) (
Relation-like the
carrier of
(product b3 : ( ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total V178() multMagma-yielding Group-like associative ) multMagma-Family of Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total V99(
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) ) )
Homomorphism of
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) ) : ( ( ) ( )
Element of the
carrier of
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) : ( ( ) ( non
empty )
set ) )
= Product t : ( ( ) (
Relation-like Function-like )
Element of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) : ( ( ) ( non
empty )
set ) ) holds
s : ( (
Function-like quasi_total V99(
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) ) ) (
Relation-like the
carrier of
(product b3 : ( ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total V178() multMagma-yielding Group-like associative ) multMagma-Family of Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total V99(
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) ) )
Homomorphism of
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) )
= t : ( ( ) (
Relation-like Function-like )
Element of ( ( ) ( non
empty )
set ) ) ) holds
ex
f being ( (
Function-like quasi_total V99(
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) ) ) (
Relation-like the
carrier of
(product b3 : ( ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total V178() multMagma-yielding Group-like associative ) multMagma-Family of Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total V99(
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) ) )
Homomorphism of
product F : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
G : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) ) st
(
f : ( (
Function-like quasi_total V99(
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) ) ) (
Relation-like the
carrier of
(product b3 : ( ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total V178() multMagma-yielding Group-like associative ) multMagma-Family of Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total V99(
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) ) )
Homomorphism of
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) ) is
bijective & ( for
x being ( ( ) (
Relation-like Function-like )
Element of ( ( ) ( non
empty )
set ) ) ex
s being ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like V33()
FinSequence-like FinSubsequence-like countable )
FinSequence of ( ( ) ( non
empty )
set ) ) st
(
len s : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like V33()
FinSequence-like FinSubsequence-like countable )
FinSequence of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real non
negative countable )
Element of
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) )
= n : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) & ( for
k being ( ( ) ( )
Element of
Seg n : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) holds
s : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like V33()
FinSequence-like FinSubsequence-like countable )
FinSequence of ( ( ) ( non
empty )
set ) )
. k : ( ( ) ( )
Element of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( ( ) ( )
set )
in F : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) )
. k : ( ( ) ( )
Element of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( ( non
empty ) ( non
empty unital Group-like associative V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ) &
s : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like V33()
FinSequence-like FinSubsequence-like countable )
FinSequence of ( ( ) ( non
empty )
set ) )
= x : ( ( ) (
Relation-like Function-like )
Element of ( ( ) ( non
empty )
set ) ) &
f : ( (
Function-like quasi_total V99(
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) ) ) (
Relation-like the
carrier of
(product b3 : ( ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total V178() multMagma-yielding Group-like associative ) multMagma-Family of Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total V99(
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) ) )
Homomorphism of
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) )
. x : ( ( ) (
Relation-like Function-like )
Element of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) : ( ( ) ( non
empty )
set ) )
= Product s : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like V33()
FinSequence-like FinSubsequence-like countable )
FinSequence of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
b2 : ( ( non
empty Group-like associative commutative ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
Group) : ( ( ) ( non
empty )
set ) ) ) ) ) ;
theorem
for
n being ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat)
for
G,
F being ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg n : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) st ( for
k being ( ( ) ( )
Element of
Seg n : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) holds
F : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) )
. k : ( (
Function-like quasi_total V99(
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
product b2 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ) ) (
Relation-like the
carrier of
(product b3 : ( ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total multMagma-yielding Group-like associative commutative ) ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total V178() multMagma-yielding Group-like associative commutative ) multMagma-Family of Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
(product b2 : ( ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total multMagma-yielding Group-like associative commutative ) ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total V178() multMagma-yielding Group-like associative commutative ) multMagma-Family of Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total V99(
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
product b2 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ) )
Homomorphism of
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
product b2 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ) : ( ( non
empty ) ( non
empty )
multMagma )
= ProjGroup (
G : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) ,
k : ( (
Function-like quasi_total V99(
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
product b2 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ) ) (
Relation-like the
carrier of
(product b3 : ( ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total multMagma-yielding Group-like associative commutative ) ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total V178() multMagma-yielding Group-like associative commutative ) multMagma-Family of Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
(product b2 : ( ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total multMagma-yielding Group-like associative commutative ) ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total V178() multMagma-yielding Group-like associative commutative ) multMagma-Family of Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total V99(
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
product b2 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ) )
Homomorphism of
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
product b2 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative V153()
V154()
V155()
V156()
V157()
V158() )
Subgroup of
product b2 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ) ) holds
ex
f being ( (
Function-like quasi_total V99(
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
product b2 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ) ) (
Relation-like the
carrier of
(product b3 : ( ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total multMagma-yielding Group-like associative commutative ) ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total V178() multMagma-yielding Group-like associative commutative ) multMagma-Family of Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
(product b2 : ( ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total multMagma-yielding Group-like associative commutative ) ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total V178() multMagma-yielding Group-like associative commutative ) multMagma-Family of Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total V99(
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
product b2 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ) )
Homomorphism of
product F : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
product G : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ) st
(
f : ( (
Function-like quasi_total V99(
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
product b2 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ) ) (
Relation-like the
carrier of
(product b3 : ( ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total multMagma-yielding Group-like associative commutative ) ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total V178() multMagma-yielding Group-like associative commutative ) multMagma-Family of Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
(product b2 : ( ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total multMagma-yielding Group-like associative commutative ) ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total V178() multMagma-yielding Group-like associative commutative ) multMagma-Family of Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total V99(
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
product b2 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ) )
Homomorphism of
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
product b2 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ) is
bijective & ( for
x being ( ( ) (
Relation-like Function-like )
Element of ( ( ) ( non
empty )
set ) ) ex
s being ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(product b2 : ( ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total multMagma-yielding Group-like associative commutative ) ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total V178() multMagma-yielding Group-like associative commutative ) multMagma-Family of Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) : ( ( ) ( non
empty )
set )
-valued Function-like V33()
FinSequence-like FinSubsequence-like countable )
FinSequence of ( ( ) ( non
empty )
set ) ) st
(
len s : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(product b2 : ( ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total multMagma-yielding Group-like associative commutative ) ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total V178() multMagma-yielding Group-like associative commutative ) multMagma-Family of Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) : ( ( ) ( non
empty )
set )
-valued Function-like V33()
FinSequence-like FinSubsequence-like countable )
FinSequence of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real non
negative countable )
Element of
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) )
= n : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) & ( for
k being ( ( ) ( )
Element of
Seg n : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) holds
s : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(product b2 : ( ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total multMagma-yielding Group-like associative commutative ) ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total V178() multMagma-yielding Group-like associative commutative ) multMagma-Family of Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) : ( ( ) ( non
empty )
set )
-valued Function-like V33()
FinSequence-like FinSubsequence-like countable )
FinSequence of ( ( ) ( non
empty )
set ) )
. k : ( ( ) ( )
Element of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( ( ) ( )
set )
in F : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) )
. k : ( ( ) ( )
Element of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( ( non
empty ) ( non
empty unital Group-like associative commutative V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ) &
s : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(product b2 : ( ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total multMagma-yielding Group-like associative commutative ) ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total V178() multMagma-yielding Group-like associative commutative ) multMagma-Family of Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) : ( ( ) ( non
empty )
set )
-valued Function-like V33()
FinSequence-like FinSubsequence-like countable )
FinSequence of ( ( ) ( non
empty )
set ) )
= x : ( ( ) (
Relation-like Function-like )
Element of ( ( ) ( non
empty )
set ) ) &
f : ( (
Function-like quasi_total V99(
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
product b2 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ) ) (
Relation-like the
carrier of
(product b3 : ( ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total multMagma-yielding Group-like associative commutative ) ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total V178() multMagma-yielding Group-like associative commutative ) multMagma-Family of Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
(product b2 : ( ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total multMagma-yielding Group-like associative commutative ) ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total V178() multMagma-yielding Group-like associative commutative ) multMagma-Family of Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total V99(
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
product b2 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ) )
Homomorphism of
product b3 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) ,
product b2 : ( (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total multMagma-yielding Group-like associative commutative ) (
Relation-like Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) )
-defined Function-like total V178()
multMagma-yielding Group-like associative commutative )
multMagma-Family of
Seg b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) : ( ( ) ( non
empty V33()
V40(
b1 : ( ( non
empty V30() ) ( non
empty V24()
V25()
V26()
V30()
V31()
V33()
V38()
V100()
ext-real positive non
negative countable )
Nat) )
countable )
Element of
K19(
NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V33() )
set ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) )
. x : ( ( ) (
Relation-like Function-like )
Element of ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like Function-like )
Element of the
carrier of
(product b2 : ( ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total multMagma-yielding Group-like associative commutative ) ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total V178() multMagma-yielding Group-like associative commutative ) multMagma-Family of Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) : ( ( ) ( non
empty )
set ) )
= Product s : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V24()
V25()
V26()
V33()
V38()
V39()
countable denumerable )
Element of
K19(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(product b2 : ( ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total multMagma-yielding Group-like associative commutative ) ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total V178() multMagma-yielding Group-like associative commutative ) multMagma-Family of Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) : ( ( ) ( non
empty )
set )
-valued Function-like V33()
FinSequence-like FinSubsequence-like countable )
FinSequence of ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like Function-like )
Element of the
carrier of
(product b2 : ( ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total multMagma-yielding Group-like associative commutative ) ( Relation-like Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) -defined Function-like total V178() multMagma-yielding Group-like associative commutative ) multMagma-Family of Seg b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) : ( ( ) ( non empty V33() V40(b1 : ( ( non empty V30() ) ( non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable ) Nat) ) countable ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() countable denumerable ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() ) set ) ) ) ) : ( (
strict ) ( non
empty strict unital Group-like associative commutative V143()
V153()
V154()
V155()
V156()
V157()
V158() )
multMagma ) : ( ( ) ( non
empty )
set ) ) ) ) ) ;