:: 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 Re