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