:: SETWOP_2 semantic presentation

REAL is set
NAT is non empty V15() V16() V17() V43() V48() V49() Element of K19(REAL)
K19(REAL) is cup-closed diff-closed preBoolean set
{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non negative V39() V40() V43() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set
the Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non negative V39() V40() V43() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non negative V39() V40() V43() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set
NAT is non empty V15() V16() V17() V43() V48() V49() set
K19(NAT) is cup-closed diff-closed preBoolean V43() set
K19(NAT) is cup-closed diff-closed preBoolean V43() set
Fin NAT is non empty cup-closed diff-closed preBoolean set
1 is non empty V15() V16() V17() V21() ext-real positive non negative V39() V40() V43() V48() Element of NAT
2 is non empty V15() V16() V17() V21() ext-real positive non negative V39() V40() V43() V48() Element of NAT
3 is non empty V15() V16() V17() V21() ext-real positive non negative V39() V40() V43() V48() Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non negative V39() V40() V43() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
D is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() set
Seg D is V43() V50(D) Element of K19(NAT)
D is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() set
D + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V39() V40() V43() V48() Element of NAT
Seg D is V43() V50(D) Element of K19(NAT)
D is non empty set
d is non empty set
K20(d,d) is Relation-like set
K20(K20(d,d),d) is Relation-like set
K19(K20(K20(d,d),d)) is cup-closed diff-closed preBoolean set
K20(D,d) is Relation-like set
K19(K20(D,d)) is cup-closed diff-closed preBoolean set
F is Element of D
G is Element of D
{.F,G.} is non empty V43() Element of Fin D
Fin D is non empty cup-closed diff-closed preBoolean set
p is Relation-like K20(d,d) -defined d -valued Function-like V14(K20(d,d)) V25(K20(d,d),d) Element of K19(K20(K20(d,d),d))
e is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
p $$ ({.F,G.},e) is Element of d
e . F is Element of d
e . G is Element of d
p . ((e . F),(e . G)) is Element of d
[(e . F),(e . G)] is set
p . [(e . F),(e . G)] is set
K20((Fin D),d) is Relation-like set
K19(K20((Fin D),d)) is cup-closed diff-closed preBoolean set
{F,G} is non empty set
e is Relation-like Fin D -defined d -valued Function-like non empty V14( Fin D) V25( Fin D,d) Element of K19(K20((Fin D),d))
e . {F,G} is set
e . {} is set
{F} is non empty V12() V50(1) set
{F,G} \ {F} is Element of K19({F,G})
K19({F,G}) is cup-closed diff-closed preBoolean set
{G} is non empty V12() V50(1) set
{.F.} is non empty V12() V43() V50(1) Element of Fin D
{.G.} is non empty V12() V43() V50(1) Element of Fin D
{.F.} \/ {.G.} is non empty V43() Element of Fin D
e . ({.F.} \/ {.G.}) is Element of d
e . {F} is set
p . ((e . {F}),(e . G)) is set
[(e . {F}),(e . G)] is set
p . [(e . {F}),(e . G)] is set
D is non empty set
Fin D is non empty cup-closed diff-closed preBoolean set
d is non empty set
K20(d,d) is Relation-like set
K20(K20(d,d),d) is Relation-like set
K19(K20(K20(d,d),d)) is cup-closed diff-closed preBoolean set
K20(D,d) is Relation-like set
K19(K20(D,d)) is cup-closed diff-closed preBoolean set
F is Element of D
{.F.} is non empty V12() V43() V50(1) Element of Fin D
G is V43() Element of Fin D
G \/ {.F.} is non empty V43() Element of Fin D
p is Relation-like K20(d,d) -defined d -valued Function-like V14(K20(d,d)) V25(K20(d,d),d) Element of K19(K20(K20(d,d),d))
e is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
p $$ ((G \/ {.F.}),e) is Element of d
p $$ (G,e) is Element of d
e . F is Element of d
p . ((p $$ (G,e)),(e . F)) is Element of d
[(p $$ (G,e)),(e . F)] is set
p . [(p $$ (G,e)),(e . F)] is set
{}. D is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non negative V39() V40() V43() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of Fin D
the_unity_wrt p is Element of d
K20((Fin D),d) is Relation-like set
K19(K20((Fin D),d)) is cup-closed diff-closed preBoolean set
e is Relation-like Fin D -defined d -valued Function-like non empty V14( Fin D) V25( Fin D,d) Element of K19(K20((Fin D),d))
e . G is Element of d
e . {} is set
{F} is non empty V12() V50(1) set
G \/ {F} is non empty set
d is Relation-like Fin D -defined d -valued Function-like non empty V14( Fin D) V25( Fin D,d) Element of K19(K20((Fin D),d))
d . (G \/ {F}) is set
d . {} is set
u is V43() Element of Fin D
d . u is set
e . u is set
c is Element of D
{c} is non empty V12() V50(1) set
u \/ {c} is non empty set
d . (u \/ {c}) is set
e . (u \/ {c}) is set
d . u is Element of d
e . u is Element of d
G \ u is V43() Element of Fin D
(G \/ {F}) \ u is Element of K19((G \/ {F}))
K19((G \/ {F})) is cup-closed diff-closed preBoolean set
e . c is Element of d
e . c is Element of d
p . ((e . u),(e . c)) is Element of d
[(e . u),(e . c)] is set
p . [(e . u),(e . c)] is set
{}. D is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non negative V39() V40() V43() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of Fin D
d . ({}. D) is set
e . ({}. D) is set
(G \/ {F}) \ G is Element of K19((G \/ {F}))
K19((G \/ {F})) is cup-closed diff-closed preBoolean set
d . G is Element of d
p . ((d . G),(e . F)) is Element of d
[(d . G),(e . F)] is set
p . [(d . G),(e . F)] is set
D is non empty set
d is non empty set
K20(d,d) is Relation-like set
K20(K20(d,d),d) is Relation-like set
K19(K20(K20(d,d),d)) is cup-closed diff-closed preBoolean set
K20(D,d) is Relation-like set
K19(K20(D,d)) is cup-closed diff-closed preBoolean set
F is Element of D
G is Element of D
p is Element of D
{.F,G,p.} is V43() Element of Fin D
Fin D is non empty cup-closed diff-closed preBoolean set
e is Relation-like K20(d,d) -defined d -valued Function-like V14(K20(d,d)) V25(K20(d,d),d) Element of K19(K20(K20(d,d),d))
e is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
e $$ ({.F,G,p.},e) is Element of d
e . F is Element of d
e . G is Element of d
e . ((e . F),(e . G)) is Element of d
[(e . F),(e . G)] is set
e . [(e . F),(e . G)] is set
e . p is Element of d
e . ((e . ((e . F),(e . G))),(e . p)) is Element of d
[(e . ((e . F),(e . G))),(e . p)] is set
e . [(e . ((e . F),(e . G))),(e . p)] is set
{F,G} is non empty set
{.F,G.} is non empty V43() Element of Fin D
{.p.} is non empty V12() V43() V50(1) Element of Fin D
{.F,G.} \/ {.p.} is non empty V43() Element of Fin D
e $$ (({.F,G.} \/ {.p.}),e) is Element of d
e $$ ({.F,G.},e) is Element of d
e . ((e $$ ({.F,G.},e)),(e . p)) is Element of d
[(e $$ ({.F,G.},e)),(e . p)] is set
e . [(e $$ ({.F,G.},e)),(e . p)] is set
D is non empty set
Fin D is non empty cup-closed diff-closed preBoolean set
d is non empty set
K20(d,d) is Relation-like set
K20(K20(d,d),d) is Relation-like set
K19(K20(K20(d,d),d)) is cup-closed diff-closed preBoolean set
K20(D,d) is Relation-like set
K19(K20(D,d)) is cup-closed diff-closed preBoolean set
F is V43() Element of Fin D
G is V43() Element of Fin D
F \/ G is V43() Element of Fin D
p is Relation-like K20(d,d) -defined d -valued Function-like V14(K20(d,d)) V25(K20(d,d),d) Element of K19(K20(K20(d,d),d))
e is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
p $$ ((F \/ G),e) is Element of d
p $$ (F,e) is Element of d
p $$ (G,e) is Element of d
p . ((p $$ (F,e)),(p $$ (G,e))) is Element of d
[(p $$ (F,e)),(p $$ (G,e))] is set
p . [(p $$ (F,e)),(p $$ (G,e))] is set
F /\ G is V43() Element of Fin D
the_unity_wrt p is Element of d
p . ((the_unity_wrt p),(p $$ (G,e))) is Element of d
[(the_unity_wrt p),(p $$ (G,e))] is set
p . [(the_unity_wrt p),(p $$ (G,e))] is set
{}. D is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non negative V39() V40() V43() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of Fin D
p $$ (({}. D),e) is Element of d
p . ((p $$ (({}. D),e)),(p $$ (G,e))) is Element of d
[(p $$ (({}. D),e)),(p $$ (G,e))] is set
p . [(p $$ (({}. D),e)),(p $$ (G,e))] is set
the_unity_wrt p is Element of d
p . ((p $$ (F,e)),(the_unity_wrt p)) is Element of d
[(p $$ (F,e)),(the_unity_wrt p)] is set
p . [(p $$ (F,e)),(the_unity_wrt p)] is set
{}. D is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non negative V39() V40() V43() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of Fin D
p $$ (({}. D),e) is Element of d
p . ((p $$ (F,e)),(p $$ (({}. D),e))) is Element of d
[(p $$ (F,e)),(p $$ (({}. D),e))] is set
p . [(p $$ (F,e)),(p $$ (({}. D),e))] is set
e is V43() Element of Fin D
F /\ e is V43() Element of Fin D
F \/ e is V43() Element of Fin D
p $$ ((F \/ e),e) is Element of d
p $$ (e,e) is Element of d
p . ((p $$ (F,e)),(p $$ (e,e))) is Element of d
[(p $$ (F,e)),(p $$ (e,e))] is set
p . [(p $$ (F,e)),(p $$ (e,e))] is set
d is Element of D
{.d.} is non empty V12() V43() V50(1) Element of Fin D
e \/ {.d.} is non empty V43() Element of Fin D
F /\ (e \/ {.d.}) is V43() Element of Fin D
F \/ (e \/ {.d.}) is non empty V43() Element of Fin D
p $$ ((F \/ (e \/ {.d.})),e) is Element of d
p $$ ((e \/ {.d.}),e) is Element of d
p . ((p $$ (F,e)),(p $$ ((e \/ {.d.}),e))) is Element of d
[(p $$ (F,e)),(p $$ ((e \/ {.d.}),e))] is set
p . [(p $$ (F,e)),(p $$ ((e \/ {.d.}),e))] is set
{d} is non empty V12() V50(1) set
e \/ {d} is non empty set
F /\ (e \/ {d}) is set
e . d is Element of d
p . ((p $$ (F,e)),(e . d)) is Element of d
[(p $$ (F,e)),(e . d)] is set
p . [(p $$ (F,e)),(e . d)] is set
(F \/ e) \/ {.d.} is non empty V43() Element of Fin D
p $$ (((F \/ e) \/ {.d.}),e) is Element of d
e . d is Element of d
p . ((p . ((p $$ (F,e)),(p $$ (e,e)))),(e . d)) is Element of d
[(p . ((p $$ (F,e)),(p $$ (e,e)))),(e . d)] is set
p . [(p . ((p $$ (F,e)),(p $$ (e,e)))),(e . d)] is set
p . ((p $$ (e,e)),(e . d)) is Element of d
[(p $$ (e,e)),(e . d)] is set
p . [(p $$ (e,e)),(e . d)] is set
p . ((p $$ (F,e)),(p . ((p $$ (e,e)),(e . d)))) is Element of d
[(p $$ (F,e)),(p . ((p $$ (e,e)),(e . d)))] is set
p . [(p $$ (F,e)),(p . ((p $$ (e,e)),(e . d)))] is set
{}. D is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non negative V39() V40() V43() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of Fin D
F /\ ({}. D) is Relation-like V43() Element of Fin D
F \/ ({}. D) is V43() Element of Fin D
p $$ ((F \/ ({}. D)),e) is Element of d
p $$ (({}. D),e) is Element of d
p . ((p $$ (F,e)),(p $$ (({}. D),e))) is Element of d
[(p $$ (F,e)),(p $$ (({}. D),e))] is set
p . [(p $$ (F,e)),(p $$ (({}. D),e))] is set
D is non empty set
Fin D is non empty cup-closed diff-closed preBoolean set
d is non empty set
Fin d is non empty cup-closed diff-closed preBoolean set
F is non empty set
K20(F,F) is Relation-like set
K20(K20(F,F),F) is Relation-like set
K19(K20(K20(F,F),F)) is cup-closed diff-closed preBoolean set
K20(D,F) is Relation-like set
K19(K20(D,F)) is cup-closed diff-closed preBoolean set
K20(d,F) is Relation-like set
K19(K20(d,F)) is cup-closed diff-closed preBoolean set
G is V43() Element of Fin D
p is V43() Element of Fin d
e is Relation-like K20(F,F) -defined F -valued Function-like V14(K20(F,F)) V25(K20(F,F),F) Element of K19(K20(K20(F,F),F))
e is Relation-like D -defined F -valued Function-like non empty V14(D) V25(D,F) Element of K19(K20(D,F))
e $$ (G,e) is Element of F
d is Relation-like d -defined F -valued Function-like non empty V14(d) V25(d,F) Element of K19(K20(d,F))
d | p is Relation-like d -defined p -defined d -defined F -valued Function-like Element of K19(K20(d,F))
e $$ (p,d) is Element of F
u is V43() Element of Fin d
d | u is Relation-like d -defined u -defined d -defined F -valued Function-like Element of K19(K20(d,F))
e $$ (u,d) is Element of F
c is Element of d
{.c.} is non empty V12() V43() V50(1) Element of Fin d
u \/ {.c.} is non empty V43() Element of Fin d
d | (u \/ {.c.}) is Relation-like d -defined u \/ {.c.} -defined d -defined F -valued Function-like Element of K19(K20(d,F))
e $$ ((u \/ {.c.}),d) is Element of F
{c} is non empty V12() V50(1) set
u \/ {c} is non empty set
s9 is V43() Element of Fin D
e $$ (s9,e) is Element of F
s is Relation-like Function-like set
dom s is set
rng s is set
s * e is Relation-like F -valued Function-like set
s . c is set
c is Element of D
{.c.} is non empty V12() V43() V50(1) Element of Fin D
s9 \ {.c.} is V43() Element of Fin D
s | u is Relation-like Function-like set
y is set
rng (s | u) is set
dom (s | u) is set
x is set
(s | u) . x is set
s . x is set
(dom s) /\ u is set
{c} is non empty V12() V50(1) set
x is set
s . x is set
{c} is non empty V12() V50(1) set
(dom s) /\ u is set
dom (s | u) is set
(s | u) . x is set
y is set
dom (d | u) is Element of K19(d)
K19(d) is cup-closed diff-closed preBoolean set
(s | u) * e is Relation-like F -valued Function-like set
dom ((s | u) * e) is set
dom d is non empty Element of K19(d)
(dom d) /\ u is Element of K19(d)
(dom d) /\ (u \/ {.c.}) is Element of K19(d)
dom (s * e) is set
s . y is set
dom e is non empty Element of K19(D)
K19(D) is cup-closed diff-closed preBoolean set
(s | u) . y is set
(s | u) . y is set
dom e is non empty Element of K19(D)
K19(D) is cup-closed diff-closed preBoolean set
s . y is set
dom (d | (u \/ {.c.})) is Element of K19(d)
dom d is non empty Element of K19(d)
(dom d) /\ (u \/ {.c.}) is Element of K19(d)
(dom d) /\ u is Element of K19(d)
dom (s * e) is set
d . c is Element of F
(s * e) . c is set
e . c is Element of F
(s9 \ {.c.}) \/ {c} is non empty set
s9 \/ {c} is non empty set
y is set
(d | u) . y is set
((s | u) * e) . y is set
(s | u) . y is set
s . y is set
d . y is set
(s * e) . y is set
e . (s . y) is set
y is set
d .: u is V43() Element of Fin F
Fin F is non empty cup-closed diff-closed preBoolean set
e .: (s9 \ {.c.}) is V43() Element of Fin F
x is set
d . x is set
(s | u) . x is set
((s | u) * e) . x is set
e . ((s | u) . x) is set
x is set
e . x is set
(s | u) " is Relation-like Function-like set
((s | u) ") . x is set
(s | u) . (((s | u) ") . x) is set
((s | u) * e) . (((s | u) ") . x) is set
d . (((s | u) ") . x) is set
e . ((e $$ (u,d)),(d . c)) is Element of F
[(e $$ (u,d)),(d . c)] is set
e . [(e $$ (u,d)),(d . c)] is set
e $$ ((s9 \ {.c.}),e) is Element of F
e . ((e $$ ((s9 \ {.c.}),e)),(e . c)) is Element of F
[(e $$ ((s9 \ {.c.}),e)),(e . c)] is set
e . [(e $$ ((s9 \ {.c.}),e)),(e . c)] is set
{}. d is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non negative V39() V40() V43() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of Fin d
d | ({}. d) is Relation-like non-empty empty-yielding NAT -defined d -defined {}. d -defined d -defined F -valued Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non negative V39() V40() V43() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of K19(K20(d,F))
e $$ (({}. d),d) is Element of F
u is V43() Element of Fin D
e $$ (u,e) is Element of F
c is Relation-like Function-like set
dom c is set
rng c is set
c * e is Relation-like F -valued Function-like set
{}. D is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non negative V39() V40() V43() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of Fin D
the_unity_wrt e is Element of F
u is Relation-like Function-like set
dom u is set
rng u is set
u * e is Relation-like F -valued Function-like set
D is non empty set
Fin D is non empty cup-closed diff-closed preBoolean set
d is non empty set
K20(D,d) is Relation-like set
K19(K20(D,d)) is cup-closed diff-closed preBoolean set
F is non empty set
K20(F,F) is Relation-like set
K20(K20(F,F),F) is Relation-like set
K19(K20(K20(F,F),F)) is cup-closed diff-closed preBoolean set
K20(d,F) is Relation-like set
K19(K20(d,F)) is cup-closed diff-closed preBoolean set
G is V43() Element of Fin D
p is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
p .: G is V43() Element of Fin d
Fin d is non empty cup-closed diff-closed preBoolean set
e is Relation-like K20(F,F) -defined F -valued Function-like V14(K20(F,F)) V25(K20(F,F),F) Element of K19(K20(K20(F,F),F))
e is Relation-like d -defined F -valued Function-like non empty V14(d) V25(d,F) Element of K19(K20(d,F))
e $$ ((p .: G),e) is Element of F
e * p is Relation-like D -defined F -valued Function-like non empty V14(D) V25(D,F) Element of K19(K20(D,F))
K20(D,F) is Relation-like set
K19(K20(D,F)) is cup-closed diff-closed preBoolean set
e $$ (G,(e * p)) is Element of F
p | G is Relation-like D -defined G -defined D -defined d -valued Function-like Element of K19(K20(D,d))
rng (p | G) is set
(e * p) | G is Relation-like D -defined G -defined D -defined F -valued Function-like Element of K19(K20(D,F))
e * (p | G) is Relation-like D -defined F -valued Function-like Element of K19(K20(D,F))
dom p is non empty Element of K19(D)
K19(D) is cup-closed diff-closed preBoolean set
dom (p | G) is Element of K19(D)
D is non empty set
Fin D is non empty cup-closed diff-closed preBoolean set
d is non empty set
K20(d,d) is Relation-like set
K20(K20(d,d),d) is Relation-like set
K19(K20(K20(d,d),d)) is cup-closed diff-closed preBoolean set
K20(D,d) is Relation-like set
K19(K20(D,d)) is cup-closed diff-closed preBoolean set
F is V43() Element of Fin D
G is Relation-like K20(d,d) -defined d -valued Function-like V14(K20(d,d)) V25(K20(d,d),d) Element of K19(K20(K20(d,d),d))
p is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
p | F is Relation-like D -defined F -defined D -defined d -valued Function-like Element of K19(K20(D,d))
G $$ (F,p) is Element of d
e is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
e | F is Relation-like D -defined F -defined D -defined d -valued Function-like Element of K19(K20(D,d))
G $$ (F,e) is Element of d
id F is Relation-like F -defined F -valued Function-like one-to-one V14(F) V25(F,F) Element of K19(K20(F,F))
K20(F,F) is Relation-like set
K19(K20(F,F)) is cup-closed diff-closed preBoolean set
dom (id F) is Element of K19(F)
K19(F) is cup-closed diff-closed preBoolean set
rng (id F) is set
e * (id F) is Relation-like F -defined d -valued Function-like Element of K19(K20(F,d))
K20(F,d) is Relation-like set
K19(K20(F,d)) is cup-closed diff-closed preBoolean set
D is non empty set
Fin D is non empty cup-closed diff-closed preBoolean set
d is non empty set
K20(d,d) is Relation-like set
K20(K20(d,d),d) is Relation-like set
K19(K20(K20(d,d),d)) is cup-closed diff-closed preBoolean set
K20(D,d) is Relation-like set
K19(K20(D,d)) is cup-closed diff-closed preBoolean set
F is V43() Element of Fin D
G is Element of d
{G} is non empty V12() V50(1) set
p is Relation-like K20(d,d) -defined d -valued Function-like V14(K20(d,d)) V25(K20(d,d),d) Element of K19(K20(K20(d,d),d))
the_unity_wrt p is Element of d
e is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
e .: F is V43() Element of Fin d
Fin d is non empty cup-closed diff-closed preBoolean set
p $$ (F,e) is Element of d
e is V43() Element of Fin D
e .: e is V43() Element of Fin d
p $$ (e,e) is Element of d
d is Element of D
{.d.} is non empty V12() V43() V50(1) Element of Fin D
e \/ {.d.} is non empty V43() Element of Fin D
e .: (e \/ {.d.}) is V43() Element of Fin d
p $$ ((e \/ {.d.}),e) is Element of d
{d} is non empty V12() V50(1) set
e \/ {d} is non empty set
e .: (e \/ {d}) is set
{}. D is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non negative V39() V40() V43() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of Fin D
e . d is Element of d
p . ((p $$ (e,e)),(e . d)) is Element of d
[(p $$ (e,e)),(e . d)] is set
p . [(p $$ (e,e)),(e . d)] is set
p . (G,(e . d)) is Element of d
[G,(e . d)] is set
p . [G,(e . d)] is set
dom e is non empty Element of K19(D)
K19(D) is cup-closed diff-closed preBoolean set
e . d is Element of d
p . (G,(e . d)) is Element of d
[G,(e . d)] is set
p . [G,(e . d)] is set
e . d is Element of d
p . (G,(e . d)) is Element of d
[G,(e . d)] is set
p . [G,(e . d)] is set
e . d is Element of d
p . (G,(e . d)) is Element of d
[G,(e . d)] is set
p . [G,(e . d)] is set
dom e is non empty Element of K19(D)
K19(D) is cup-closed diff-closed preBoolean set
Im (e,d) is set
e .: {d} is set
{(e . d)} is non empty V12() V50(1) set
{}. D is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non negative V39() V40() V43() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of Fin D
e .: ({}. D) is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non negative V39() V40() V43() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of Fin d
p $$ (({}. D),e) is Element of d
D is non empty set
Fin D is non empty cup-closed diff-closed preBoolean set
d is non empty set
K20(d,d) is Relation-like set
K20(K20(d,d),d) is Relation-like set
K19(K20(K20(d,d),d)) is cup-closed diff-closed preBoolean set
K20(D,d) is Relation-like set
K19(K20(D,d)) is cup-closed diff-closed preBoolean set
F is V43() Element of Fin D
G is Element of d
p is Relation-like K20(d,d) -defined d -valued Function-like V14(K20(d,d)) V25(K20(d,d),d) Element of K19(K20(K20(d,d),d))
the_unity_wrt p is Element of d
e is Relation-like K20(d,d) -defined d -valued Function-like V14(K20(d,d)) V25(K20(d,d),d) Element of K19(K20(K20(d,d),d))
e . (G,G) is Element of d
[G,G] is set
e . [G,G] is set
e is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
p $$ (F,e) is Element of d
d is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
p $$ (F,d) is Element of d
e . ((p $$ (F,e)),(p $$ (F,d))) is Element of d
[(p $$ (F,e)),(p $$ (F,d))] is set
e . [(p $$ (F,e)),(p $$ (F,d))] is set
e .: (e,d) is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
p $$ (F,(e .: (e,d))) is Element of d
u is V43() Element of Fin D
p $$ (u,e) is Element of d
p $$ (u,d) is Element of d
e . ((p $$ (u,e)),(p $$ (u,d))) is Element of d
[(p $$ (u,e)),(p $$ (u,d))] is set
e . [(p $$ (u,e)),(p $$ (u,d))] is set
p $$ (u,(e .: (e,d))) is Element of d
c is Element of D
{.c.} is non empty V12() V43() V50(1) Element of Fin D
u \/ {.c.} is non empty V43() Element of Fin D
p $$ ((u \/ {.c.}),e) is Element of d
p $$ ((u \/ {.c.}),d) is Element of d
e . ((p $$ ((u \/ {.c.}),e)),(p $$ ((u \/ {.c.}),d))) is Element of d
[(p $$ ((u \/ {.c.}),e)),(p $$ ((u \/ {.c.}),d))] is set
e . [(p $$ ((u \/ {.c.}),e)),(p $$ ((u \/ {.c.}),d))] is set
p $$ ((u \/ {.c.}),(e .: (e,d))) is Element of d
e . c is Element of d
p . ((p $$ (u,e)),(e . c)) is Element of d
[(p $$ (u,e)),(e . c)] is set
p . [(p $$ (u,e)),(e . c)] is set
d . c is Element of d
p . ((p $$ (u,d)),(d . c)) is Element of d
[(p $$ (u,d)),(d . c)] is set
p . [(p $$ (u,d)),(d . c)] is set
e . ((e . c),(d . c)) is Element of d
[(e . c),(d . c)] is set
e . [(e . c),(d . c)] is set
p . ((e . ((p $$ (u,e)),(p $$ (u,d)))),(e . ((e . c),(d . c)))) is Element of d
[(e . ((p $$ (u,e)),(p $$ (u,d)))),(e . ((e . c),(d . c)))] is set
p . [(e . ((p $$ (u,e)),(p $$ (u,d)))),(e . ((e . c),(d . c)))] is set
(e .: (e,d)) . c is Element of d
p . ((e . ((p $$ (u,e)),(p $$ (u,d)))),((e .: (e,d)) . c)) is Element of d
[(e . ((p $$ (u,e)),(p $$ (u,d)))),((e .: (e,d)) . c)] is set
p . [(e . ((p $$ (u,e)),(p $$ (u,d)))),((e .: (e,d)) . c)] is set
{}. D is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non negative V39() V40() V43() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of Fin D
p $$ (({}. D),e) is Element of d
p $$ (({}. D),d) is Element of d
e . ((p $$ (({}. D),e)),(p $$ (({}. D),d))) is Element of d
[(p $$ (({}. D),e)),(p $$ (({}. D),d))] is set
e . [(p $$ (({}. D),e)),(p $$ (({}. D),d))] is set
p $$ (({}. D),(e .: (e,d))) is Element of d
D is non empty set
K20(D,D) is Relation-like set
K20(K20(D,D),D) is Relation-like set
K19(K20(K20(D,D),D)) is cup-closed diff-closed preBoolean set
d is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
F is Element of D
G is Element of D
d . (F,G) is Element of D
[F,G] is set
d . [F,G] is set
p is Element of D
d . (F,p) is Element of D
[F,p] is set
d . [F,p] is set
e is Element of D
d . (p,e) is Element of D
[p,e] is set
d . [p,e] is set
d . ((d . (F,G)),(d . (p,e))) is Element of D
[(d . (F,G)),(d . (p,e))] is set
d . [(d . (F,G)),(d . (p,e))] is set
d . (G,e) is Element of D
[G,e] is set
d . [G,e] is set
d . ((d . (F,p)),(d . (G,e))) is Element of D
[(d . (F,p)),(d . (G,e))] is set
d . [(d . (F,p)),(d . (G,e))] is set
d . (G,(d . (p,e))) is Element of D
[G,(d . (p,e))] is set
d . [G,(d . (p,e))] is set
d . (F,(d . (G,(d . (p,e))))) is Element of D
[F,(d . (G,(d . (p,e))))] is set
d . [F,(d . (G,(d . (p,e))))] is set
d . (G,p) is Element of D
[G,p] is set
d . [G,p] is set
d . ((d . (G,p)),e) is Element of D
[(d . (G,p)),e] is set
d . [(d . (G,p)),e] is set
d . (F,(d . ((d . (G,p)),e))) is Element of D
[F,(d . ((d . (G,p)),e))] is set
d . [F,(d . ((d . (G,p)),e))] is set
d . (p,G) is Element of D
[p,G] is set
d . [p,G] is set
d . ((d . (p,G)),e) is Element of D
[(d . (p,G)),e] is set
d . [(d . (p,G)),e] is set
d . (F,(d . ((d . (p,G)),e))) is Element of D
[F,(d . ((d . (p,G)),e))] is set
d . [F,(d . ((d . (p,G)),e))] is set
d . (p,(d . (G,e))) is Element of D
[p,(d . (G,e))] is set
d . [p,(d . (G,e))] is set
d . (F,(d . (p,(d . (G,e))))) is Element of D
[F,(d . (p,(d . (G,e))))] is set
d . [F,(d . (p,(d . (G,e))))] is set
D is non empty set
Fin D is non empty cup-closed diff-closed preBoolean set
d is non empty set
K20(d,d) is Relation-like set
K20(K20(d,d),d) is Relation-like set
K19(K20(K20(d,d),d)) is cup-closed diff-closed preBoolean set
K20(D,d) is Relation-like set
K19(K20(D,d)) is cup-closed diff-closed preBoolean set
F is V43() Element of Fin D
G is Relation-like K20(d,d) -defined d -valued Function-like V14(K20(d,d)) V25(K20(d,d),d) Element of K19(K20(K20(d,d),d))
p is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
G $$ (F,p) is Element of d
e is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
G $$ (F,e) is Element of d
G . ((G $$ (F,p)),(G $$ (F,e))) is Element of d
[(G $$ (F,p)),(G $$ (F,e))] is set
G . [(G $$ (F,p)),(G $$ (F,e))] is set
G .: (p,e) is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
G $$ (F,(G .: (p,e))) is Element of d
the_unity_wrt G is Element of d
G . ((the_unity_wrt G),(the_unity_wrt G)) is Element of d
[(the_unity_wrt G),(the_unity_wrt G)] is set
G . [(the_unity_wrt G),(the_unity_wrt G)] is set
d is Element of d
u is Element of d
G . (d,u) is Element of d
[d,u] is set
G . [d,u] is set
c is Element of d
s9 is Element of d
G . (c,s9) is Element of d
[c,s9] is set
G . [c,s9] is set
G . ((G . (d,u)),(G . (c,s9))) is Element of d
[(G . (d,u)),(G . (c,s9))] is set
G . [(G . (d,u)),(G . (c,s9))] is set
G . (d,c) is Element of d
[d,c] is set
G . [d,c] is set
G . (u,s9) is Element of d
[u,s9] is set
G . [u,s9] is set
G . ((G . (d,c)),(G . (u,s9))) is Element of d
[(G . (d,c)),(G . (u,s9))] is set
G . [(G . (d,c)),(G . (u,s9))] is set
D is non empty set
Fin D is non empty cup-closed diff-closed preBoolean set
d is non empty set
K20(d,d) is Relation-like set
K20(K20(d,d),d) is Relation-like set
K19(K20(K20(d,d),d)) is cup-closed diff-closed preBoolean set
K20(D,d) is Relation-like set
K19(K20(D,d)) is cup-closed diff-closed preBoolean set
id d is Relation-like d -defined d -valued Function-like one-to-one non empty V14(d) V25(d,d) Element of K19(K20(d,d))
K19(K20(d,d)) is cup-closed diff-closed preBoolean set
F is V43() Element of Fin D
G is Relation-like K20(d,d) -defined d -valued Function-like V14(K20(d,d)) V25(K20(d,d),d) Element of K19(K20(K20(d,d),d))
the_inverseOp_wrt G is Relation-like d -defined d -valued Function-like non empty V14(d) V25(d,d) Element of K19(K20(d,d))
G * ((id d),(the_inverseOp_wrt G)) is Relation-like K20(d,d) -defined d -valued Function-like V14(K20(d,d)) V25(K20(d,d),d) Element of K19(K20(K20(d,d),d))
p is Relation-like K20(d,d) -defined d -valued Function-like V14(K20(d,d)) V25(K20(d,d),d) Element of K19(K20(K20(d,d),d))
e is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
G $$ (F,e) is Element of d
e is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
G $$ (F,e) is Element of d
p . ((G $$ (F,e)),(G $$ (F,e))) is Element of d
[(G $$ (F,e)),(G $$ (F,e))] is set
p . [(G $$ (F,e)),(G $$ (F,e))] is set
p .: (e,e) is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
G $$ (F,(p .: (e,e))) is Element of d
the_unity_wrt G is Element of d
p . ((the_unity_wrt G),(the_unity_wrt G)) is Element of d
[(the_unity_wrt G),(the_unity_wrt G)] is set
p . [(the_unity_wrt G),(the_unity_wrt G)] is set
u is Element of d
c is Element of d
p . (u,c) is Element of d
[u,c] is set
p . [u,c] is set
s9 is Element of d
s is Element of d
p . (s9,s) is Element of d
[s9,s] is set
p . [s9,s] is set
G . ((p . (u,c)),(p . (s9,s))) is Element of d
[(p . (u,c)),(p . (s9,s))] is set
G . [(p . (u,c)),(p . (s9,s))] is set
G . (u,s9) is Element of d
[u,s9] is set
G . [u,s9] is set
G . (c,s) is Element of d
[c,s] is set
G . [c,s] is set
p . ((G . (u,s9)),(G . (c,s))) is Element of d
[(G . (u,s9)),(G . (c,s))] is set
p . [(G . (u,s9)),(G . (c,s))] is set
D is non empty set
Fin D is non empty cup-closed diff-closed preBoolean set
d is non empty set
K20(d,d) is Relation-like set
K20(K20(d,d),d) is Relation-like set
K19(K20(K20(d,d),d)) is cup-closed diff-closed preBoolean set
K20(D,d) is Relation-like set
K19(K20(D,d)) is cup-closed diff-closed preBoolean set
F is V43() Element of Fin D
G is Element of d
p is Element of d
e is Relation-like K20(d,d) -defined d -valued Function-like V14(K20(d,d)) V25(K20(d,d),d) Element of K19(K20(K20(d,d),d))
the_unity_wrt e is Element of d
e is Relation-like K20(d,d) -defined d -valued Function-like V14(K20(d,d)) V25(K20(d,d),d) Element of K19(K20(K20(d,d),d))
e . (p,G) is Element of d
[p,G] is set
e . [p,G] is set
d is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
e $$ (F,d) is Element of d
e . (p,(e $$ (F,d))) is Element of d
[p,(e $$ (F,d))] is set
e . [p,(e $$ (F,d))] is set
e [;] (p,d) is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
e $$ (F,(e [;] (p,d))) is Element of d
u is V43() Element of Fin D
e $$ (u,d) is Element of d
e . (p,(e $$ (u,d))) is Element of d
[p,(e $$ (u,d))] is set
e . [p,(e $$ (u,d))] is set
e $$ (u,(e [;] (p,d))) is Element of d
c is Element of D
{.c.} is non empty V12() V43() V50(1) Element of Fin D
u \/ {.c.} is non empty V43() Element of Fin D
e $$ ((u \/ {.c.}),d) is Element of d
e . (p,(e $$ ((u \/ {.c.}),d))) is Element of d
[p,(e $$ ((u \/ {.c.}),d))] is set
e . [p,(e $$ ((u \/ {.c.}),d))] is set
e $$ ((u \/ {.c.}),(e [;] (p,d))) is Element of d
d . c is Element of d
e . ((e $$ (u,d)),(d . c)) is Element of d
[(e $$ (u,d)),(d . c)] is set
e . [(e $$ (u,d)),(d . c)] is set
e . (p,(e . ((e $$ (u,d)),(d . c)))) is Element of d
[p,(e . ((e $$ (u,d)),(d . c)))] is set
e . [p,(e . ((e $$ (u,d)),(d . c)))] is set
e . (p,(d . c)) is Element of d
[p,(d . c)] is set
e . [p,(d . c)] is set
e . ((e . (p,(e $$ (u,d)))),(e . (p,(d . c)))) is Element of d
[(e . (p,(e $$ (u,d)))),(e . (p,(d . c)))] is set
e . [(e . (p,(e $$ (u,d)))),(e . (p,(d . c)))] is set
(e [;] (p,d)) . c is Element of d
e . ((e $$ (u,(e [;] (p,d)))),((e [;] (p,d)) . c)) is Element of d
[(e $$ (u,(e [;] (p,d)))),((e [;] (p,d)) . c)] is set
e . [(e $$ (u,(e [;] (p,d)))),((e [;] (p,d)) . c)] is set
{}. D is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non negative V39() V40() V43() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of Fin D
e $$ (({}. D),d) is Element of d
e . (p,(e $$ (({}. D),d))) is Element of d
[p,(e $$ (({}. D),d))] is set
e . [p,(e $$ (({}. D),d))] is set
e $$ (({}. D),(e [;] (p,d))) is Element of d
D is non empty set
Fin D is non empty cup-closed diff-closed preBoolean set
d is non empty set
K20(d,d) is Relation-like set
K20(K20(d,d),d) is Relation-like set
K19(K20(K20(d,d),d)) is cup-closed diff-closed preBoolean set
K20(D,d) is Relation-like set
K19(K20(D,d)) is cup-closed diff-closed preBoolean set
F is V43() Element of Fin D
G is Element of d
p is Element of d
e is Relation-like K20(d,d) -defined d -valued Function-like V14(K20(d,d)) V25(K20(d,d),d) Element of K19(K20(K20(d,d),d))
the_unity_wrt e is Element of d
e is Relation-like K20(d,d) -defined d -valued Function-like V14(K20(d,d)) V25(K20(d,d),d) Element of K19(K20(K20(d,d),d))
e . (G,p) is Element of d
[G,p] is set
e . [G,p] is set
d is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
e $$ (F,d) is Element of d
e . ((e $$ (F,d)),p) is Element of d
[(e $$ (F,d)),p] is set
e . [(e $$ (F,d)),p] is set
e [:] (d,p) is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
e $$ (F,(e [:] (d,p))) is Element of d
u is V43() Element of Fin D
e $$ (u,d) is Element of d
e . ((e $$ (u,d)),p) is Element of d
[(e $$ (u,d)),p] is set
e . [(e $$ (u,d)),p] is set
e $$ (u,(e [:] (d,p))) is Element of d
c is Element of D
{.c.} is non empty V12() V43() V50(1) Element of Fin D
u \/ {.c.} is non empty V43() Element of Fin D
e $$ ((u \/ {.c.}),d) is Element of d
e . ((e $$ ((u \/ {.c.}),d)),p) is Element of d
[(e $$ ((u \/ {.c.}),d)),p] is set
e . [(e $$ ((u \/ {.c.}),d)),p] is set
e $$ ((u \/ {.c.}),(e [:] (d,p))) is Element of d
d . c is Element of d
e . ((e $$ (u,d)),(d . c)) is Element of d
[(e $$ (u,d)),(d . c)] is set
e . [(e $$ (u,d)),(d . c)] is set
e . ((e . ((e $$ (u,d)),(d . c))),p) is Element of d
[(e . ((e $$ (u,d)),(d . c))),p] is set
e . [(e . ((e $$ (u,d)),(d . c))),p] is set
e . ((d . c),p) is Element of d
[(d . c),p] is set
e . [(d . c),p] is set
e . ((e . ((e $$ (u,d)),p)),(e . ((d . c),p))) is Element of d
[(e . ((e $$ (u,d)),p)),(e . ((d . c),p))] is set
e . [(e . ((e $$ (u,d)),p)),(e . ((d . c),p))] is set
(e [:] (d,p)) . c is Element of d
e . ((e $$ (u,(e [:] (d,p)))),((e [:] (d,p)) . c)) is Element of d
[(e $$ (u,(e [:] (d,p)))),((e [:] (d,p)) . c)] is set
e . [(e $$ (u,(e [:] (d,p)))),((e [:] (d,p)) . c)] is set
{}. D is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non negative V39() V40() V43() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of Fin D
e $$ (({}. D),d) is Element of d
e . ((e $$ (({}. D),d)),p) is Element of d
[(e $$ (({}. D),d)),p] is set
e . [(e $$ (({}. D),d)),p] is set
e $$ (({}. D),(e [:] (d,p))) is Element of d
D is non empty set
Fin D is non empty cup-closed diff-closed preBoolean set
d is non empty set
K20(d,d) is Relation-like set
K20(K20(d,d),d) is Relation-like set
K19(K20(K20(d,d),d)) is cup-closed diff-closed preBoolean set
K20(D,d) is Relation-like set
K19(K20(D,d)) is cup-closed diff-closed preBoolean set
F is V43() Element of Fin D
G is Element of d
p is Relation-like K20(d,d) -defined d -valued Function-like V14(K20(d,d)) V25(K20(d,d),d) Element of K19(K20(K20(d,d),d))
e is Relation-like K20(d,d) -defined d -valued Function-like V14(K20(d,d)) V25(K20(d,d),d) Element of K19(K20(K20(d,d),d))
e is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
p $$ (F,e) is Element of d
e . (G,(p $$ (F,e))) is Element of d
[G,(p $$ (F,e))] is set
e . [G,(p $$ (F,e))] is set
e [;] (G,e) is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
p $$ (F,(e [;] (G,e))) is Element of d
the_unity_wrt p is Element of d
e . (G,(the_unity_wrt p)) is Element of d
[G,(the_unity_wrt p)] is set
e . [G,(the_unity_wrt p)] is set
D is non empty set
Fin D is non empty cup-closed diff-closed preBoolean set
d is non empty set
K20(d,d) is Relation-like set
K20(K20(d,d),d) is Relation-like set
K19(K20(K20(d,d),d)) is cup-closed diff-closed preBoolean set
K20(D,d) is Relation-like set
K19(K20(D,d)) is cup-closed diff-closed preBoolean set
F is V43() Element of Fin D
G is Element of d
p is Relation-like K20(d,d) -defined d -valued Function-like V14(K20(d,d)) V25(K20(d,d),d) Element of K19(K20(K20(d,d),d))
e is Relation-like K20(d,d) -defined d -valued Function-like V14(K20(d,d)) V25(K20(d,d),d) Element of K19(K20(K20(d,d),d))
e is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
p $$ (F,e) is Element of d
e . ((p $$ (F,e)),G) is Element of d
[(p $$ (F,e)),G] is set
e . [(p $$ (F,e)),G] is set
e [:] (e,G) is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
p $$ (F,(e [:] (e,G))) is Element of d
the_unity_wrt p is Element of d
e . ((the_unity_wrt p),G) is Element of d
[(the_unity_wrt p),G] is set
e . [(the_unity_wrt p),G] is set
D is non empty set
Fin D is non empty cup-closed diff-closed preBoolean set
d is non empty set
K20(d,d) is Relation-like set
K20(K20(d,d),d) is Relation-like set
K19(K20(K20(d,d),d)) is cup-closed diff-closed preBoolean set
F is non empty set
K20(F,F) is Relation-like set
K20(K20(F,F),F) is Relation-like set
K19(K20(K20(F,F),F)) is cup-closed diff-closed preBoolean set
K20(D,F) is Relation-like set
K19(K20(D,F)) is cup-closed diff-closed preBoolean set
K20(F,d) is Relation-like set
K19(K20(F,d)) is cup-closed diff-closed preBoolean set
G is V43() Element of Fin D
p is Relation-like K20(F,F) -defined F -valued Function-like V14(K20(F,F)) V25(K20(F,F),F) Element of K19(K20(K20(F,F),F))
the_unity_wrt p is Element of F
e is Relation-like D -defined F -valued Function-like non empty V14(D) V25(D,F) Element of K19(K20(D,F))
p $$ (G,e) is Element of F
e is Relation-like K20(d,d) -defined d -valued Function-like V14(K20(d,d)) V25(K20(d,d),d) Element of K19(K20(K20(d,d),d))
the_unity_wrt e is Element of d
d is Relation-like F -defined d -valued Function-like non empty V14(F) V25(F,d) Element of K19(K20(F,d))
d . (the_unity_wrt p) is Element of d
d . (p $$ (G,e)) is Element of d
d * e is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
K20(D,d) is Relation-like set
K19(K20(D,d)) is cup-closed diff-closed preBoolean set
e $$ (G,(d * e)) is Element of d
u is V43() Element of Fin D
p $$ (u,e) is Element of F
d . (p $$ (u,e)) is Element of d
e $$ (u,(d * e)) is Element of d
c is Element of D
{.c.} is non empty V12() V43() V50(1) Element of Fin D
u \/ {.c.} is non empty V43() Element of Fin D
p $$ ((u \/ {.c.}),e) is Element of F
d . (p $$ ((u \/ {.c.}),e)) is Element of d
e $$ ((u \/ {.c.}),(d * e)) is Element of d
e . c is Element of F
p . ((p $$ (u,e)),(e . c)) is Element of F
[(p $$ (u,e)),(e . c)] is set
p . [(p $$ (u,e)),(e . c)] is set
d . (p . ((p $$ (u,e)),(e . c))) is Element of d
d . (e . c) is Element of d
e . ((e $$ (u,(d * e))),(d . (e . c))) is Element of d
[(e $$ (u,(d * e))),(d . (e . c))] is set
e . [(e $$ (u,(d * e))),(d . (e . c))] is set
(d * e) . c is Element of d
e . ((e $$ (u,(d * e))),((d * e) . c)) is Element of d
[(e $$ (u,(d * e))),((d * e) . c)] is set
e . [(e $$ (u,(d * e))),((d * e) . c)] is set
{}. D is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non negative V39() V40() V43() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of Fin D
p $$ (({}. D),e) is Element of F
d . (p $$ (({}. D),e)) is Element of d
e $$ (({}. D),(d * e)) is Element of d
D is non empty set
Fin D is non empty cup-closed diff-closed preBoolean set
d is non empty set
K20(d,d) is Relation-like set
K20(K20(d,d),d) is Relation-like set
K19(K20(K20(d,d),d)) is cup-closed diff-closed preBoolean set
K19(K20(d,d)) is cup-closed diff-closed preBoolean set
K20(D,d) is Relation-like set
K19(K20(D,d)) is cup-closed diff-closed preBoolean set
F is V43() Element of Fin D
G is Relation-like K20(d,d) -defined d -valued Function-like V14(K20(d,d)) V25(K20(d,d),d) Element of K19(K20(K20(d,d),d))
the_unity_wrt G is Element of d
p is Relation-like d -defined d -valued Function-like non empty V14(d) V25(d,d) Element of K19(K20(d,d))
p . (the_unity_wrt G) is Element of d
e is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
G $$ (F,e) is Element of d
p . (G $$ (F,e)) is Element of d
p * e is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
G $$ (F,(p * e)) is Element of d
D is non empty set
Fin D is non empty cup-closed diff-closed preBoolean set
d is non empty set
K20(d,d) is Relation-like set
K20(K20(d,d),d) is Relation-like set
K19(K20(K20(d,d),d)) is cup-closed diff-closed preBoolean set
K20(D,d) is Relation-like set
K19(K20(D,d)) is cup-closed diff-closed preBoolean set
id d is Relation-like d -defined d -valued Function-like one-to-one non empty V14(d) V25(d,d) Element of K19(K20(d,d))
K19(K20(d,d)) is cup-closed diff-closed preBoolean set
F is V43() Element of Fin D
G is Element of d
p is Relation-like K20(d,d) -defined d -valued Function-like V14(K20(d,d)) V25(K20(d,d),d) Element of K19(K20(K20(d,d),d))
e is Relation-like K20(d,d) -defined d -valued Function-like V14(K20(d,d)) V25(K20(d,d),d) Element of K19(K20(K20(d,d),d))
e [;] (G,(id d)) is Relation-like d -defined d -valued Function-like non empty V14(d) V25(d,d) Element of K19(K20(d,d))
e is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
p $$ (F,e) is Element of d
(e [;] (G,(id d))) . (p $$ (F,e)) is Element of d
(e [;] (G,(id d))) * e is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
p $$ (F,((e [;] (G,(id d))) * e)) is Element of d
the_unity_wrt p is Element of d
c is Element of d
s9 is Element of d
p . (c,s9) is Element of d
[c,s9] is set
p . [c,s9] is set
(e [;] (G,(id d))) . (p . (c,s9)) is Element of d
(e [;] (G,(id d))) . c is Element of d
(e [;] (G,(id d))) . s9 is Element of d
p . (((e [;] (G,(id d))) . c),((e [;] (G,(id d))) . s9)) is Element of d
[((e [;] (G,(id d))) . c),((e [;] (G,(id d))) . s9)] is set
p . [((e [;] (G,(id d))) . c),((e [;] (G,(id d))) . s9)] is set
(e [;] (G,(id d))) . (the_unity_wrt p) is Element of d
D is non empty set
Fin D is non empty cup-closed diff-closed preBoolean set
d is non empty set
K20(d,d) is Relation-like set
K20(K20(d,d),d) is Relation-like set
K19(K20(K20(d,d),d)) is cup-closed diff-closed preBoolean set
K20(D,d) is Relation-like set
K19(K20(D,d)) is cup-closed diff-closed preBoolean set
F is V43() Element of Fin D
G is Relation-like K20(d,d) -defined d -valued Function-like V14(K20(d,d)) V25(K20(d,d),d) Element of K19(K20(K20(d,d),d))
the_inverseOp_wrt G is Relation-like d -defined d -valued Function-like non empty V14(d) V25(d,d) Element of K19(K20(d,d))
K19(K20(d,d)) is cup-closed diff-closed preBoolean set
p is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
G $$ (F,p) is Element of d
(the_inverseOp_wrt G) . (G $$ (F,p)) is Element of d
(the_inverseOp_wrt G) * p is Relation-like D -defined d -valued Function-like non empty V14(D) V25(D,d) Element of K19(K20(D,d))
G $$ (F,((the_inverseOp_wrt G) * p)) is Element of d
the_unity_wrt G is Element of d
d is Element of d
u is Element of d
G . (d,u) is Element of d
[d,u] is set
G . [d,u] is set
(the_inverseOp_wrt G) . (G . (d,u)) is Element of d
(the_inverseOp_wrt G) . d is Element of d
(the_inverseOp_wrt G) . u is Element of d
G . (((the_inverseOp_wrt G) . d),((the_inverseOp_wrt G) . u)) is Element of d
[((the_inverseOp_wrt G) . d),((the_inverseOp_wrt G) . u)] is set
G . [((the_inverseOp_wrt G) . d),((the_inverseOp_wrt G) . u)] is set
(the_inverseOp_wrt G) . (the_unity_wrt G) is Element of d
D is non empty set
F is Element of D
NAT --> F is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V19() V25( NAT ,D) Element of K19(K20(NAT,D))
K20(NAT,D) is Relation-like V43() set
K19(K20(NAT,D)) is cup-closed diff-closed preBoolean V43() set
d is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
(NAT --> F) +* d is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
D is non empty set
d is Element of D
F is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() set
G is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
dom G is Element of K19(NAT)
(D,G,d) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
K20(NAT,D) is Relation-like V43() set
K19(K20(NAT,D)) is cup-closed diff-closed preBoolean V43() set
NAT --> d is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V19() V25( NAT ,D) Element of K19(K20(NAT,D))
(NAT --> d) +* G is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
(D,G,d) . F is set
G . F is set
(NAT --> d) . F is set
D is non empty set
d is Element of D
F is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
(D,F,d) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
K20(NAT,D) is Relation-like V43() set
K19(K20(NAT,D)) is cup-closed diff-closed preBoolean V43() set
NAT --> d is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V19() V25( NAT ,D) Element of K19(K20(NAT,D))
(NAT --> d) +* F is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
dom F is Element of K19(NAT)
(D,F,d) | (dom F) is Relation-like NAT -defined dom F -defined NAT -defined D -valued Function-like Element of K19(K20(NAT,D))
len F is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
Seg (len F) is V43() V50( len F) Element of K19(NAT)
dom (D,F,d) is non empty Element of K19(NAT)
(D,F,d) | (Seg (len F)) is Relation-like NAT -defined Seg (len F) -defined NAT -defined D -valued Function-like Element of K19(K20(NAT,D))
dom ((D,F,d) | (Seg (len F))) is Element of K19(NAT)
e is set
((D,F,d) | (Seg (len F))) . e is set
(D,F,d) . e is set
F . e is set
D is non empty set
d is Element of D
F is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
dom F is Element of K19(NAT)
G is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
F ^ G is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
(D,(F ^ G),d) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
K20(NAT,D) is Relation-like V43() set
K19(K20(NAT,D)) is cup-closed diff-closed preBoolean V43() set
NAT --> d is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V19() V25( NAT ,D) Element of K19(K20(NAT,D))
(NAT --> d) +* (F ^ G) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
(D,(F ^ G),d) | (dom F) is Relation-like NAT -defined dom F -defined NAT -defined D -valued Function-like Element of K19(K20(NAT,D))
len F is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
Seg (len F) is V43() V50( len F) Element of K19(NAT)
dom (D,(F ^ G),d) is non empty Element of K19(NAT)
(D,(F ^ G),d) | (Seg (len F)) is Relation-like NAT -defined Seg (len F) -defined NAT -defined D -valued Function-like Element of K19(K20(NAT,D))
dom ((D,(F ^ G),d) | (Seg (len F))) is Element of K19(NAT)
len G is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
(len F) + (len G) is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
len (F ^ G) is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
Seg (len (F ^ G)) is V43() V50( len (F ^ G)) Element of K19(NAT)
dom (F ^ G) is Element of K19(NAT)
e is set
((D,(F ^ G),d) | (Seg (len F))) . e is set
(D,(F ^ G),d) . e is set
(F ^ G) . e is set
F . e is set
D is non empty set
d is Element of D
{d} is non empty V12() V50(1) set
F is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
(D,F,d) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
K20(NAT,D) is Relation-like V43() set
K19(K20(NAT,D)) is cup-closed diff-closed preBoolean V43() set
NAT --> d is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V19() V25( NAT ,D) Element of K19(K20(NAT,D))
(NAT --> d) +* F is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
rng (D,F,d) is non empty set
rng F is set
(rng F) \/ {d} is non empty set
G is set
dom (D,F,d) is non empty Element of K19(NAT)
p is set
(D,F,d) . p is set
e is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
dom F is Element of K19(NAT)
F . e is set
e is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
dom F is Element of K19(NAT)
e is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
dom F is Element of K19(NAT)
e is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
dom F is Element of K19(NAT)
dom F is Element of K19(NAT)
p is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() set
F . p is set
(D,F,d) . p is set
dom F is Element of K19(NAT)
len F is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
Seg (len F) is V43() V50( len F) Element of K19(NAT)
(len F) + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V39() V40() V43() V48() Element of NAT
(D,F,d) . ((len F) + 1) is Element of D
D is non empty set
d is non empty set
K20(d,D) is Relation-like set
K19(K20(d,D)) is cup-closed diff-closed preBoolean set
F is Element of d
G is Relation-like d -defined D -valued Function-like non empty V14(d) V25(d,D) Element of K19(K20(d,D))
G . F is Element of D
p is Relation-like NAT -defined d -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of d
(d,p,F) is Relation-like NAT -defined d -valued Function-like non empty V14( NAT ) V25( NAT ,d) Element of K19(K20(NAT,d))
K20(NAT,d) is Relation-like V43() set
K19(K20(NAT,d)) is cup-closed diff-closed preBoolean V43() set
NAT --> F is Relation-like NAT -defined d -valued Function-like non empty V14( NAT ) V19() V25( NAT ,d) Element of K19(K20(NAT,d))
(NAT --> F) +* p is Relation-like NAT -defined d -valued Function-like non empty V14( NAT ) V25( NAT ,d) Element of K19(K20(NAT,d))
G * (d,p,F) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
K20(NAT,D) is Relation-like V43() set
K19(K20(NAT,D)) is cup-closed diff-closed preBoolean V43() set
G * p is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
(D,(G * p),(G . F)) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
NAT --> (G . F) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V19() V25( NAT ,D) Element of K19(K20(NAT,D))
(NAT --> (G . F)) +* (G * p) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
dom (G * p) is Element of K19(NAT)
len (G * p) is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
Seg (len (G * p)) is V43() V50( len (G * p)) Element of K19(NAT)
len p is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
Seg (len p) is V43() V50( len p) Element of K19(NAT)
dom p is Element of K19(NAT)
e is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
(d,p,F) . e is Element of d
G . ((d,p,F) . e) is Element of D
p . e is set
G . (p . e) is set
(G * p) . e is set
(D,(G * p),(G . F)) . e is Element of D
e is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
(d,p,F) . e is Element of d
G . ((d,p,F) . e) is Element of D
(D,(G * p),(G . F)) . e is Element of D
e is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
(d,p,F) . e is Element of d
G . ((d,p,F) . e) is Element of D
(D,(G * p),(G . F)) . e is Element of D
e is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
(d,p,F) . e is Element of d
G . ((d,p,F) . e) is Element of D
(D,(G * p),(G . F)) . e is Element of D
(G * (d,p,F)) . e is Element of D
D is non empty set
K20(D,D) is Relation-like set
K20(K20(D,D),D) is Relation-like set
K19(K20(K20(D,D),D)) is cup-closed diff-closed preBoolean set
d is Element of D
F is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
F . (d,d) is Element of D
[d,d] is set
F . [d,d] is set
G is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
len G is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
(D,G,d) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
K20(NAT,D) is Relation-like V43() set
K19(K20(NAT,D)) is cup-closed diff-closed preBoolean V43() set
NAT --> d is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V19() V25( NAT ,D) Element of K19(K20(NAT,D))
(NAT --> d) +* G is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
p is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
len p is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
(D,p,d) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
(NAT --> d) +* p is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
F .: ((D,G,d),(D,p,d)) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
F .: (G,p) is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
(D,(F .: (G,p)),d) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
(NAT --> d) +* (F .: (G,p)) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
len (F .: (G,p)) is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
dom (F .: (G,p)) is Element of K19(NAT)
Seg (len (F .: (G,p))) is V43() V50( len (F .: (G,p))) Element of K19(NAT)
dom G is Element of K19(NAT)
Seg (len G) is V43() V50( len G) Element of K19(NAT)
dom p is Element of K19(NAT)
Seg (len p) is V43() V50( len p) Element of K19(NAT)
e is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
(D,G,d) . e is Element of D
(D,p,d) . e is Element of D
F . (((D,G,d) . e),((D,p,d) . e)) is Element of D
[((D,G,d) . e),((D,p,d) . e)] is set
F . [((D,G,d) . e),((D,p,d) . e)] is set
G . e is set
F . ((G . e),((D,p,d) . e)) is set
[(G . e),((D,p,d) . e)] is set
F . [(G . e),((D,p,d) . e)] is set
p . e is set
F . ((G . e),(p . e)) is set
[(G . e),(p . e)] is set
F . [(G . e),(p . e)] is set
(F .: (G,p)) . e is set
(D,(F .: (G,p)),d) . e is Element of D
e is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
(D,G,d) . e is Element of D
(D,p,d) . e is Element of D
F . (((D,G,d) . e),((D,p,d) . e)) is Element of D
[((D,G,d) . e),((D,p,d) . e)] is set
F . [((D,G,d) . e),((D,p,d) . e)] is set
F . (d,((D,p,d) . e)) is Element of D
[d,((D,p,d) . e)] is set
F . [d,((D,p,d) . e)] is set
(D,(F .: (G,p)),d) . e is Element of D
e is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
(D,G,d) . e is Element of D
(D,p,d) . e is Element of D
F . (((D,G,d) . e),((D,p,d) . e)) is Element of D
[((D,G,d) . e),((D,p,d) . e)] is set
F . [((D,G,d) . e),((D,p,d) . e)] is set
(D,(F .: (G,p)),d) . e is Element of D
e is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
(D,G,d) . e is Element of D
(D,p,d) . e is Element of D
F . (((D,G,d) . e),((D,p,d) . e)) is Element of D
[((D,G,d) . e),((D,p,d) . e)] is set
F . [((D,G,d) . e),((D,p,d) . e)] is set
(D,(F .: (G,p)),d) . e is Element of D
(F .: ((D,G,d),(D,p,d))) . e is Element of D
D is non empty set
K20(D,D) is Relation-like set
K20(K20(D,D),D) is Relation-like set
K19(K20(K20(D,D),D)) is cup-closed diff-closed preBoolean set
d is Element of D
F is Element of D
G is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
G . (d,F) is Element of D
[d,F] is set
G . [d,F] is set
p is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
(D,p,d) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
K20(NAT,D) is Relation-like V43() set
K19(K20(NAT,D)) is cup-closed diff-closed preBoolean V43() set
NAT --> d is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V19() V25( NAT ,D) Element of K19(K20(NAT,D))
(NAT --> d) +* p is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
G [:] ((D,p,d),F) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
G [:] (p,F) is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
(D,(G [:] (p,F)),d) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
(NAT --> d) +* (G [:] (p,F)) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
dom p is Element of K19(NAT)
len p is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
Seg (len p) is V43() V50( len p) Element of K19(NAT)
len (G [:] (p,F)) is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
dom (G [:] (p,F)) is Element of K19(NAT)
Seg (len (G [:] (p,F))) is V43() V50( len (G [:] (p,F))) Element of K19(NAT)
e is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
(D,p,d) . e is Element of D
G . (((D,p,d) . e),F) is Element of D
[((D,p,d) . e),F] is set
G . [((D,p,d) . e),F] is set
p . e is set
G . ((p . e),F) is set
[(p . e),F] is set
G . [(p . e),F] is set
(G [:] (p,F)) . e is set
(D,(G [:] (p,F)),d) . e is Element of D
e is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
(D,p,d) . e is Element of D
G . (((D,p,d) . e),F) is Element of D
[((D,p,d) . e),F] is set
G . [((D,p,d) . e),F] is set
(D,(G [:] (p,F)),d) . e is Element of D
e is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
(D,p,d) . e is Element of D
G . (((D,p,d) . e),F) is Element of D
[((D,p,d) . e),F] is set
G . [((D,p,d) . e),F] is set
(D,(G [:] (p,F)),d) . e is Element of D
e is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
(D,p,d) . e is Element of D
G . (((D,p,d) . e),F) is Element of D
[((D,p,d) . e),F] is set
G . [((D,p,d) . e),F] is set
(D,(G [:] (p,F)),d) . e is Element of D
(G [:] ((D,p,d),F)) . e is Element of D
D is non empty set
K20(D,D) is Relation-like set
K20(K20(D,D),D) is Relation-like set
K19(K20(K20(D,D),D)) is cup-closed diff-closed preBoolean set
d is Element of D
F is Element of D
G is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
G . (d,F) is Element of D
[d,F] is set
G . [d,F] is set
p is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
(D,p,F) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
K20(NAT,D) is Relation-like V43() set
K19(K20(NAT,D)) is cup-closed diff-closed preBoolean V43() set
NAT --> F is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V19() V25( NAT ,D) Element of K19(K20(NAT,D))
(NAT --> F) +* p is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
G [;] (d,(D,p,F)) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
G [;] (d,p) is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
(D,(G [;] (d,p)),F) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
(NAT --> F) +* (G [;] (d,p)) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
dom p is Element of K19(NAT)
len p is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
Seg (len p) is V43() V50( len p) Element of K19(NAT)
len (G [;] (d,p)) is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
dom (G [;] (d,p)) is Element of K19(NAT)
Seg (len (G [;] (d,p))) is V43() V50( len (G [;] (d,p))) Element of K19(NAT)
e is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
(D,p,F) . e is Element of D
G . (d,((D,p,F) . e)) is Element of D
[d,((D,p,F) . e)] is set
G . [d,((D,p,F) . e)] is set
p . e is set
G . (d,(p . e)) is set
[d,(p . e)] is set
G . [d,(p . e)] is set
(G [;] (d,p)) . e is set
(D,(G [;] (d,p)),F) . e is Element of D
e is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
(D,p,F) . e is Element of D
G . (d,((D,p,F) . e)) is Element of D
[d,((D,p,F) . e)] is set
G . [d,((D,p,F) . e)] is set
(D,(G [;] (d,p)),F) . e is Element of D
e is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
(D,p,F) . e is Element of D
G . (d,((D,p,F) . e)) is Element of D
[d,((D,p,F) . e)] is set
G . [d,((D,p,F) . e)] is set
(D,(G [;] (d,p)),F) . e is Element of D
e is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
(D,p,F) . e is Element of D
G . (d,((D,p,F) . e)) is Element of D
[d,((D,p,F) . e)] is set
G . [d,((D,p,F) . e)] is set
(D,(G [;] (d,p)),F) . e is Element of D
(G [;] (d,(D,p,F))) . e is Element of D
D is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() set
Seg D is V43() V50(D) set
D is non empty set
K20(D,D) is Relation-like set
K20(K20(D,D),D) is Relation-like set
K19(K20(K20(D,D),D)) is cup-closed diff-closed preBoolean set
D is non empty set
K20(D,D) is Relation-like set
K20(K20(D,D),D) is Relation-like set
K19(K20(K20(D,D),D)) is cup-closed diff-closed preBoolean set
F is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
d is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
len d is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
F "**" d is Element of D
findom d is V43() Element of Fin NAT
the_unity_wrt F is Element of D
(D,d,(the_unity_wrt F)) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
K20(NAT,D) is Relation-like V43() set
K19(K20(NAT,D)) is cup-closed diff-closed preBoolean V43() set
NAT --> (the_unity_wrt F) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V19() V25( NAT ,D) Element of K19(K20(NAT,D))
(NAT --> (the_unity_wrt F)) +* d is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
F $$ ((findom d),(D,d,(the_unity_wrt F))) is Element of D
G is Element of D
p is Element of D
D is non empty set
K20(D,D) is Relation-like set
K20(K20(D,D),D) is Relation-like set
K19(K20(K20(D,D),D)) is cup-closed diff-closed preBoolean set
d is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
the_unity_wrt d is Element of D
F is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() set
F |-> (the_unity_wrt d) is Relation-like NAT -defined D -valued Function-like V43() V50(F) FinSequence-like FinSubsequence-like Element of F -tuples_on D
F -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
d "**" (F |-> (the_unity_wrt d)) is Element of D
p is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() set
p |-> (the_unity_wrt d) is Relation-like NAT -defined D -valued Function-like V43() V50(p) FinSequence-like FinSubsequence-like Element of p -tuples_on D
p -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
d "**" (p |-> (the_unity_wrt d)) is Element of D
p + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V39() V40() V43() V48() Element of NAT
(p + 1) |-> (the_unity_wrt d) is Relation-like NAT -defined D -valued Function-like V43() V50(p + 1) FinSequence-like FinSubsequence-like Element of (p + 1) -tuples_on D
(p + 1) -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
d "**" ((p + 1) |-> (the_unity_wrt d)) is Element of D
<*(the_unity_wrt d)*> is Relation-like NAT -defined D -valued Function-like constant non empty V12() V43() V50(1) FinSequence-like FinSubsequence-like FinSequence of D
(p |-> (the_unity_wrt d)) ^ <*(the_unity_wrt d)*> is Relation-like NAT -defined D -valued Function-like non empty V43() V50(p + 1) FinSequence-like FinSubsequence-like FinSequence of D
d "**" ((p |-> (the_unity_wrt d)) ^ <*(the_unity_wrt d)*>) is Element of D
d . ((d "**" (p |-> (the_unity_wrt d))),(the_unity_wrt d)) is Element of D
[(d "**" (p |-> (the_unity_wrt d))),(the_unity_wrt d)] is set
d . [(d "**" (p |-> (the_unity_wrt d))),(the_unity_wrt d)] is set
0 |-> (the_unity_wrt d) is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non negative V39() V40() V43() V48() V50( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered Element of 0 -tuples_on D
0 -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
d "**" (0 |-> (the_unity_wrt d)) is Element of D
<*> D is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non negative V39() V40() V43() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
d "**" (<*> D) is Element of D
D is non empty set
K20(D,D) is Relation-like set
K20(K20(D,D),D) is Relation-like set
K19(K20(K20(D,D),D)) is cup-closed diff-closed preBoolean set
d is Element of D
F is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
G is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() set
G |-> d is Relation-like NAT -defined D -valued Function-like V43() V50(G) FinSequence-like FinSubsequence-like Element of G -tuples_on D
G -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
F "**" (G |-> d) is Element of D
p is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() set
G + p is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() set
(G + p) |-> d is Relation-like NAT -defined D -valued Function-like V43() V50(G + p) FinSequence-like FinSubsequence-like Element of (G + p) -tuples_on D
(G + p) -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
F "**" ((G + p) |-> d) is Element of D
p |-> d is Relation-like NAT -defined D -valued Function-like V43() V50(p) FinSequence-like FinSubsequence-like Element of p -tuples_on D
p -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
F "**" (p |-> d) is Element of D
F . ((F "**" (G |-> d)),(F "**" (p |-> d))) is Element of D
[(F "**" (G |-> d)),(F "**" (p |-> d))] is set
F . [(F "**" (G |-> d)),(F "**" (p |-> d))] is set
len (G |-> d) is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
len (p |-> d) is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
(G |-> d) ^ (p |-> d) is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
F "**" ((G |-> d) ^ (p |-> d)) is Element of D
D is non empty set
K20(D,D) is Relation-like set
K20(K20(D,D),D) is Relation-like set
K19(K20(K20(D,D),D)) is cup-closed diff-closed preBoolean set
d is Element of D
F is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
G is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() set
G |-> d is Relation-like NAT -defined D -valued Function-like V43() V50(G) FinSequence-like FinSubsequence-like Element of G -tuples_on D
G -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
F "**" (G |-> d) is Element of D
p is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() set
G * p is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() set
(G * p) |-> d is Relation-like NAT -defined D -valued Function-like V43() V50(G * p) FinSequence-like FinSubsequence-like Element of (G * p) -tuples_on D
(G * p) -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
F "**" ((G * p) |-> d) is Element of D
p |-> (F "**" (G |-> d)) is Relation-like NAT -defined D -valued Function-like V43() V50(p) FinSequence-like FinSubsequence-like Element of p -tuples_on D
p -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
F "**" (p |-> (F "**" (G |-> d))) is Element of D
the_unity_wrt F is Element of D
<*> D is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non negative V39() V40() V43() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
<*> D is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non negative V39() V40() V43() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
<*> D is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non negative V39() V40() V43() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
e is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() set
G * e is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() set
(G * e) |-> d is Relation-like NAT -defined D -valued Function-like V43() V50(G * e) FinSequence-like FinSubsequence-like Element of (G * e) -tuples_on D
(G * e) -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
F "**" ((G * e) |-> d) is Element of D
e |-> (F "**" (G |-> d)) is Relation-like NAT -defined D -valued Function-like V43() V50(e) FinSequence-like FinSubsequence-like Element of e -tuples_on D
e -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
F "**" (e |-> (F "**" (G |-> d))) is Element of D
e + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V39() V40() V43() V48() Element of NAT
G * (e + 1) is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() set
(G * (e + 1)) |-> d is Relation-like NAT -defined D -valued Function-like V43() V50(G * (e + 1)) FinSequence-like FinSubsequence-like Element of (G * (e + 1)) -tuples_on D
(G * (e + 1)) -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
F "**" ((G * (e + 1)) |-> d) is Element of D
(e + 1) |-> (F "**" (G |-> d)) is Relation-like NAT -defined D -valued Function-like V43() V50(e + 1) FinSequence-like FinSubsequence-like Element of (e + 1) -tuples_on D
(e + 1) -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
F "**" ((e + 1) |-> (F "**" (G |-> d))) is Element of D
1 |-> (F "**" (G |-> d)) is Relation-like NAT -defined D -valued Function-like constant non empty V12() V43() V50(1) FinSequence-like FinSubsequence-like Element of 1 -tuples_on D
1 -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
<*(F "**" (G |-> d))*> is Relation-like NAT -defined D -valued Function-like constant non empty V12() V43() V50(1) FinSequence-like FinSubsequence-like FinSequence of D
1 + 0 is non empty V15() V16() V17() V21() ext-real positive non negative V39() V40() V43() V48() Element of NAT
G * 0 is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
G * (e + 1) is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
(G * (e + 1)) |-> d is Relation-like NAT -defined D -valued Function-like V43() V50(G * (e + 1)) FinSequence-like FinSubsequence-like Element of (G * (e + 1)) -tuples_on D
(G * (e + 1)) -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
F "**" ((G * (e + 1)) |-> d) is Element of D
G * 1 is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
(G * e) + (G * 1) is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
((G * e) + (G * 1)) |-> d is Relation-like NAT -defined D -valued Function-like V43() V50((G * e) + (G * 1)) FinSequence-like FinSubsequence-like Element of ((G * e) + (G * 1)) -tuples_on D
((G * e) + (G * 1)) -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
F "**" (((G * e) + (G * 1)) |-> d) is Element of D
F . ((F "**" ((G * e) |-> d)),(F "**" (G |-> d))) is Element of D
[(F "**" ((G * e) |-> d)),(F "**" (G |-> d))] is set
F . [(F "**" ((G * e) |-> d)),(F "**" (G |-> d))] is set
1 |-> (F "**" (G |-> d)) is Relation-like NAT -defined D -valued Function-like constant non empty V12() V43() V50(1) FinSequence-like FinSubsequence-like Element of 1 -tuples_on D
1 -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
F "**" (1 |-> (F "**" (G |-> d))) is Element of D
F . ((F "**" ((G * e) |-> d)),(F "**" (1 |-> (F "**" (G |-> d))))) is Element of D
[(F "**" ((G * e) |-> d)),(F "**" (1 |-> (F "**" (G |-> d))))] is set
F . [(F "**" ((G * e) |-> d)),(F "**" (1 |-> (F "**" (G |-> d))))] is set
1 + 0 is non empty V15() V16() V17() V21() ext-real positive non negative V39() V40() V43() V48() Element of NAT
G * 0 is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() set
(G * 0) |-> d is Relation-like NAT -defined D -valued Function-like V43() V50(G * 0) FinSequence-like FinSubsequence-like Element of (G * 0) -tuples_on D
(G * 0) -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
F "**" ((G * 0) |-> d) is Element of D
0 |-> (F "**" (G |-> d)) is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non negative V39() V40() V43() V48() V50( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered Element of 0 -tuples_on D
0 -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
F "**" (0 |-> (F "**" (G |-> d))) is Element of D
D is non empty set
K20(D,D) is Relation-like set
K20(K20(D,D),D) is Relation-like set
K19(K20(K20(D,D),D)) is cup-closed diff-closed preBoolean set
d is non empty set
K20(d,d) is Relation-like set
K20(K20(d,d),d) is Relation-like set
K19(K20(K20(d,d),d)) is cup-closed diff-closed preBoolean set
K20(d,D) is Relation-like set
K19(K20(d,D)) is cup-closed diff-closed preBoolean set
F is Relation-like K20(d,d) -defined d -valued Function-like V14(K20(d,d)) V25(K20(d,d),d) Element of K19(K20(K20(d,d),d))
the_unity_wrt F is Element of d
G is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
the_unity_wrt G is Element of D
p is Relation-like d -defined D -valued Function-like non empty V14(d) V25(d,D) Element of K19(K20(d,D))
p . (the_unity_wrt F) is Element of D
e is Relation-like NAT -defined d -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of d
F "**" e is Element of d
p . (F "**" e) is Element of D
p * e is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
G "**" (p * e) is Element of D
e is Relation-like NAT -defined d -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of d
F "**" e is Element of d
p . (F "**" e) is Element of D
p * e is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
G "**" (p * e) is Element of D
d is Element of d
<*d*> is Relation-like NAT -defined d -valued Function-like constant non empty V12() V43() V50(1) FinSequence-like FinSubsequence-like FinSequence of d
e ^ <*d*> is Relation-like NAT -defined d -valued Function-like non empty V43() FinSequence-like FinSubsequence-like FinSequence of d
F "**" (e ^ <*d*>) is Element of d
p . (F "**" (e ^ <*d*>)) is Element of D
p * (e ^ <*d*>) is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
G "**" (p * (e ^ <*d*>)) is Element of D
F . ((F "**" e),d) is Element of d
[(F "**" e),d] is set
F . [(F "**" e),d] is set
p . (F . ((F "**" e),d)) is Element of D
p . d is Element of D
G . ((G "**" (p * e)),(p . d)) is Element of D
[(G "**" (p * e)),(p . d)] is set
G . [(G "**" (p * e)),(p . d)] is set
<*(p . d)*> is Relation-like NAT -defined D -valued Function-like constant non empty V12() V43() V50(1) FinSequence-like FinSubsequence-like FinSequence of D
(p * e) ^ <*(p . d)*> is Relation-like NAT -defined D -valued Function-like non empty V43() FinSequence-like FinSubsequence-like FinSequence of D
G "**" ((p * e) ^ <*(p . d)*>) is Element of D
<*> d is Relation-like non-empty empty-yielding NAT -defined d -valued Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non negative V39() V40() V43() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of d
F "**" (<*> d) is Element of d
p . (F "**" (<*> d)) is Element of D
<*> D is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non negative V39() V40() V43() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
G "**" (<*> D) is Element of D
p * (<*> d) is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non negative V39() V40() V43() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
G "**" (p * (<*> d)) is Element of D
D is non empty set
K20(D,D) is Relation-like set
K20(K20(D,D),D) is Relation-like set
K19(K20(K20(D,D),D)) is cup-closed diff-closed preBoolean set
K19(K20(D,D)) is cup-closed diff-closed preBoolean set
d is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
the_unity_wrt d is Element of D
F is Relation-like D -defined D -valued Function-like non empty V14(D) V25(D,D) Element of K19(K20(D,D))
F . (the_unity_wrt d) is Element of D
G is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
d "**" G is Element of D
F . (d "**" G) is Element of D
F * G is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
d "**" (F * G) is Element of D
D is non empty set
K20(D,D) is Relation-like set
K20(K20(D,D),D) is Relation-like set
K19(K20(K20(D,D),D)) is cup-closed diff-closed preBoolean set
id D is Relation-like D -defined D -valued Function-like one-to-one non empty V14(D) V25(D,D) Element of K19(K20(D,D))
K19(K20(D,D)) is cup-closed diff-closed preBoolean set
d is Element of D
F is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
G is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
G [;] (d,(id D)) is Relation-like D -defined D -valued Function-like non empty V14(D) V25(D,D) Element of K19(K20(D,D))
p is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
F "**" p is Element of D
(G [;] (d,(id D))) . (F "**" p) is Element of D
(G [;] (d,(id D))) * p is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
F "**" ((G [;] (d,(id D))) * p) is Element of D
the_unity_wrt F is Element of D
d is Element of D
u is Element of D
F . (d,u) is Element of D
[d,u] is set
F . [d,u] is set
(G [;] (d,(id D))) . (F . (d,u)) is Element of D
(G [;] (d,(id D))) . d is Element of D
(G [;] (d,(id D))) . u is Element of D
F . (((G [;] (d,(id D))) . d),((G [;] (d,(id D))) . u)) is Element of D
[((G [;] (d,(id D))) . d),((G [;] (d,(id D))) . u)] is set
F . [((G [;] (d,(id D))) . d),((G [;] (d,(id D))) . u)] is set
(G [;] (d,(id D))) . (the_unity_wrt F) is Element of D
D is non empty set
K20(D,D) is Relation-like set
K20(K20(D,D),D) is Relation-like set
K19(K20(K20(D,D),D)) is cup-closed diff-closed preBoolean set
d is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
the_inverseOp_wrt d is Relation-like D -defined D -valued Function-like non empty V14(D) V25(D,D) Element of K19(K20(D,D))
K19(K20(D,D)) is cup-closed diff-closed preBoolean set
F is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
d "**" F is Element of D
(the_inverseOp_wrt d) . (d "**" F) is Element of D
(the_inverseOp_wrt d) * F is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
d "**" ((the_inverseOp_wrt d) * F) is Element of D
the_unity_wrt d is Element of D
e is Element of D
e is Element of D
d . (e,e) is Element of D
[e,e] is set
d . [e,e] is set
(the_inverseOp_wrt d) . (d . (e,e)) is Element of D
(the_inverseOp_wrt d) . e is Element of D
(the_inverseOp_wrt d) . e is Element of D
d . (((the_inverseOp_wrt d) . e),((the_inverseOp_wrt d) . e)) is Element of D
[((the_inverseOp_wrt d) . e),((the_inverseOp_wrt d) . e)] is set
d . [((the_inverseOp_wrt d) . e),((the_inverseOp_wrt d) . e)] is set
(the_inverseOp_wrt d) . (the_unity_wrt d) is Element of D
D is non empty set
K20(D,D) is Relation-like set
K20(K20(D,D),D) is Relation-like set
K19(K20(K20(D,D),D)) is cup-closed diff-closed preBoolean set
d is Element of D
F is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
the_unity_wrt F is Element of D
G is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
G . (d,d) is Element of D
[d,d] is set
G . [d,d] is set
p is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
len p is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
F "**" p is Element of D
e is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
len e is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
F "**" e is Element of D
G . ((F "**" p),(F "**" e)) is Element of D
[(F "**" p),(F "**" e)] is set
G . [(F "**" p),(F "**" e)] is set
G .: (p,e) is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
F "**" (G .: (p,e)) is Element of D
len (G .: (p,e)) is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
dom (G .: (p,e)) is Element of K19(NAT)
Seg (len (G .: (p,e))) is V43() V50( len (G .: (p,e))) Element of K19(NAT)
dom e is Element of K19(NAT)
Seg (len e) is V43() V50( len e) Element of K19(NAT)
dom p is Element of K19(NAT)
Seg (len p) is V43() V50( len p) Element of K19(NAT)
findom p is V43() Element of Fin NAT
(D,p,d) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
K20(NAT,D) is Relation-like V43() set
K19(K20(NAT,D)) is cup-closed diff-closed preBoolean V43() set
NAT --> d is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V19() V25( NAT ,D) Element of K19(K20(NAT,D))
(NAT --> d) +* p is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
F $$ ((findom p),(D,p,d)) is Element of D
G . ((F $$ ((findom p),(D,p,d))),(F "**" e)) is Element of D
[(F $$ ((findom p),(D,p,d))),(F "**" e)] is set
G . [(F $$ ((findom p),(D,p,d))),(F "**" e)] is set
findom e is V43() Element of Fin NAT
(D,e,d) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
(NAT --> d) +* e is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
F $$ ((findom e),(D,e,d)) is Element of D
G . ((F $$ ((findom p),(D,p,d))),(F $$ ((findom e),(D,e,d)))) is Element of D
[(F $$ ((findom p),(D,p,d))),(F $$ ((findom e),(D,e,d)))] is set
G . [(F $$ ((findom p),(D,p,d))),(F $$ ((findom e),(D,e,d)))] is set
G .: ((D,p,d),(D,e,d)) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
F $$ ((findom p),(G .: ((D,p,d),(D,e,d)))) is Element of D
findom (G .: (p,e)) is V43() Element of Fin NAT
(D,(G .: (p,e)),d) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
(NAT --> d) +* (G .: (p,e)) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
F $$ ((findom (G .: (p,e))),(D,(G .: (p,e)),d)) is Element of D
D is non empty set
K20(D,D) is Relation-like set
K20(K20(D,D),D) is Relation-like set
K19(K20(K20(D,D),D)) is cup-closed diff-closed preBoolean set
d is Element of D
F is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
the_unity_wrt F is Element of D
G is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
G . (d,d) is Element of D
[d,d] is set
G . [d,d] is set
p is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() set
p -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
e is Relation-like NAT -defined D -valued Function-like V43() V50(p) FinSequence-like FinSubsequence-like Element of p -tuples_on D
F "**" e is Element of D
e is Relation-like NAT -defined D -valued Function-like V43() V50(p) FinSequence-like FinSubsequence-like Element of p -tuples_on D
F "**" e is Element of D
G . ((F "**" e),(F "**" e)) is Element of D
[(F "**" e),(F "**" e)] is set
G . [(F "**" e),(F "**" e)] is set
G .: (e,e) is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
F "**" (G .: (e,e)) is Element of D
len e is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
len e is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
D is non empty set
K20(D,D) is Relation-like set
K20(K20(D,D),D) is Relation-like set
K19(K20(K20(D,D),D)) is cup-closed diff-closed preBoolean set
d is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
F is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
len F is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
d "**" F is Element of D
G is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
len G is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
d "**" G is Element of D
d . ((d "**" F),(d "**" G)) is Element of D
[(d "**" F),(d "**" G)] is set
d . [(d "**" F),(d "**" G)] is set
d .: (F,G) is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
d "**" (d .: (F,G)) is Element of D
the_unity_wrt d is Element of D
d . ((the_unity_wrt d),(the_unity_wrt d)) is Element of D
[(the_unity_wrt d),(the_unity_wrt d)] is set
d . [(the_unity_wrt d),(the_unity_wrt d)] is set
e is Element of D
e is Element of D
d . (e,e) is Element of D
[e,e] is set
d . [e,e] is set
d is Element of D
u is Element of D
d . (d,u) is Element of D
[d,u] is set
d . [d,u] is set
d . ((d . (e,e)),(d . (d,u))) is Element of D
[(d . (e,e)),(d . (d,u))] is set
d . [(d . (e,e)),(d . (d,u))] is set
d . (e,d) is Element of D
[e,d] is set
d . [e,d] is set
d . (e,u) is Element of D
[e,u] is set
d . [e,u] is set
d . ((d . (e,d)),(d . (e,u))) is Element of D
[(d . (e,d)),(d . (e,u))] is set
d . [(d . (e,d)),(d . (e,u))] is set
D is non empty set
K20(D,D) is Relation-like set
K20(K20(D,D),D) is Relation-like set
K19(K20(K20(D,D),D)) is cup-closed diff-closed preBoolean set
d is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
F is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() set
F -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
G is Relation-like NAT -defined D -valued Function-like V43() V50(F) FinSequence-like FinSubsequence-like Element of F -tuples_on D
d "**" G is Element of D
p is Relation-like NAT -defined D -valued Function-like V43() V50(F) FinSequence-like FinSubsequence-like Element of F -tuples_on D
d "**" p is Element of D
d . ((d "**" G),(d "**" p)) is Element of D
[(d "**" G),(d "**" p)] is set
d . [(d "**" G),(d "**" p)] is set
d .: (G,p) is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
d "**" (d .: (G,p)) is Element of D
len G is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
len p is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
D is non empty set
K20(D,D) is Relation-like set
K20(K20(D,D),D) is Relation-like set
K19(K20(K20(D,D),D)) is cup-closed diff-closed preBoolean set
d is Element of D
F is Element of D
G is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
G . (d,F) is Element of D
[d,F] is set
G . [d,F] is set
p is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() set
p |-> (G . (d,F)) is Relation-like NAT -defined D -valued Function-like V43() V50(p) FinSequence-like FinSubsequence-like Element of p -tuples_on D
p -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
G "**" (p |-> (G . (d,F))) is Element of D
p |-> d is Relation-like NAT -defined D -valued Function-like V43() V50(p) FinSequence-like FinSubsequence-like Element of p -tuples_on D
G "**" (p |-> d) is Element of D
p |-> F is Relation-like NAT -defined D -valued Function-like V43() V50(p) FinSequence-like FinSubsequence-like Element of p -tuples_on D
G "**" (p |-> F) is Element of D
G . ((G "**" (p |-> d)),(G "**" (p |-> F))) is Element of D
[(G "**" (p |-> d)),(G "**" (p |-> F))] is set
G . [(G "**" (p |-> d)),(G "**" (p |-> F))] is set
e is Relation-like NAT -defined D -valued Function-like V43() V50(p) FinSequence-like FinSubsequence-like Element of p -tuples_on D
e is Relation-like NAT -defined D -valued Function-like V43() V50(p) FinSequence-like FinSubsequence-like Element of p -tuples_on D
G .: (e,e) is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
K20(D,D) is Relation-like set
K20(K20(D,D),D) is Relation-like set
K19(K20(K20(D,D),D)) is cup-closed diff-closed preBoolean set
id D is Relation-like D -defined D -valued Function-like one-to-one non empty V14(D) V25(D,D) Element of K19(K20(D,D))
K19(K20(D,D)) is cup-closed diff-closed preBoolean set
d is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
the_inverseOp_wrt d is Relation-like D -defined D -valued Function-like non empty V14(D) V25(D,D) Element of K19(K20(D,D))
d * ((id D),(the_inverseOp_wrt d)) is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
F is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
G is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() set
G -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
p is Relation-like NAT -defined D -valued Function-like V43() V50(G) FinSequence-like FinSubsequence-like Element of G -tuples_on D
d "**" p is Element of D
e is Relation-like NAT -defined D -valued Function-like V43() V50(G) FinSequence-like FinSubsequence-like Element of G -tuples_on D
d "**" e is Element of D
F . ((d "**" p),(d "**" e)) is Element of D
[(d "**" p),(d "**" e)] is set
F . [(d "**" p),(d "**" e)] is set
F .: (p,e) is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
d "**" (F .: (p,e)) is Element of D
the_unity_wrt d is Element of D
F . ((the_unity_wrt d),(the_unity_wrt d)) is Element of D
[(the_unity_wrt d),(the_unity_wrt d)] is set
F . [(the_unity_wrt d),(the_unity_wrt d)] is set
d is Element of D
u is Element of D
F . (d,u) is Element of D
[d,u] is set
F . [d,u] is set
c is Element of D
s9 is Element of D
F . (c,s9) is Element of D
[c,s9] is set
F . [c,s9] is set
d . ((F . (d,u)),(F . (c,s9))) is Element of D
[(F . (d,u)),(F . (c,s9))] is set
d . [(F . (d,u)),(F . (c,s9))] is set
d . (d,c) is Element of D
[d,c] is set
d . [d,c] is set
d . (u,s9) is Element of D
[u,s9] is set
d . [u,s9] is set
F . ((d . (d,c)),(d . (u,s9))) is Element of D
[(d . (d,c)),(d . (u,s9))] is set
F . [(d . (d,c)),(d . (u,s9))] is set
D is non empty set
K20(D,D) is Relation-like set
K20(K20(D,D),D) is Relation-like set
K19(K20(K20(D,D),D)) is cup-closed diff-closed preBoolean set
d is Element of D
F is Element of D
G is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
the_unity_wrt G is Element of D
p is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
p . (F,d) is Element of D
[F,d] is set
p . [F,d] is set
e is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
G "**" e is Element of D
p . (F,(G "**" e)) is Element of D
[F,(G "**" e)] is set
p . [F,(G "**" e)] is set
p [;] (F,e) is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
G "**" (p [;] (F,e)) is Element of D
len e is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
len (p [;] (F,e)) is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
Seg (len e) is V43() V50( len e) Element of K19(NAT)
dom e is Element of K19(NAT)
Seg (len (p [;] (F,e))) is V43() V50( len (p [;] (F,e))) Element of K19(NAT)
dom (p [;] (F,e)) is Element of K19(NAT)
findom e is V43() Element of Fin NAT
(D,e,d) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
K20(NAT,D) is Relation-like V43() set
K19(K20(NAT,D)) is cup-closed diff-closed preBoolean V43() set
NAT --> d is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V19() V25( NAT ,D) Element of K19(K20(NAT,D))
(NAT --> d) +* e is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
G $$ ((findom e),(D,e,d)) is Element of D
p . (F,(G $$ ((findom e),(D,e,d)))) is Element of D
[F,(G $$ ((findom e),(D,e,d)))] is set
p . [F,(G $$ ((findom e),(D,e,d)))] is set
p [;] (F,(D,e,d)) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
G $$ ((findom e),(p [;] (F,(D,e,d)))) is Element of D
(D,(p [;] (F,e)),d) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
(NAT --> d) +* (p [;] (F,e)) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
G $$ ((findom e),(D,(p [;] (F,e)),d)) is Element of D
D is non empty set
K20(D,D) is Relation-like set
K20(K20(D,D),D) is Relation-like set
K19(K20(K20(D,D),D)) is cup-closed diff-closed preBoolean set
d is Element of D
F is Element of D
G is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
the_unity_wrt G is Element of D
p is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
p . (d,F) is Element of D
[d,F] is set
p . [d,F] is set
e is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
G "**" e is Element of D
p . ((G "**" e),F) is Element of D
[(G "**" e),F] is set
p . [(G "**" e),F] is set
p [:] (e,F) is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
G "**" (p [:] (e,F)) is Element of D
len e is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
len (p [:] (e,F)) is V15() V16() V17() V21() ext-real non negative V39() V40() V43() V48() Element of NAT
Seg (len e) is V43() V50( len e) Element of K19(NAT)
dom e is Element of K19(NAT)
Seg (len (p [:] (e,F))) is V43() V50( len (p [:] (e,F))) Element of K19(NAT)
dom (p [:] (e,F)) is Element of K19(NAT)
findom e is V43() Element of Fin NAT
(D,e,d) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
K20(NAT,D) is Relation-like V43() set
K19(K20(NAT,D)) is cup-closed diff-closed preBoolean V43() set
NAT --> d is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V19() V25( NAT ,D) Element of K19(K20(NAT,D))
(NAT --> d) +* e is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
G $$ ((findom e),(D,e,d)) is Element of D
p . ((G $$ ((findom e),(D,e,d))),F) is Element of D
[(G $$ ((findom e),(D,e,d))),F] is set
p . [(G $$ ((findom e),(D,e,d))),F] is set
p [:] ((D,e,d),F) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
G $$ ((findom e),(p [:] ((D,e,d),F))) is Element of D
(D,(p [:] (e,F)),d) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
(NAT --> d) +* (p [:] (e,F)) is Relation-like NAT -defined D -valued Function-like non empty V14( NAT ) V25( NAT ,D) Element of K19(K20(NAT,D))
G $$ ((findom e),(D,(p [:] (e,F)),d)) is Element of D
D is non empty set
K20(D,D) is Relation-like set
K20(K20(D,D),D) is Relation-like set
K19(K20(K20(D,D),D)) is cup-closed diff-closed preBoolean set
d is Element of D
F is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
G is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
p is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
F "**" p is Element of D
G . (d,(F "**" p)) is Element of D
[d,(F "**" p)] is set
G . [d,(F "**" p)] is set
G [;] (d,p) is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
F "**" (G [;] (d,p)) is Element of D
the_unity_wrt F is Element of D
G . (d,(the_unity_wrt F)) is Element of D
[d,(the_unity_wrt F)] is set
G . [d,(the_unity_wrt F)] is set
D is non empty set
K20(D,D) is Relation-like set
K20(K20(D,D),D) is Relation-like set
K19(K20(K20(D,D),D)) is cup-closed diff-closed preBoolean set
d is Element of D
F is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
G is Relation-like K20(D,D) -defined D -valued Function-like V14(K20(D,D)) V25(K20(D,D),D) Element of K19(K20(K20(D,D),D))
p is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
F "**" p is Element of D
G . ((F "**" p),d) is Element of D
[(F "**" p),d] is set
G . [(F "**" p),d] is set
G [:] (p,d) is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D
F "**" (G [:] (p,d)) is Element of D
the_unity_wrt F is Element of D
G . ((the_unity_wrt F),d) is Element of D
[(the_unity_wrt F),d] is set
G . [(the_unity_wrt F),d] is set