REAL is non empty non trivial non finite complex-membered ext-real-membered real-membered V207() V210() V211() V213() set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V207() V208() V210() Element of bool REAL
bool REAL is non empty non trivial non finite set
COMPLEX is non empty non trivial non finite complex-membered V207() set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V207() V208() V210() set
bool omega is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
RAT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered V207() set
INT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered integer-membered V207() set
[:COMPLEX,COMPLEX:] is Relation-like non empty non trivial non finite V191() set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like non empty non trivial non finite V191() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set
[:REAL,REAL:] is Relation-like non empty non trivial non finite V191() V192() V193() set
bool [:REAL,REAL:] is non empty non trivial non finite set
[:[:REAL,REAL:],REAL:] is Relation-like non empty non trivial non finite V191() V192() V193() set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set
[:RAT,RAT:] is Relation-like RAT -valued non empty non trivial non finite V191() V192() V193() set
bool [:RAT,RAT:] is non empty non trivial non finite set
[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued non empty non trivial non finite V191() V192() V193() set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set
[:INT,INT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V191() V192() V193() set
bool [:INT,INT:] is non empty non trivial non finite set
[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V191() V192() V193() set
bool [:[:INT,INT:],INT:] is non empty non trivial non finite set
[:NAT,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V191() V192() V193() V194() set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V191() V192() V193() V194() set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set
K284() is set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT
2 is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT
[:2,2:] is Relation-like RAT -valued INT -valued non empty finite V191() V192() V193() V194() set
[:[:2,2:],2:] is Relation-like RAT -valued INT -valued non empty finite V191() V192() V193() V194() set
bool [:[:2,2:],2:] is non empty finite V39() set
{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() V32() integer finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V191() V192() V193() V194() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V207() V210() V211() V212() V213() set
3 is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT
Seg 1 is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{1} is non empty trivial finite V39() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() set
Seg 2 is non empty finite 2 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
{1,2} is non empty finite V39() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() set
0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() V32() integer finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V46() ext-real non positive non negative V191() V192() V193() V194() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V207() V210() V211() V212() V213() Element of NAT
idseq 2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*1,2*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set
<*1*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
[1,1] is set
{1,1} is non empty finite V39() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() set
{{1,1},{1}} is non empty finite V39() set
{[1,1]} is Relation-like Function-like constant non empty trivial finite 1 -element set
<*2*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
[1,2] is set
{{1,2},{1}} is non empty finite V39() set
{[1,2]} is Relation-like Function-like constant non empty trivial finite 1 -element set
<*1*> ^ <*2*> is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT
Sgm {} is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V191() V192() V193() V194() FinSequence of NAT
len {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() V32() integer finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V191() V192() V193() V194() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V207() V210() V211() V212() V213() set
Permutations 2 is non empty permutational set
<*2,1*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set
<*2*> ^ <*1*> is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like set
{<*1,2*>,<*2,1*>} is functional non empty finite V39() set
<*> INT is Relation-like non-empty empty-yielding NAT -defined INT -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() V32() integer finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V191() V192() V193() V194() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V207() V210() V211() V212() V213() FinSequence of INT
[:NAT,INT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V191() V192() V193() set
O is set
G is set
Funcs (G,G) is functional non empty set
[:O,(Funcs (G,G)):] is Relation-like set
bool [:O,(Funcs (G,G)):] is non empty set
O is set
G is set
Funcs (G,G) is functional non empty set
[:O,(Funcs (G,G)):] is Relation-like set
bool [:O,(Funcs (G,G)):] is non empty set
[#] G is non proper Element of bool G
bool G is non empty set
s1 is Relation-like O -defined Funcs (G,G) -valued Function-like total quasi_total Element of bool [:O,(Funcs (G,G)):]
[:G,G:] is Relation-like set
bool [:G,G:] is non empty set
s2 is Element of O
s19 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]
s1 . s2 is Relation-like Function-like set
s19 .: ([#] G) is Element of bool G
O is set
G is set
Funcs (G,G) is functional non empty set
[:O,(Funcs (G,G)):] is Relation-like set
bool [:O,(Funcs (G,G)):] is non empty set
bool G is non empty set
s2 is Element of bool G
s1 is Relation-like O -defined Funcs (G,G) -valued Function-like total quasi_total Element of bool [:O,(Funcs (G,G)):]
bool G is non empty Element of bool (bool G)
bool (bool G) is non empty set
s19 is set
meet s19 is set
[#] G is non proper Element of bool G
p is set
p is Element of bool G
f1 is set
i is set
s199 is Element of bool G
[:G,G:] is Relation-like set
bool [:G,G:] is non empty set
f1 is Element of O
i is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]
s1 . f1 is Relation-like Function-like set
s199 is set
i .: p is Element of bool G
s199 is set
i .: s199 is Element of bool G
f2 is Element of bool G
f1 is Element of bool G
f1 is Element of bool G
s19 is Element of bool G
s29 is Element of bool G
O is set
G is set
Funcs (G,G) is functional non empty set
[:O,(Funcs (G,G)):] is Relation-like set
bool [:O,(Funcs (G,G)):] is non empty set
s2 is Relation-like NAT -defined O -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of O
len s2 is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT
[:G,G:] is Relation-like set
bool [:G,G:] is non empty set
id G is Relation-like G -defined G -valued Function-like one-to-one total quasi_total Element of bool [:G,G:]
s1 is Relation-like O -defined Funcs (G,G) -valued Function-like total quasi_total Element of bool [:O,(Funcs (G,G)):]
s2 . 1 is set
s1 . (s2 . 1) is Relation-like Function-like set
s19 is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT
s19 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT
s29 is Relation-like NAT -defined O -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of O
len s29 is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT
s29 . 1 is set
s1 . (s29 . 1) is Relation-like Function-like set
Seg s19 is finite s19 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT : ( 1 <= b1 & b1 <= s19 ) } is set
s29 | (Seg s19) is Relation-like NAT -defined Seg s19 -defined NAT -defined O -valued Function-like finite FinSubsequence-like Element of bool [:NAT,O:]
[:NAT,O:] is Relation-like set
bool [:NAT,O:] is non empty set
p is Relation-like NAT -defined O -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of O
len p is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT
Seg (len s29) is finite len s29 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT : ( 1 <= b1 & b1 <= len s29 ) } is set
dom s29 is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of bool NAT
rng s29 is finite Element of bool O
bool O is non empty set
dom s1 is Element of bool O
rng s1 is functional Element of bool (Funcs (G,G))
bool (Funcs (G,G)) is non empty set
the Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:] is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]
s199 is Relation-like Function-like Element of Funcs (G,G)
<*s199*> is Relation-like NAT -defined Funcs (G,G) -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on (Funcs (G,G))
1 -tuples_on (Funcs (G,G)) is FinSequenceSet of Funcs (G,G)
[1,s199] is set
{1,s199} is non empty finite set
{{1,s199},{1}} is non empty finite V39() set
{[1,s199]} is Relation-like Function-like constant non empty trivial finite 1 -element set
p is Relation-like Function-like set
dom p is set
rng p is set
len <*s199*> is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT
<*s199*> . (len <*s199*>) is Relation-like Function-like set
<*s199*> . 1 is Relation-like Function-like set
f2 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]
p is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal ext-real non negative set
<*s199*> . p is Relation-like Function-like set
p + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT
s29 . (p + 1) is set
s1 . (s29 . (p + 1)) is Relation-like Function-like set
<*s199*> . (p + 1) is Relation-like Function-like set
the Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:] * the Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:] is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]
s29 . (s19 + 1) is set
s1 . (s29 . (s19 + 1)) is Relation-like Function-like set
0 + s19 is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT
Seg (s19 + 1) is non empty finite s19 + 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT : ( 1 <= b1 & b1 <= s19 + 1 ) } is set
(Seg (s19 + 1)) /\ (Seg s19) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of bool NAT
dom s29 is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of bool NAT
(dom s29) /\ (Seg s19) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of bool NAT
Seg (len s29) is finite len s29 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT : ( 1 <= b1 & b1 <= len s29 ) } is set
rng s29 is finite Element of bool O
bool O is non empty set
dom s1 is Element of bool O
rng s1 is functional Element of bool (Funcs (G,G))
bool (Funcs (G,G)) is non empty set
s199 is Relation-like Function-like set
dom s199 is set
rng s199 is set
p . 1 is set
s1 . (p . 1) is Relation-like Function-like set
s199 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]
s199 is Relation-like NAT -defined Funcs (G,G) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs (G,G)
len s199 is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT
s199 . (len s199) is Relation-like Function-like set
s199 . 1 is Relation-like Function-like set
s199 . s19 is Relation-like Function-like set
Seg (len s199) is finite len s199 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT : ( 1 <= b1 & b1 <= len s199 ) } is set
dom s199 is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of bool NAT
H1 is Relation-like Function-like set
dom H1 is set
rng H1 is set
i is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]
p is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]
p * i is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]
<*(p * i)*> is Relation-like NAT -defined bool [:G,G:] -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on (bool [:G,G:])
1 -tuples_on (bool [:G,G:]) is FinSequenceSet of bool [:G,G:]
[1,(p * i)] is set
{1,(p * i)} is non empty finite set
{{1,(p * i)},{1}} is non empty finite V39() set
{[1,(p * i)]} is Relation-like Function-like constant non empty trivial finite 1 -element set
s199 ^ <*(p * i)*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
j is Relation-like NAT -defined Funcs (G,G) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs (G,G)
len j is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT
j . (len j) is Relation-like Function-like set
j . 1 is Relation-like Function-like set
len <*(p * i)*> is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT
(len p) + (len <*(p * i)*>) is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT
(len s199) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT
(len p) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT
H2 is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal ext-real non negative set
j . H2 is Relation-like Function-like set
H2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT
s29 . (H2 + 1) is set
s1 . (s29 . (H2 + 1)) is Relation-like Function-like set
j . (H2 + 1) is Relation-like Function-like set
H1 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]
s299 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]
H1 * s299 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]
s199 . H2 is Relation-like Function-like set
p . (H2 + 1) is set
s1 . (p . (H2 + 1)) is Relation-like Function-like set
s199 . (H2 + 1) is Relation-like Function-like set
s299 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]
H1 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]
s299 * H1 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]
1 + s19 is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT
s19 is Relation-like NAT -defined O -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of O
len s19 is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT
s19 . 1 is set
s1 . (s19 . 1) is Relation-like Function-like set
s29 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]
s19 is Relation-like NAT -defined Funcs (G,G) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs (G,G)
len s19 is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT
s19 . (len s19) is Relation-like Function-like set
s19 . 1 is Relation-like Function-like set
s19 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]
p is Relation-like NAT -defined Funcs (G,G) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs (G,G)
p . (len s2) is Relation-like Function-like set
len p is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT
p . 1 is Relation-like Function-like set
s29 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]
f1 is Relation-like NAT -defined Funcs (G,G) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs (G,G)
f1 . (len s2) is Relation-like Function-like set
len f1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT
f1 . 1 is Relation-like Function-like set
i is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal ext-real non negative set
p . i is Relation-like Function-like set
f1 . i is Relation-like Function-like set
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT
p . (i + 1) is Relation-like Function-like set
f1 . (i + 1) is Relation-like Function-like set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT
s2 . (i + 1) is set
s1 . (s2 . (i + 1)) is Relation-like Function-like set
s199 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]
s199 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]
s199 * s199 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]
f2 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]
p is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]
f2 * p is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]
p . 0 is Relation-like Function-like set
f1 . 0 is Relation-like Function-like set
s19 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]
s29 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]
p is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]
i is Relation-like NAT -defined Funcs (G,G) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs (G,G)
i . (len s2) is Relation-like Function-like set
len i is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT
i . 1 is Relation-like Function-like set
f1 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]
s199 is Relation-like NAT -defined Funcs (G,G) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs (G,G)
s199 . (len s2) is Relation-like Function-like set
len s199 is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT
s199 . 1 is Relation-like Function-like set
O is set
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
Funcs ( the carrier of G, the carrier of G) is functional non empty set
[:O,(Funcs ( the carrier of G, the carrier of G)):] is Relation-like set
bool [:O,(Funcs ( the carrier of G, the carrier of G)):] is non empty set
O is set
the non empty set is non empty set
[: the non empty set , the non empty set :] is Relation-like non empty set
[:[: the non empty set , the non empty set :], the non empty set :] is Relation-like non empty set
bool [:[: the non empty set , the non empty set :], the non empty set :] is non empty set
the Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like non empty total quasi_total Element of bool [:[: the non empty set , the non empty set :], the non empty set :] is Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like non empty total quasi_total Element of bool [:[: the non empty set , the non empty set :], the non empty set :]
Funcs ( the non empty set , the non empty set ) is functional non empty set
[:O,(Funcs ( the non empty set , the non empty set )):] is Relation-like set
bool [:O,(Funcs ( the non empty set , the non empty set )):] is non empty set
the Relation-like O -defined Funcs ( the non empty set , the non empty set ) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the non empty set , the non empty set )):] is Relation-like O -defined Funcs ( the non empty set , the non empty set ) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the non empty set , the non empty set )):]
(O, the non empty set , the Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like non empty total quasi_total Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Relation-like O -defined Funcs ( the non empty set , the non empty set ) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the non empty set , the non empty set )):]) is (O) (O)
O is set
O is set
G is set
id G is Relation-like G -defined G -valued Function-like one-to-one total quasi_total Element of bool [:G,G:]
[:G,G:] is Relation-like set
bool [:G,G:] is non empty set
{(id G)} is functional non empty trivial finite 1 -element set
[:O,{(id G)}:] is Relation-like set
Funcs (G,G) is functional non empty set
[:O,(Funcs (G,G)):] is Relation-like set
bool [:O,(Funcs (G,G)):] is non empty set
s2 is set
s19 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]
s2 is Relation-like O -defined Funcs (G,G) -valued Element of bool [:O,(Funcs (G,G)):]
dom s2 is Element of bool O
bool O is non empty set
s19 is set
s29 is set
p is set
[s19,p] is set
{s19,p} is non empty finite set
{s19} is non empty trivial finite 1 -element set
{{s19,p},{s19}} is non empty finite V39() set
s19 is set
s29 is set
[s19,s29] is set
{s19,s29} is non empty finite set
{s19} is non empty trivial finite 1 -element set
{{s19,s29},{s19}} is non empty finite V39() set
p is set
[s19,p] is set
{s19,p} is non empty finite set
{{s19,p},{s19}} is non empty finite V39() set
f1 is set
i is set
[f1,i] is set
{f1,i} is non empty finite set
{f1} is non empty trivial finite 1 -element set
{{f1,i},{f1}} is non empty finite V39() set
s199 is set
s199 is set
[s199,s199] is set
{s199,s199} is non empty finite set
{s199} is non empty trivial finite 1 -element set
{{s199,s199},{s199}} is non empty finite V39() set
s19 is Relation-like O -defined Funcs (G,G) -valued Function-like Element of bool [:O,(Funcs (G,G)):]
O is set
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
Funcs ( the carrier of G, the carrier of G) is functional non empty set
[:O,(Funcs ( the carrier of G, the carrier of G)):] is Relation-like set
bool [:O,(Funcs ( the carrier of G, the carrier of G)):] is non empty set
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one non empty total quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is Relation-like non empty set
bool [: the carrier of G, the carrier of G:] is non empty set
{(id the carrier of G)} is functional non empty trivial finite 1 -element set
[:O,{(id the carrier of G)}:] is Relation-like set
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
s1 is Relation-like O -defined Funcs ( the carrier of G, the carrier of G) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the carrier of G, the carrier of G)):]
(O, the carrier of G, the multF of G,s1) is (O) (O)
p is non empty (O)
1_ G is non being_of_order_0 Element of the carrier of G
f1 is non empty multMagma
the carrier of f1 is non empty set
s199 is Element of the carrier of f1
f2 is Element of the carrier of f1
p is Element of the carrier of G
p " is Element of the carrier of G
s199 is Element of the carrier of f1
f2 * s199 is Element of the carrier of f1
the multF of f1 is Relation-like [: the carrier of f1, the carrier of f1:] -defined the carrier of f1 -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of f1, the carrier of f1:], the carrier of f1:]
[: the carrier of f1, the carrier of f1:] is Relation-like non empty set
[:[: the carrier of f1, the carrier of f1:], the carrier of f1:] is Relation-like non empty set
bool [:[: the carrier of f1, the carrier of f1:], the carrier of f1:] is non empty set
the multF of f1 . (f2,s199) is Element of the carrier of f1
p * (1_ G) is Element of the carrier of G
the multF of G . (p,(1_ G)) is Element of the carrier of G
s199 * f2 is Element of the carrier of f1
the multF of f1 . (s199,f2) is Element of the carrier of f1
(1_ G) * p is Element of the carrier of G
the multF of G . ((1_ G),p) is Element of the carrier of G
j is Element of the carrier of f1
j is Element of the carrier of f1
f2 * j is Element of the carrier of f1
the multF of f1 . (f2,j) is Element of the carrier of f1
p * (p ") is Element of the carrier of G
the multF of G . (p,(p ")) is Element of the carrier of G
j * f2 is Element of the carrier of f1
the multF of f1 . (j,f2) is Element of the carrier of f1
(p ") * p is Element of the carrier of G
the multF of G . ((p "),p) is Element of the carrier of G
the carrier of p is non empty set
the multF of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]
[: the carrier of p, the carrier of p:] is Relation-like non empty set
[:[: the carrier of p, the carrier of p:], the carrier of p:] is Relation-like non empty set
bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set
multMagma(# the carrier of p, the multF of p #) is non empty strict multMagma
i is non empty unital Group-like associative multMagma
the carrier of i is non empty set
Funcs ( the carrier of i, the carrier of i) is functional non empty set
[:O,(Funcs ( the carrier of i, the carrier of i)):] is Relation-like set
bool [:O,(Funcs ( the carrier of i, the carrier of i)):] is non empty set
Funcs ( the carrier of p, the carrier of p) is functional non empty set
s199 is Relation-like O -defined Funcs ( the carrier of i, the carrier of i) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the carrier of i, the carrier of i)):]
the of p is Relation-like O -defined Funcs ( the carrier of p, the carrier of p) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the carrier of p, the carrier of p)):]
[:O,(Funcs ( the carrier of p, the carrier of p)):] is Relation-like set
bool [:O,(Funcs ( the carrier of p, the carrier of p)):] is non empty set
the multF of i is Relation-like [: the carrier of i, the carrier of i:] -defined the carrier of i -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of i, the carrier of i:], the carrier of i:]
[: the carrier of i, the carrier of i:] is Relation-like non empty set
[:[: the carrier of i, the carrier of i:], the carrier of i:] is Relation-like non empty set
bool [:[: the carrier of i, the carrier of i:], the carrier of i:] is non empty set
multMagma(# the carrier of i, the multF of i #) is non empty strict multMagma
s199 is Element of O
dom s1 is Element of bool O
bool O is non empty set
s1 . s199 is Relation-like Function-like set
[s199,(s1 . s199)] is set
{s199,(s1 . s199)} is non empty finite set
{s199} is non empty trivial finite 1 -element set
{{s199,(s1 . s199)},{s199}} is non empty finite V39() set
id the carrier of i is Relation-like the carrier of i -defined the carrier of i -valued Function-like one-to-one non empty total quasi_total Element of bool [: the carrier of i, the carrier of i:]
bool [: the carrier of i, the carrier of i:] is non empty set
{(id the carrier of i)} is functional non empty trivial finite 1 -element set
[:O,{(id the carrier of i)}:] is Relation-like set
f2 is set
p is set
[f2,p] is set
{f2,p} is non empty finite set
{f2} is non empty trivial finite 1 -element set
{{f2,p},{f2}} is non empty finite V39() set
s199 . s199 is Relation-like Function-like set
i is Element of the carrier of f1
s199 is Element of the carrier of f1
s199 is Element of the carrier of f1
i * s199 is Element of the carrier of f1
the multF of f1 . (i,s199) is Element of the carrier of f1
(i * s199) * s199 is Element of the carrier of f1
the multF of f1 . ((i * s199),s199) is Element of the carrier of f1
f2 is Element of the carrier of G
p is Element of the carrier of G
f2 * p is Element of the carrier of G
the multF of G . (f2,p) is Element of the carrier of G
H1 is Element of the carrier of G
(f2 * p) * H1 is Element of the carrier of G
the multF of G . ((f2 * p),H1) is Element of the carrier of G
p * H1 is Element of the carrier of G
the multF of G . (p,H1) is Element of the carrier of G
f2 * (p * H1) is Element of the carrier of G
the multF of G . (f2,(p * H1)) is Element of the carrier of G
s199 * s199 is Element of the carrier of f1
the multF of f1 . (s199,s199) is Element of the carrier of f1
i * (s199 * s199) is Element of the carrier of f1
the multF of f1 . (i,(s199 * s199)) is Element of the carrier of f1
i is Element of the carrier of f1
O is set
the non empty strict unital Group-like associative multMagma is non empty strict unital Group-like associative multMagma
s1 is non empty (O)
the carrier of s1 is non empty set
the multF of s1 is Relation-like [: the carrier of s1, the carrier of s1:] -defined the carrier of s1 -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of s1, the carrier of s1:], the carrier of s1:]
[: the carrier of s1, the carrier of s1:] is Relation-like non empty set
[:[: the carrier of s1, the carrier of s1:], the carrier of s1:] is Relation-like non empty set
bool [:[: the carrier of s1, the carrier of s1:], the carrier of s1:] is non empty set
multMagma(# the carrier of s1, the multF of s1 #) is non empty strict multMagma
O is set
s1 is Element of O
G is non empty unital Group-like associative (O) (O)
the of G is Relation-like O -defined Funcs ( the carrier of G, the carrier of G) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the carrier of G, the carrier of G)):]
the carrier of G is non empty set
Funcs ( the carrier of G, the carrier of G) is functional non empty set
[:O,(Funcs ( the carrier of G, the carrier of G)):] is Relation-like set
bool [:O,(Funcs ( the carrier of G, the carrier of G)):] is non empty set
the of G . s1 is Relation-like Function-like set
[: the carrier of G, the carrier of G:] is Relation-like non empty set
bool [: the carrier of G, the carrier of G:] is non empty set
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one non empty total quasi_total Element of bool [: the carrier of G, the carrier of G:]
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
multMagma(# the carrier of G, the multF of G #) is non empty strict multMagma
s2 is non empty unital Group-like associative multMagma
the carrier of s2 is non empty set
the multF of s2 is Relation-like [: the carrier of s2, the carrier of s2:] -defined the carrier of s2 -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of s2, the carrier of s2:], the carrier of s2:]
[: the carrier of s2, the carrier of s2:] is Relation-like non empty set
[:[: the carrier of s2, the carrier of s2:], the carrier of s2:] is Relation-like non empty set
bool [:[: the carrier of s2, the carrier of s2:], the carrier of s2:] is non empty set
multMagma(# the carrier of s2, the multF of s2 #) is non empty strict multMagma
Funcs ( the carrier of s2, the carrier of s2) is functional non empty set
[:O,(Funcs ( the carrier of s2, the carrier of s2)):] is Relation-like set
bool [:O,(Funcs ( the carrier of s2, the carrier of s2)):] is non empty set
s19 is Relation-like O -defined Funcs ( the carrier of s2, the carrier of s2) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the carrier of s2, the carrier of s2)):]
bool [: the carrier of s2, the carrier of s2:] is non empty set
s19 . s1 is Relation-like Function-like set
s29 is Relation-like the carrier of s2 -defined the carrier of s2 -valued Function-like non empty total quasi_total unity-preserving multiplicative Element of bool [: the carrier of s2, the carrier of s2:]
f1 is Element of the carrier of G
i is Element of the carrier of G
p is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty total quasi_total Element of bool [: the carrier of G, the carrier of G:]
f1 * i is Element of the carrier of G
the multF of G . (f1,i) is Element of the carrier of G
p . (f1 * i) is Element of the carrier of G
s199 is Element of the carrier of s2
s199 is Element of the carrier of s2
s199 * s199 is Element of the carrier of s2
the multF of s2 . (s199,s199) is Element of the carrier of s2
s29 . (s199 * s199) is Element of the carrier of s2
s29 . s199 is Element of the carrier of s2
s29 . s199 is Element of the carrier of s2
(s29 . s199) * (s29 . s199) is Element of the carrier of s2
the multF of s2 . ((s29 . s199),(s29 . s199)) is Element of the carrier of s2
p . f1 is Element of the carrier of G
p . i is Element of the carrier of G
the multF of G . ((p . f1),(p . i)) is Element of the carrier of G
(p . f1) * (p . i) is Element of the carrier of G
O is set
G is non empty unital Group-like associative (O) (O)
the carrier of G is non empty set
s2 is Element of O
(O,G,s2) is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty total quasi_total unity-preserving multiplicative Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is Relation-like non empty set
bool [: the carrier of G, the carrier of G:] is non empty set
(O,G,s2) | the carrier of G is Relation-like the carrier of G -defined the carrier of G -defined the carrier of G -valued Function-like Element of bool [: the carrier of G, the carrier of G:]
O is set
G is non empty unital Group-like associative (O) (O)
the carrier of G is non empty set
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is Relation-like non empty set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
the of G is Relation-like O -defined Funcs ( the carrier of G, the carrier of G) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the carrier of G, the carrier of G)):]
Funcs ( the carrier of G, the carrier of G) is functional non empty set
[:O,(Funcs ( the carrier of G, the carrier of G)):] is Relation-like set
bool [:O,(Funcs ( the carrier of G, the carrier of G)):] is non empty set
(O, the carrier of G, the multF of G, the of G) is (O) (O)
1_ G is non being_of_order_0 Element of the carrier of G
s1 is non empty multMagma
the carrier of s1 is non empty set
s19 is Element of the carrier of s1
p is Element of the carrier of s1
f1 is Element of the carrier of G
f1 " is Element of the carrier of G
s29 is Element of the carrier of s1
p * s29 is Element of the carrier of s1
the multF of s1 is Relation-like [: the carrier of s1, the carrier of s1:] -defined the carrier of s1 -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of s1, the carrier of s1:], the carrier of s1:]
[: the carrier of s1, the carrier of s1:] is Relation-like non empty set
[:[: the carrier of s1, the carrier of s1:], the carrier of s1:] is Relation-like non empty set
bool [:[: the carrier of s1, the carrier of s1:], the carrier of s1:] is non empty set
the multF of s1 . (p,s29) is Element of the carrier of s1
f1 * (1_ G) is Element of the carrier of G
the multF of G . (f1,(1_ G)) is Element of the carrier of G
s29 * p is Element of the carrier of s1
the multF of s1 . (s29,p) is Element of the carrier of s1
(1_ G) * f1 is Element of the carrier of G
the multF of G . ((1_ G),f1) is Element of the carrier of G
s199 is Element of the carrier of s1
s199 is Element of the carrier of s1
p * s199 is Element of the carrier of s1
the multF of s1 . (p,s199) is Element of the carrier of s1
f1 * (f1 ") is Element of the carrier of G
the multF of G . (f1,(f1 ")) is Element of the carrier of G
s199 * p is Element of the carrier of s1
the multF of s1 . (s199,p) is Element of the carrier of s1
(f1 ") * f1 is Element of the carrier of G
the multF of G . ((f1 "),f1) is Element of the carrier of G
s2 is Element of the carrier of s1
s19 is Element of the carrier of s1
s29 is Element of the carrier of s1
s2 * s19 is Element of the carrier of s1
the multF of s1 . (s2,s19) is Element of the carrier of s1
(s2 * s19) * s29 is Element of the carrier of s1
the multF of s1 . ((s2 * s19),s29) is Element of the carrier of s1
p is Element of the carrier of G
f1 is Element of the carrier of G
p * f1 is Element of the carrier of G
the multF of G . (p,f1) is Element of the carrier of G
i is Element of the carrier of G
(p * f1) * i is Element of the carrier of G
the multF of G . ((p * f1),i) is Element of the carrier of G
f1 * i is Element of the carrier of G
the multF of G . (f1,i) is Element of the carrier of G
p * (f1 * i) is Element of the carrier of G
the multF of G . (p,(f1 * i)) is Element of the carrier of G
s19 * s29 is Element of the carrier of s1
the multF of s1 . (s19,s29) is Element of the carrier of s1
s2 * (s19 * s29) is Element of the carrier of s1
the multF of s1 . (s2,(s19 * s29)) is Element of the carrier of s1
s19 is Element of the carrier of s1
s2 is non empty unital Group-like associative (O) (O)
the carrier of s2 is non empty set
Funcs ( the carrier of s2, the carrier of s2) is functional non empty set
the of s2 is Relation-like O -defined Funcs ( the carrier of s2, the carrier of s2) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the carrier of s2, the carrier of s2)):]
[:O,(Funcs ( the carrier of s2, the carrier of s2)):] is Relation-like set
bool [:O,(Funcs ( the carrier of s2, the carrier of s2)):] is non empty set
the multF of s2 is Relation-like [: the carrier of s2, the carrier of s2:] -defined the carrier of s2 -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of s2, the carrier of s2:], the carrier of s2:]
[: the carrier of s2, the carrier of s2:] is Relation-like non empty set
[:[: the carrier of s2, the carrier of s2:], the carrier of s2:] is Relation-like non empty set
bool [:[: the carrier of s2, the carrier of s2:], the carrier of s2:] is non empty set
multMagma(# the carrier of s2, the multF of s2 #) is non empty strict multMagma
s19 is non empty unital Group-like associative multMagma
the carrier of s19 is non empty set
Funcs ( the carrier of s19, the carrier of s19) is functional non empty set
[:O,(Funcs ( the carrier of s19, the carrier of s19)):] is Relation-like set
bool [:O,(Funcs ( the carrier of s19, the carrier of s19)):] is non empty set
s29 is Relation-like O -defined Funcs ( the carrier of s19, the carrier of s19) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the carrier of s19, the carrier of s19)):]
the multF of s19 is Relation-like [: the carrier of s19, the carrier of s19:] -defined the carrier of s19 -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of s19, the carrier of s19:], the carrier of s19:]
[: the carrier of s19, the carrier of s19:] is Relation-like non empty set
[:[: the carrier of s19, the carrier of s19:], the carrier of s19:] is Relation-like non empty set
bool [:[: the carrier of s19, the carrier of s19:], the carrier of s19:] is non empty set
multMagma(# the carrier of s19, the multF of s19 #) is non empty strict multMagma
s29 is Element of O
s19 is non empty unital Group-like associative (O) (O)
(O,s19,s29) is Relation-like the carrier of s19 -defined the carrier of s19 -valued Function-like non empty total quasi_total unity-preserving multiplicative Element of bool [: the carrier of s19, the carrier of s19:]
the carrier of s19 is non empty set
[: the carrier of s19, the carrier of s19:] is Relation-like non empty set
bool [: the carrier of s19, the carrier of s19:] is non empty set
the of s19 is Relation-like O -defined Funcs ( the carrier of s19, the carrier of s19) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the carrier of s19, the carrier of s19)):]
Funcs ( the carrier of s19, the carrier of s19) is functional non empty set
[:O,(Funcs ( the carrier of s19, the carrier of s19)):] is Relation-like set
bool [:O,(Funcs ( the carrier of s19, the carrier of s19)):] is non empty set
the of s19 . s29 is Relation-like Function-like set
(O,G,s29) is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty total quasi_total unity-preserving multiplicative Element of bool [: the carrier of G, the carrier of G:]
bool [: the carrier of G, the carrier of G:] is non empty set
s29 is Element of O
s19 is non empty unital Group-like associative (O) (O)
the carrier of s19 is non empty set
(O,s19,s29) is Relation-like the carrier of s19 -defined the carrier of s19 -valued Function-like non empty total quasi_total unity-preserving multiplicative Element of bool [: the carrier of s19, the carrier of s19:]
[: the carrier of s19, the carrier of s19:] is Relation-like non empty set
bool [: the carrier of s19, the carrier of s19:] is non empty set
id the carrier of s19 is Relation-like the carrier of s19 -defined the carrier of s19 -valued Function-like one-to-one non empty total quasi_total Element of bool [: the carrier of s19, the carrier of s19:]
(O,G,s29) is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty total quasi_total unity-preserving multiplicative Element of bool [: the carrier of G, the carrier of G:]
bool [: the carrier of G, the carrier of G:] is non empty set
s29 is Element of O
s19 is non empty unital Group-like associative (O) (O)
the carrier of s19 is non empty set
(O,s19,s29) is Relation-like the carrier of s19 -defined the carrier of s19 -valued Function-like non empty total quasi_total unity-preserving multiplicative Element of bool [: the carrier of s19, the carrier of s19:]
[: the carrier of s19, the carrier of s19:] is Relation-like non empty set
bool [: the carrier of s19, the carrier of s19:] is non empty set
(O,G,s29) is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty total quasi_total unity-preserving multiplicative Element of bool [: the carrier of G, the carrier of G:]
bool [: the carrier of G, the carrier of G:] is non empty set
s19 is non empty unital Group-like associative (O) (O)
the carrier of s19 is non empty set
s29 is Element of O
(O,s19,s29) is Relation-like the carrier of s19 -defined the carrier of s19 -valued Function-like non empty total quasi_total unity-preserving multiplicative Element of bool [: the carrier of s19, the carrier of s19:]
[: the carrier of s19, the carrier of s19:] is Relation-like non empty set
bool [: the carrier of s19, the carrier of s19:] is non empty set
(O,G,s29) is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty total quasi_total unity-preserving multiplicative Element of bool [: the carrier of G, the carrier of G:]
bool [: the carrier of G, the carrier of G:] is non empty set
dom (O,s19,s29) is non empty Element of bool the carrier of s19
bool the carrier of s19 is non empty set
(O,G,s29) | the carrier of s19 is Relation-like the carrier of G -defined the carrier of s19 -defined the carrier of G -defined the carrier of G -valued Function-like Element of bool [: the carrier of G, the carrier of G:]
dom the multF of G is Relation-like the carrier of G -defined the carrier of G -valued non empty Element of bool [: the carrier of G, the carrier of G:]
the multF of s19 is Relation-like [: the carrier of s19, the carrier of s19:] -defined the carrier of s19 -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of s19, the carrier of s19:], the carrier of s19:]
[:[: the carrier of s19, the carrier of s19:], the carrier of s19:] is Relation-like non empty set
bool [:[: the carrier of s19, the carrier of s19:], the carrier of s19:] is non empty set
the multF of G || the carrier of s19 is set
the multF of G | [: the carrier of s19, the carrier of s19:] is Relation-like [: the carrier of s19, the carrier of s19:] -defined [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like set
O is set
G is non empty unital Group-like associative (O) (O)
the carrier of G is non empty set
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is Relation-like non empty set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
the of G is Relation-like O -defined Funcs ( the carrier of G, the carrier of G) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the carrier of G, the carrier of G)):]
Funcs ( the carrier of G, the carrier of G) is functional non empty set
[:O,(Funcs ( the carrier of G, the carrier of G)):] is Relation-like set
bool [:O,(Funcs ( the carrier of G, the carrier of G)):] is non empty set
(O, the carrier of G, the multF of G, the of G) is (O) (O)
s1 is non empty unital Group-like associative (O) (O,G)
O is set
G is non empty unital Group-like associative (O) (O)
s1 is non empty unital Group-like associative (O) (O) (O,G)
the carrier of s1 is non empty set
s2 is non empty unital Group-like associative (O) (O) (O,G)
the carrier of s2 is non empty set
the of s2 is Relation-like O -defined Funcs ( the carrier of s2, the carrier of s2) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the carrier of s2, the carrier of s2)):]
Funcs ( the carrier of s2, the carrier of s2) is functional non empty set
[:O,(Funcs ( the carrier of s2, the carrier of s2)):] is Relation-like set
bool [:O,(Funcs ( the carrier of s2, the carrier of s2)):] is non empty set
dom the of s2 is Element of bool O
bool O is non empty set
the of s1 is Relation-like O -defined Funcs ( the carrier of s1, the carrier of s1) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the carrier of s1, the carrier of s1)):]
Funcs ( the carrier of s1, the carrier of s1) is functional non empty set
[:O,(Funcs ( the carrier of s1, the carrier of s1)):] is Relation-like set
bool [:O,(Funcs ( the carrier of s1, the carrier of s1)):] is non empty set
dom the of s1 is Element of bool O
p is set
f1 is Element of O
(O,s1,f1) is Relation-like the carrier of s1 -defined the carrier of s1 -valued Function-like non empty total quasi_total unity-preserving multiplicative Element of bool [: the carrier of s1, the carrier of s1:]
[: the carrier of s1, the carrier of s1:] is Relation-like non empty set
bool [: the carrier of s1, the carrier of s1:] is non empty set
the of s1 . f1 is Relation-like Function-like set
the carrier of G is non empty set
(O,G,f1) is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty total quasi_total unity-preserving multiplicative Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is Relation-like non empty set
bool [: the carrier of G, the carrier of G:] is non empty set
(O,G,f1) | the carrier of s2 is Relation-like the carrier of s2 -defined the carrier of G -defined the carrier of G -valued Function-like Element of bool [: the carrier of G, the carrier of G:]
(O,s2,f1) is Relation-like the carrier of s2 -defined the carrier of s2 -valued Function-like non empty total quasi_total unity-preserving multiplicative Element of bool [: the carrier of s2, the carrier of s2:]
[: the carrier of s2, the carrier of s2:] is Relation-like non empty set
bool [: the carrier of s2, the carrier of s2:] is non empty set
the of s1 . p is Relation-like Function-like set
the of s2 . p is Relation-like Function-like set
s19 is non empty unital Group-like associative Subgroup of G
the carrier of s19 is non empty set
the multF of s19 is Relation-like [: the carrier of s19, the carrier of s19:] -defined the carrier of s19 -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of s19, the carrier of s19:], the carrier of s19:]
[: the carrier of s19, the carrier of s19:] is Relation-like non empty set
[:[: the carrier of s19, the carrier of s19:], the carrier of s19:] is Relation-like non empty set
bool [:[: the carrier of s19, the carrier of s19:], the carrier of s19:] is non empty set
multMagma(# the carrier of s19, the multF of s19 #) is non empty strict multMagma
s29 is non empty unital Group-like associative Subgroup of G
the carrier of s29 is non empty set
the multF of s29 is Relation-like [: the carrier of s29, the carrier of s29:] -defined the carrier of s29 -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of s29, the carrier of s29:], the carrier of s29:]
[: the carrier of s29, the carrier of s29:] is Relation-like non empty set
[:[: the carrier of s29, the carrier of s29:], the carrier of s29:] is Relation-like non empty set
bool [:[: the carrier of s29, the carrier of s29:], the carrier of s29:] is non empty set
multMagma(# the carrier of s29, the multF of s29 #) is non empty strict multMagma
O is set
G is non empty unital Group-like associative (O) (O)
1_ G is non being_of_order_0 Element of the carrier of G
the carrier of G is non empty set
{(1_ G)} is non empty trivial finite 1 -element set
(1). G is non empty trivial finite 1 -element strict unital Group-like associative normal Subgroup of G
s2 is non empty (O)
the carrier of s2 is non empty set
the multF of s2 is Relation-like [: the carrier of s2, the carrier of s2:] -defined the carrier of s2 -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of s2, the carrier of s2:], the carrier of s2:]
[: the carrier of s2, the carrier of s2:] is Relation-like non empty set
[:[: the carrier of s2, the carrier of s2:], the carrier of s2:] is Relation-like non empty set
bool [:[: the carrier of s2, the carrier of s2:], the carrier of s2:] is non empty set
multMagma(# the carrier of s2, the multF of s2 #) is non empty strict multMagma
s19 is non empty unital Group-like associative (O) (O) (O)
the carrier of s19 is non empty set
the multF of s19 is Relation-like [: the carrier of s19, the carrier of s19:] -defined the carrier of s19 -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of s19, the carrier of s19:], the carrier of s19:]
[: the carrier of s19, the carrier of s19:] is Relation-like non empty set
[:[: the carrier of s19, the carrier of s19:], the carrier of s19:] is Relation-like non empty set
bool [:[: the carrier of s19, the carrier of s19:], the carrier of s19:] is non empty set
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is Relation-like non empty set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
the multF of G || the carrier of s19 is set
the multF of G | [: the carrier of s19, the carrier of s19:] is Relation-like [: the carrier of s19, the carrier of s19:] -defined [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like set
s29 is Element of O
(O,s19,s29) is Relation-like the carrier of s19 -defined the carrier of s19 -valued Function-like non empty total quasi_total unity-preserving multiplicative Element of bool [: the carrier of s19, the carrier of s19:]
bool [: the carrier of s19, the carrier of s19:] is non empty set
(O,G,s29) is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty total quasi_total unity-preserving multiplicative Element of bool [: the carrier of G, the carrier of G:]
bool [: the carrier of G, the carrier of G:] is non empty set
(O,G,s29) | the carrier of s19 is Relation-like the carrier of G -defined the carrier of s19 -defined the carrier of G -defined the carrier of G -valued Function-like Element of bool [: the carrier of G, the carrier of G:]
f1 is Relation-like Function-like set
dom f1 is set
id the carrier of s19 is Relation-like the carrier of s19 -defined the carrier of s19 -valued Function-like one-to-one non empty total quasi_total Element of bool [: the carrier of s19, the carrier of s19:]
(O,G,s29) * (id the carrier of s19) is Relation-like the carrier of s19 -defined the carrier of G -valued Function-like Element of bool [: the carrier of s19, the carrier of G:]
[: the carrier of s19, the carrier of G:] is Relation-like non empty set
bool [: the carrier of s19, the carrier of G:] is non empty set
dom ((O,G,s29) * (id the carrier of s19)) is Element of bool the carrier of s19
bool the carrier of s19 is non empty set
dom (O,G,s29) is non empty Element of bool the carrier of G
bool the carrier of G is non empty set
(dom (O,G,s29)) /\ the carrier of s19 is Element of bool the carrier of G
the carrier of G /\ the carrier of s19 is set
the carrier of ((1). G) is non empty trivial finite 1 -element set
i is set
dom (id the carrier of s19) is non empty Element of bool the carrier of s19
1_ s19 is non being_of_order_0 Element of the carrier of s19
p is Relation-like Function-like set
p . i is set
f1 . i is set
((O,G,s29) * (id the carrier of s19)) . i is set
(id the carrier of s19) . i is set
(O,G,s29) . ((id the carrier of s19) . i) is set
(O,G,s29) . i is set
dom p is set
s29 is non empty unital Group-like associative (O) (O) (O,G)
the carrier of s29 is non empty set
s1 is non empty unital Group-like associative (O) (O) (O,G)
the carrier of s1 is non empty set
s2 is non empty unital Group-like associative (O) (O) (O,G)
the carrier of s2 is non empty set
O is set
G is non empty unital Group-like associative (O) (O)
the carrier of G is non empty set
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is Relation-like non empty set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
the of G is Relation-like O -defined Funcs ( the carrier of G, the carrier of G) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the carrier of G, the carrier of G)):]
Funcs ( the carrier of G, the carrier of G) is functional non empty set
[:O,(Funcs ( the carrier of G, the carrier of G)):] is Relation-like set
bool [:O,(Funcs ( the carrier of G, the carrier of G)):] is non empty set
(O, the carrier of G, the multF of G, the of G) is (O) (O)
O is set
G is non empty unital Group-like associative (O) (O)
O is set
G is non empty unital Group-like associative (O) (O)
(O,G) is non empty unital Group-like associative (O) (O) (O,G)
p is non empty strict unital Group-like associative Subgroup of G
s19 is non empty unital Group-like associative (O) (O,G)
the carrier of s19 is non empty set
the multF of s19 is Relation-like [: the carrier of s19, the carrier of s19:] -defined the carrier of s19 -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of s19, the carrier of s19:], the carrier of s19:]
[: the carrier of s19, the carrier of s19:] is Relation-like non empty set
[:[: the carrier of s19, the carrier of s19:], the carrier of s19:] is Relation-like non empty set
bool [:[: the carrier of s19, the carrier of s19:], the carrier of s19:] is non empty set
multMagma(# the carrier of s19, the multF of s19 #) is non empty strict multMagma
s29 is non empty unital Group-like associative multMagma
(1). s29 is non empty trivial finite 1 -element strict unital Group-like associative normal Subgroup of s29
the multF of ((1). s29) is Relation-like [: the carrier of ((1). s29), the carrier of ((1). s29):] -defined the carrier of ((1). s29) -valued Function-like non empty total quasi_total associative finite Element of bool [:[: the carrier of ((1). s29), the carrier of ((1). s29):], the carrier of ((1). s29):]
the carrier of ((1). s29) is non empty trivial finite 1 -element set
[: the carrier of ((1). s29), the carrier of ((1). s29):] is Relation-like non empty finite set
[:[: the carrier of ((1). s29), the carrier of ((1). s29):], the carrier of ((1). s29):] is Relation-like non empty finite set
bool [:[: the carrier of ((1). s29), the carrier of ((1). s29):], the carrier of ((1). s29):] is non empty finite V39() set
the multF of s29 is Relation-like [: the carrier of s29, the carrier of s29:] -defined the carrier of s29 -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of s29, the carrier of s29:], the carrier of s29:]
the carrier of s29 is non empty set
[: the carrier of s29, the carrier of s29:] is Relation-like non empty set
[:[: the carrier of s29, the carrier of s29:], the carrier of s29:] is Relation-like non empty set
bool [:[: the carrier of s29, the carrier of s29:], the carrier of s29:] is non empty set
the multF of s29 || the carrier of ((1). s29) is set
the multF of s29 | [: the carrier of ((1). s29), the carrier of ((1). s29):] is Relation-like [: the carrier of ((1). s29), the carrier of ((1). s29):] -defined [: the carrier of s29, the carrier of s29:] -defined the carrier of s29 -valued Function-like finite set
1_ s29 is non being_of_order_0 Element of the carrier of s29
{(1_ s29)} is non empty trivial finite 1 -element set
the carrier of (O,G) is non empty set
O is set
G is non empty unital Group-like associative (O) (O)
s1 is non empty unital Group-like associative (O) (O,G)
(O,s1) is non empty unital Group-like associative (O) (O) (O,s1)
s2 is non empty unital Group-like associative (O) (O)
s19 is non empty unital Group-like associative (O) (O,s1)
the carrier of s19 is non empty set
the multF of s19 is Relation-like [: the carrier of s19, the carrier of s19:] -defined the carrier of s19 -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of s19, the carrier of s19:], the carrier of s19:]
[: the carrier of s19, the carrier of s19:] is Relation-like non empty set
[:[: the carrier of s19, the carrier of s19:], the carrier of s19:] is Relation-like non empty set
bool [:[: the carrier of s19, the carrier of s19:], the carrier of s19:] is non empty set
multMagma(# the carrier of s19, the multF of s19 #) is non empty strict multMagma
s29 is non empty strict unital Group-like associative Subgroup of s1
the carrier of s29 is non empty set
p is non empty unital Group-like associative multMagma
1_ p is non being_of_order_0 Element of the carrier of p
the carrier of p is non empty set
{(1_ p)} is non empty trivial finite 1 -element set
(1). p is non empty trivial finite 1 -element strict unital Group-like associative normal Subgroup of p
O is set
G is non empty unital Group-like associative (O) (O)
(O,G) is non empty unital Group-like associative (O) (O) (O,G)
s1 is non empty unital Group-like associative multMagma
s2 is non empty strict unital Group-like associative Subgroup of G
the carrier of (O,G) is non empty set
the multF of (O,G) is Relation-like [: the carrier of (O,G), the carrier of (O,G):] -defined the carrier of (O,G) -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of (O,G), the