:: FINSEQOP semantic presentation

K151() is set
K155() is non empty V31() V32() V33() V42() V47() V48() Element of bool K151()
bool K151() is non empty set
{} is Relation-like non-empty empty-yielding K155() -defined Function-like one-to-one constant functional empty Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set
1 is non empty V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
{{},1} is non empty set
K150() is non empty V31() V32() V33() V42() V47() V48() set
bool K150() is non empty V42() set
bool K155() is non empty V42() set
0 is Relation-like non-empty empty-yielding K155() -defined Function-like one-to-one constant functional empty Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of K155()
2 is non empty V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
3 is non empty V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
D is Relation-like Function-like set
<:{},D:> is Relation-like Function-like set
<:D,{}:> is Relation-like Function-like set
dom <:{},D:> is set
dom {} is Relation-like non-empty empty-yielding K155() -defined Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of bool K155()
dom D is set
(dom {}) /\ (dom D) is Relation-like Element of bool K155()
dom <:D,{}:> is set
(dom D) /\ (dom {}) is Relation-like Element of bool K155()
D is Relation-like Function-like set
[:{},D:] is Relation-like Function-like set
[:D,{}:] is Relation-like Function-like set
dom [:{},D:] is set
dom {} is Relation-like non-empty empty-yielding K155() -defined Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of bool K155()
dom D is set
[:(dom {}),(dom D):] is Relation-like set
dom [:D,{}:] is set
[:(dom D),(dom {}):] is Relation-like set
D is Relation-like Function-like set
F is Relation-like Function-like set
D .: ({},F) is Relation-like Function-like set
<:{},F:> is Relation-like Function-like set
<:{},F:> * D is Relation-like Function-like set
D .: (F,{}) is Relation-like Function-like set
<:F,{}:> is Relation-like Function-like set
<:F,{}:> * D is Relation-like Function-like set
{} * D is Relation-like non-empty empty-yielding K155() -defined Function-like one-to-one constant functional empty Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set
D is set
F is Relation-like Function-like set
F [:] ({},D) is Relation-like Function-like set
dom {} is Relation-like non-empty empty-yielding K155() -defined Function-like one-to-one constant functional empty Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set
(dom {}) --> D is Relation-like non-empty empty-yielding dom {} -defined Function-like one-to-one constant functional empty total Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set
{D} is non empty trivial V49(1) set
[:(dom {}),{D}:] is Relation-like set
<:{},((dom {}) --> D):> is Relation-like Function-like set
<:{},((dom {}) --> D):> * F is Relation-like Function-like set
dom {} is Relation-like non-empty empty-yielding K155() -defined Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of bool K155()
(dom {}) --> D is Relation-like non-empty empty-yielding dom {} -defined {D} -valued Function-like one-to-one constant functional empty total V18( dom {},{D}) Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of bool [:(dom {}),{D}:]
[:(dom {}),{D}:] is Relation-like set
bool [:(dom {}),{D}:] is non empty set
F .: ({},((dom {}) --> D)) is Relation-like Function-like set
<:{},((dom {}) --> D):> is Relation-like Function-like set
<:{},((dom {}) --> D):> * F is Relation-like Function-like set
D is set
F is Relation-like Function-like set
F [;] (D,{}) is Relation-like Function-like set
dom {} is Relation-like non-empty empty-yielding K155() -defined Function-like one-to-one constant functional empty Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set
(dom {}) --> D is Relation-like non-empty empty-yielding dom {} -defined Function-like one-to-one constant functional empty total Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set
{D} is non empty trivial V49(1) set
[:(dom {}),{D}:] is Relation-like set
<:((dom {}) --> D),{}:> is Relation-like Function-like set
<:((dom {}) --> D),{}:> * F is Relation-like Function-like set
dom {} is Relation-like non-empty empty-yielding K155() -defined Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of bool K155()
(dom {}) --> D is Relation-like non-empty empty-yielding dom {} -defined {D} -valued Function-like one-to-one constant functional empty total V18( dom {},{D}) Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of bool [:(dom {}),{D}:]
[:(dom {}),{D}:] is Relation-like set
bool [:(dom {}),{D}:] is non empty set
F .: (((dom {}) --> D),{}) is Relation-like Function-like set
<:((dom {}) --> D),{}:> is Relation-like Function-like set
<:((dom {}) --> D),{}:> * F is Relation-like Function-like set
D is set
F is set
{F} is non empty trivial V49(1) set
G is set
{G} is non empty trivial V49(1) set
[:{F},{G}:] is Relation-like non empty set
[F,G] is set
{[F,G]} is Relation-like Function-like constant non empty trivial V49(1) set
D --> F is Relation-like D -defined {F} -valued Function-like constant total V18(D,{F}) Element of bool [:D,{F}:]
[:D,{F}:] is Relation-like set
bool [:D,{F}:] is non empty set
D --> G is Relation-like D -defined {G} -valued Function-like constant total V18(D,{G}) Element of bool [:D,{G}:]
[:D,{G}:] is Relation-like set
bool [:D,{G}:] is non empty set
<:(D --> F),(D --> G):> is Relation-like D -defined [:{F},{G}:] -valued Function-like total V18(D,[:{F},{G}:]) Element of bool [:D,[:{F},{G}:]:]
[:D,[:{F},{G}:]:] is Relation-like set
bool [:D,[:{F},{G}:]:] is non empty set
D --> [F,G] is Relation-like D -defined {[F,G]} -valued Function-like constant total V18(D,{[F,G]}) Element of bool [:D,{[F,G]}:]
[:D,{[F,G]}:] is Relation-like set
bool [:D,{[F,G]}:] is non empty set
rng <:(D --> F),(D --> G):> is Relation-like {F} -defined {G} -valued Element of bool [:{F},{G}:]
bool [:{F},{G}:] is non empty set
the Element of D is Element of D
dom (D --> F) is Element of bool D
bool D is non empty set
dom (D --> G) is Element of bool D
dom <:(D --> F),(D --> G):> is Element of bool D
(D --> F) . the Element of D is set
(D --> G) . the Element of D is set
<:(D --> F),(D --> G):> . the Element of D is set
D is Relation-like Function-like set
dom D is set
F is set
G is set
u is set
[G,u] is set
F --> G is Relation-like F -defined {G} -valued Function-like constant total V18(F,{G}) Element of bool [:F,{G}:]
{G} is non empty trivial V49(1) set
[:F,{G}:] is Relation-like set
bool [:F,{G}:] is non empty set
F --> u is Relation-like F -defined {u} -valued Function-like constant total V18(F,{u}) Element of bool [:F,{u}:]
{u} is non empty trivial V49(1) set
[:F,{u}:] is Relation-like set
bool [:F,{u}:] is non empty set
D .: ((F --> G),(F --> u)) is Relation-like Function-like set
<:(F --> G),(F --> u):> is Relation-like Function-like set
<:(F --> G),(F --> u):> * D is Relation-like Function-like set
D . (G,u) is set
D . [G,u] is set
F --> (D . (G,u)) is Relation-like F -defined {(D . (G,u))} -valued Function-like constant total V18(F,{(D . (G,u))}) Element of bool [:F,{(D . (G,u))}:]
{(D . (G,u))} is non empty trivial V49(1) set
[:F,{(D . (G,u))}:] is Relation-like set
bool [:F,{(D . (G,u))}:] is non empty set
F --> [G,u] is Relation-like F -defined {[G,u]} -valued Function-like constant total V18(F,{[G,u]}) Element of bool [:F,{[G,u]}:]
{[G,u]} is Relation-like Function-like constant non empty trivial V49(1) set
[:F,{[G,u]}:] is Relation-like set
bool [:F,{[G,u]}:] is non empty set
(F --> [G,u]) * D is Relation-like F -defined Function-like set
D is non empty set
F is non empty set
[:D,F:] is Relation-like non empty set
G is non empty set
[:[:D,F:],G:] is Relation-like non empty set
bool [:[:D,F:],G:] is non empty set
u is Relation-like [:D,F:] -defined G -valued Function-like non empty total V18([:D,F:],G) Element of bool [:[:D,F:],G:]
d1 is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
d2 is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
u .: (d1,d2) is Relation-like Function-like set
<:d1,d2:> is Relation-like Function-like set
<:d1,d2:> * u is Relation-like G -valued Function-like set
D is non empty set
F is non empty set
[:D,F:] is Relation-like non empty set
G is non empty set
[:[:D,F:],G:] is Relation-like non empty set
bool [:[:D,F:],G:] is non empty set
u is Relation-like [:D,F:] -defined G -valued Function-like non empty total V18([:D,F:],G) Element of bool [:[:D,F:],G:]
d1 is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
d2 is Element of F
u [:] (d1,d2) is Relation-like Function-like set
dom d1 is set
(dom d1) --> d2 is Relation-like dom d1 -defined F -valued Function-like constant total set
{d2} is non empty trivial V49(1) set
[:(dom d1),{d2}:] is Relation-like set
<:d1,((dom d1) --> d2):> is Relation-like Function-like set
<:d1,((dom d1) --> d2):> * u is Relation-like G -valued Function-like set
D is non empty set
F is non empty set
[:D,F:] is Relation-like non empty set
G is non empty set
[:[:D,F:],G:] is Relation-like non empty set
bool [:[:D,F:],G:] is non empty set
u is Relation-like [:D,F:] -defined G -valued Function-like non empty total V18([:D,F:],G) Element of bool [:[:D,F:],G:]
d1 is Element of D
d2 is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
u [;] (d1,d2) is Relation-like Function-like set
dom d2 is set
(dom d2) --> d1 is Relation-like dom d2 -defined D -valued Function-like constant total set
{d1} is non empty trivial V49(1) set
[:(dom d2),{d1}:] is Relation-like set
<:((dom d2) --> d1),d2:> is Relation-like Function-like set
<:((dom d2) --> d1),d2:> * u is Relation-like G -valued Function-like set
D is set
F is set
[:D,F:] is Relation-like set
bool [:D,F:] is non empty set
G is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
u is Relation-like D -defined F -valued Function-like V18(D,F) Element of bool [:D,F:]
G * u is Relation-like K155() -defined F -valued Function-like set
D is non empty set
F is non empty set
[:D,F:] is Relation-like non empty set
bool [:D,F:] is non empty set
G is Element of D
<*G*> is Relation-like K155() -defined D -valued Function-like constant non empty trivial V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of D
u is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
u ^ <*G*> is Relation-like K155() -defined D -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of D
d1 is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
(D,F,(u ^ <*G*>),d1) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
(D,F,u,d1) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
d1 . G is Element of F
<*(d1 . G)*> is Relation-like K155() -defined F -valued Function-like constant non empty trivial V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of F
(D,F,u,d1) ^ <*(d1 . G)*> is Relation-like K155() -defined F -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of F
len u is V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
(len u) + 1 is non empty V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
len (D,F,(u ^ <*G*>),d1) is V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
len (u ^ <*G*>) is non empty V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
len (D,F,u,d1) is V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
dom (D,F,(u ^ <*G*>),d1) is Element of bool K155()
Seg ((len u) + 1) is non empty V42() V49((len u) + 1) Element of bool K155()
Seg (len u) is V42() V49( len u) Element of bool K155()
dom u is Element of bool K155()
Seg (len (D,F,u,d1)) is V42() V49( len (D,F,u,d1)) Element of bool K155()
dom (D,F,u,d1) is Element of bool K155()
f is V31() V32() V33() V37() V38() V41() V42() V47() set
(u ^ <*G*>) . f is set
d1 . ((u ^ <*G*>) . f) is set
u . f is set
d1 . (u . f) is set
(D,F,u,d1) . f is set
((D,F,u,d1) ^ <*(d1 . G)*>) . f is set
(u ^ <*G*>) . f is set
d1 . ((u ^ <*G*>) . f) is set
((D,F,u,d1) ^ <*(d1 . G)*>) . f is set
(u ^ <*G*>) . f is set
d1 . ((u ^ <*G*>) . f) is set
((D,F,u,d1) ^ <*(d1 . G)*>) . f is set
(u ^ <*G*>) . f is set
d1 . ((u ^ <*G*>) . f) is set
((D,F,u,d1) ^ <*(d1 . G)*>) . f is set
(D,F,(u ^ <*G*>),d1) . f is set
len ((D,F,u,d1) ^ <*(d1 . G)*>) is non empty V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
(len (D,F,u,d1)) + 1 is non empty V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
D is non empty set
F is non empty set
[:D,F:] is Relation-like non empty set
bool [:D,F:] is non empty set
G is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
u is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
G ^ u is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
d1 is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
(D,F,(G ^ u),d1) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
(D,F,G,d1) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
(D,F,u,d1) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
(D,F,G,d1) ^ (D,F,u,d1) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
d2 is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
G ^ d2 is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
(D,F,(G ^ d2),d1) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
(D,F,d2,d1) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
(D,F,G,d1) ^ (D,F,d2,d1) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
d3 is Element of D
<*d3*> is Relation-like K155() -defined D -valued Function-like constant non empty trivial V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of D
d2 ^ <*d3*> is Relation-like K155() -defined D -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of D
G ^ (d2 ^ <*d3*>) is Relation-like K155() -defined D -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of D
(D,F,(G ^ (d2 ^ <*d3*>)),d1) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
(D,F,(d2 ^ <*d3*>),d1) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
(D,F,G,d1) ^ (D,F,(d2 ^ <*d3*>),d1) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
(G ^ d2) ^ <*d3*> is Relation-like K155() -defined D -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of D
(D,F,((G ^ d2) ^ <*d3*>),d1) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
d1 . d3 is Element of F
<*(d1 . d3)*> is Relation-like K155() -defined F -valued Function-like constant non empty trivial V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of F
(D,F,(G ^ d2),d1) ^ <*(d1 . d3)*> is Relation-like K155() -defined F -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of F
(D,F,d2,d1) ^ <*(d1 . d3)*> is Relation-like K155() -defined F -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of F
(D,F,G,d1) ^ ((D,F,d2,d1) ^ <*(d1 . d3)*>) is Relation-like K155() -defined F -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of F
<*> D is Relation-like non-empty empty-yielding K155() -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
[:K155(),D:] is Relation-like non empty V42() set
G ^ (<*> D) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
(D,F,(G ^ (<*> D)),d1) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
(D,F,(<*> D),d1) is Relation-like non-empty empty-yielding K155() -defined F -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of F
[:K155(),F:] is Relation-like non empty V42() set
(D,F,G,d1) ^ (D,F,(<*> D),d1) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
D is non empty set
F is non empty set
[:F,D:] is Relation-like non empty set
[:K155(),F:] is Relation-like non empty V42() set
G is non empty set
[:[:F,D:],G:] is Relation-like non empty set
bool [:[:F,D:],G:] is non empty set
<*> G is Relation-like non-empty empty-yielding K155() -defined G -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of G
[:K155(),G:] is Relation-like non empty V42() set
u is V31() V32() V33() V37() V38() V41() V42() V47() set
d1 is Relation-like [:F,D:] -defined G -valued Function-like non empty total V18([:F,D:],G) Element of bool [:[:F,D:],G:]
d2 is Relation-like K155() -defined D -valued Function-like V42() V49(u) FinSequence-like FinSubsequence-like FinSequence of D
d3 is Relation-like non-empty empty-yielding K155() -defined F -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of F
(F,D,G,d1,d3,d2) is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of G
<:d3,d2:> is Relation-like Function-like set
<:d3,d2:> * d1 is Relation-like G -valued Function-like set
<*> F is Relation-like non-empty empty-yielding K155() -defined F -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of F
D is non empty set
F is non empty set
[:D,F:] is Relation-like non empty set
[:K155(),F:] is Relation-like non empty V42() set
G is non empty set
[:[:D,F:],G:] is Relation-like non empty set
bool [:[:D,F:],G:] is non empty set
<*> G is Relation-like non-empty empty-yielding K155() -defined G -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of G
[:K155(),G:] is Relation-like non empty V42() set
u is Element of D
d1 is Relation-like [:D,F:] -defined G -valued Function-like non empty total V18([:D,F:],G) Element of bool [:[:D,F:],G:]
d2 is Relation-like non-empty empty-yielding K155() -defined F -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of F
(D,F,G,d1,u,d2) is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of G
dom d2 is Relation-like non-empty empty-yielding K155() -defined Function-like one-to-one constant functional empty Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) V49( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered set
(dom d2) --> u is Relation-like non-empty empty-yielding dom d2 -defined D -valued Function-like one-to-one constant functional empty total Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set
{u} is non empty trivial V49(1) set
[:(dom d2),{u}:] is Relation-like set
<:((dom d2) --> u),d2:> is Relation-like Function-like set
<:((dom d2) --> u),d2:> * d1 is Relation-like G -valued Function-like set
<*> F is Relation-like non-empty empty-yielding K155() -defined F -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of F
D is non empty set
F is non empty set
[:F,D:] is Relation-like non empty set
[:K155(),F:] is Relation-like non empty V42() set
G is non empty set
[:[:F,D:],G:] is Relation-like non empty set
bool [:[:F,D:],G:] is non empty set
<*> G is Relation-like non-empty empty-yielding K155() -defined G -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of G
[:K155(),G:] is Relation-like non empty V42() set
u is Element of D
d1 is Relation-like [:F,D:] -defined G -valued Function-like non empty total V18([:F,D:],G) Element of bool [:[:F,D:],G:]
d2 is Relation-like non-empty empty-yielding K155() -defined F -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of F
(F,D,G,d1,d2,u) is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of G
dom d2 is Relation-like non-empty empty-yielding K155() -defined Function-like one-to-one constant functional empty Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) V49( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered set
(dom d2) --> u is Relation-like non-empty empty-yielding dom d2 -defined D -valued Function-like one-to-one constant functional empty total Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set
{u} is non empty trivial V49(1) set
[:(dom d2),{u}:] is Relation-like set
<:d2,((dom d2) --> u):> is Relation-like Function-like set
<:d2,((dom d2) --> u):> * d1 is Relation-like G -valued Function-like set
<*> F is Relation-like non-empty empty-yielding K155() -defined F -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of F
D is non empty set
F is non empty set
G is non empty set
[:F,G:] is Relation-like non empty set
[:[:F,G:],D:] is Relation-like non empty set
bool [:[:F,G:],D:] is non empty set
u is Element of F
<*u*> is Relation-like K155() -defined F -valued Function-like constant non empty trivial V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of F
d1 is Element of G
<*d1*> is Relation-like K155() -defined G -valued Function-like constant non empty trivial V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of G
d2 is V31() V32() V33() V37() V38() V41() V42() V47() set
d3 is Relation-like [:F,G:] -defined D -valued Function-like non empty total V18([:F,G:],D) Element of bool [:[:F,G:],D:]
d3 . (u,d1) is Element of D
[u,d1] is set
d3 . [u,d1] is set
<*(d3 . (u,d1))*> is Relation-like K155() -defined D -valued Function-like constant non empty trivial V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of D
d4 is Relation-like K155() -defined F -valued Function-like V42() V49(d2) FinSequence-like FinSubsequence-like FinSequence of F
d4 ^ <*u*> is Relation-like K155() -defined F -valued Function-like non empty V42() V49(d2 + 1) FinSequence-like FinSubsequence-like FinSequence of F
d2 + 1 is non empty V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
f is Relation-like K155() -defined G -valued Function-like V42() V49(d2) FinSequence-like FinSubsequence-like FinSequence of G
f ^ <*d1*> is Relation-like K155() -defined G -valued Function-like non empty V42() V49(d2 + 1) FinSequence-like FinSubsequence-like FinSequence of G
(F,G,D,d3,(d4 ^ <*u*>),(f ^ <*d1*>)) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:(d4 ^ <*u*>),(f ^ <*d1*>):> is Relation-like Function-like set
<:(d4 ^ <*u*>),(f ^ <*d1*>):> * d3 is Relation-like D -valued Function-like set
(F,G,D,d3,d4,f) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:d4,f:> is Relation-like Function-like set
<:d4,f:> * d3 is Relation-like D -valued Function-like set
(F,G,D,d3,d4,f) ^ <*(d3 . (u,d1))*> is Relation-like K155() -defined D -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of D
len f is V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
len (f ^ <*d1*>) is non empty V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
len d4 is V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
len (F,G,D,d3,d4,f) is V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
len (d4 ^ <*u*>) is non empty V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
len (F,G,D,d3,(d4 ^ <*u*>),(f ^ <*d1*>)) is V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
dom (F,G,D,d3,(d4 ^ <*u*>),(f ^ <*d1*>)) is Element of bool K155()
Seg (d2 + 1) is non empty V42() V49(d2 + 1) Element of bool K155()
d is V31() V32() V33() V37() V38() V41() V42() V47() set
Seg d2 is V42() V49(d2) Element of bool K155()
Seg (len d4) is V42() V49( len d4) Element of bool K155()
dom d4 is V49(d2) Element of bool K155()
(d4 ^ <*u*>) . d is set
d4 . d is set
Seg (len (F,G,D,d3,d4,f)) is V42() V49( len (F,G,D,d3,d4,f)) Element of bool K155()
dom (F,G,D,d3,d4,f) is Element of bool K155()
Seg (len f) is V42() V49( len f) Element of bool K155()
dom f is V49(d2) Element of bool K155()
(f ^ <*d1*>) . d is set
f . d is set
d3 . (((d4 ^ <*u*>) . d),((f ^ <*d1*>) . d)) is set
[((d4 ^ <*u*>) . d),((f ^ <*d1*>) . d)] is set
d3 . [((d4 ^ <*u*>) . d),((f ^ <*d1*>) . d)] is set
(F,G,D,d3,d4,f) . d is set
((F,G,D,d3,d4,f) ^ <*(d3 . (u,d1))*>) . d is set
(d4 ^ <*u*>) . d is set
(f ^ <*d1*>) . d is set
d3 . (((d4 ^ <*u*>) . d),((f ^ <*d1*>) . d)) is set
[((d4 ^ <*u*>) . d),((f ^ <*d1*>) . d)] is set
d3 . [((d4 ^ <*u*>) . d),((f ^ <*d1*>) . d)] is set
((F,G,D,d3,d4,f) ^ <*(d3 . (u,d1))*>) . d is set
Seg d2 is V42() V49(d2) Element of bool K155()
(d4 ^ <*u*>) . d is set
(f ^ <*d1*>) . d is set
d3 . (((d4 ^ <*u*>) . d),((f ^ <*d1*>) . d)) is set
[((d4 ^ <*u*>) . d),((f ^ <*d1*>) . d)] is set
d3 . [((d4 ^ <*u*>) . d),((f ^ <*d1*>) . d)] is set
((F,G,D,d3,d4,f) ^ <*(d3 . (u,d1))*>) . d is set
(d4 ^ <*u*>) . d is set
(f ^ <*d1*>) . d is set
d3 . (((d4 ^ <*u*>) . d),((f ^ <*d1*>) . d)) is set
[((d4 ^ <*u*>) . d),((f ^ <*d1*>) . d)] is set
d3 . [((d4 ^ <*u*>) . d),((f ^ <*d1*>) . d)] is set
((F,G,D,d3,d4,f) ^ <*(d3 . (u,d1))*>) . d is set
(F,G,D,d3,(d4 ^ <*u*>),(f ^ <*d1*>)) . d is set
len ((F,G,D,d3,d4,f) ^ <*(d3 . (u,d1))*>) is non empty V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
(len (F,G,D,d3,d4,f)) + 1 is non empty V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
D is non empty set
F is non empty set
G is non empty set
[:F,G:] is Relation-like non empty set
[:[:F,G:],D:] is Relation-like non empty set
bool [:[:F,G:],D:] is non empty set
u is V31() V32() V33() V37() V38() V41() V42() V47() set
d1 is V31() V32() V33() V37() V38() V41() V42() V47() set
d2 is Relation-like [:F,G:] -defined D -valued Function-like non empty total V18([:F,G:],D) Element of bool [:[:F,G:],D:]
d3 is Relation-like K155() -defined F -valued Function-like V42() V49(u) FinSequence-like FinSubsequence-like FinSequence of F
d4 is Relation-like K155() -defined G -valued Function-like V42() V49(u) FinSequence-like FinSubsequence-like FinSequence of G
(F,G,D,d2,d3,d4) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:d3,d4:> is Relation-like Function-like set
<:d3,d4:> * d2 is Relation-like D -valued Function-like set
f is Relation-like K155() -defined F -valued Function-like V42() V49(d1) FinSequence-like FinSubsequence-like FinSequence of F
d3 ^ f is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
g is Relation-like K155() -defined G -valued Function-like V42() V49(d1) FinSequence-like FinSubsequence-like FinSequence of G
d4 ^ g is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of G
(F,G,D,d2,(d3 ^ f),(d4 ^ g)) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:(d3 ^ f),(d4 ^ g):> is Relation-like Function-like set
<:(d3 ^ f),(d4 ^ g):> * d2 is Relation-like D -valued Function-like set
(F,G,D,d2,f,g) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:f,g:> is Relation-like Function-like set
<:f,g:> * d2 is Relation-like D -valued Function-like set
(F,G,D,d2,d3,d4) ^ (F,G,D,d2,f,g) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
H is V31() V32() V33() V37() V38() V41() V42() V47() set
H + 1 is non empty V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
H -tuples_on F is functional non empty FinSequence-membered FinSequenceSet of F
F * is functional non empty FinSequence-membered FinSequenceSet of F
{ b₁ where b₁ is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like Element of F * : len b₁ = H } is set
i is Relation-like K155() -defined F -valued Function-like V42() V49(H + 1) FinSequence-like FinSubsequence-like FinSequence of F
S1 is Relation-like K155() -defined F -valued Function-like V42() V49(H) FinSequence-like FinSubsequence-like Element of H -tuples_on F
d is Element of F
<*d*> is Relation-like K155() -defined F -valued Function-like constant non empty trivial V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of F
S1 ^ <*d*> is Relation-like K155() -defined F -valued Function-like non empty V42() V49(H + 1) FinSequence-like FinSubsequence-like FinSequence of F
d3 ^ i is Relation-like K155() -defined F -valued Function-like V42() V49(u + (H + 1)) FinSequence-like FinSubsequence-like FinSequence of F
u + (H + 1) is non empty V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
d3 ^ S1 is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
(d3 ^ S1) ^ <*d*> is Relation-like K155() -defined F -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of F
H -tuples_on G is functional non empty FinSequence-membered FinSequenceSet of G
G * is functional non empty FinSequence-membered FinSequenceSet of G
{ b₁ where b₁ is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like Element of G * : len b₁ = H } is set
j is Relation-like K155() -defined G -valued Function-like V42() V49(H + 1) FinSequence-like FinSubsequence-like FinSequence of G
S19 is Relation-like K155() -defined G -valued Function-like V42() V49(H) FinSequence-like FinSubsequence-like Element of H -tuples_on G
d9 is Element of G
<*d9*> is Relation-like K155() -defined G -valued Function-like constant non empty trivial V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of G
S19 ^ <*d9*> is Relation-like K155() -defined G -valued Function-like non empty V42() V49(H + 1) FinSequence-like FinSubsequence-like FinSequence of G
d4 ^ j is Relation-like K155() -defined G -valued Function-like V42() V49(u + (H + 1)) FinSequence-like FinSubsequence-like FinSequence of G
d4 ^ S19 is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of G
(d4 ^ S19) ^ <*d9*> is Relation-like K155() -defined G -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of G
S1 is Relation-like K155() -defined F -valued Function-like V42() V49(H) FinSequence-like FinSubsequence-like FinSequence of F
d3 ^ S1 is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
u + H is V31() V32() V33() V37() V38() V41() V42() V47() set
S19 is Relation-like K155() -defined G -valued Function-like V42() V49(H) FinSequence-like FinSubsequence-like FinSequence of G
d4 ^ S19 is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of G
(F,G,D,d2,(d3 ^ i),(d4 ^ j)) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:(d3 ^ i),(d4 ^ j):> is Relation-like Function-like set
<:(d3 ^ i),(d4 ^ j):> * d2 is Relation-like D -valued Function-like set
(F,G,D,d2,(d3 ^ S1),(d4 ^ S19)) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:(d3 ^ S1),(d4 ^ S19):> is Relation-like Function-like set
<:(d3 ^ S1),(d4 ^ S19):> * d2 is Relation-like D -valued Function-like set
d2 . (d,d9) is Element of D
[d,d9] is set
d2 . [d,d9] is set
<*(d2 . (d,d9))*> is Relation-like K155() -defined D -valued Function-like constant non empty trivial V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of D
(F,G,D,d2,(d3 ^ S1),(d4 ^ S19)) ^ <*(d2 . (d,d9))*> is Relation-like K155() -defined D -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of D
(F,G,D,d2,S1,S19) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:S1,S19:> is Relation-like Function-like set
<:S1,S19:> * d2 is Relation-like D -valued Function-like set
(F,G,D,d2,d3,d4) ^ (F,G,D,d2,S1,S19) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
((F,G,D,d2,d3,d4) ^ (F,G,D,d2,S1,S19)) ^ <*(d2 . (d,d9))*> is Relation-like K155() -defined D -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of D
(F,G,D,d2,S1,S19) ^ <*(d2 . (d,d9))*> is Relation-like K155() -defined D -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of D
(F,G,D,d2,d3,d4) ^ ((F,G,D,d2,S1,S19) ^ <*(d2 . (d,d9))*>) is Relation-like K155() -defined D -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of D
(F,G,D,d2,i,j) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:i,j:> is Relation-like Function-like set
<:i,j:> * d2 is Relation-like D -valued Function-like set
(F,G,D,d2,d3,d4) ^ (F,G,D,d2,i,j) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
H is V31() V32() V33() V37() V38() V41() V42() V47() set
H + 1 is non empty V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
i is Relation-like K155() -defined F -valued Function-like V42() V49(H + 1) FinSequence-like FinSubsequence-like FinSequence of F
d3 ^ i is Relation-like K155() -defined F -valued Function-like V42() V49(u + (H + 1)) FinSequence-like FinSubsequence-like FinSequence of F
u + (H + 1) is non empty V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
j is Relation-like K155() -defined G -valued Function-like V42() V49(H + 1) FinSequence-like FinSubsequence-like FinSequence of G
d4 ^ j is Relation-like K155() -defined G -valued Function-like V42() V49(u + (H + 1)) FinSequence-like FinSubsequence-like FinSequence of G
(F,G,D,d2,(d3 ^ i),(d4 ^ j)) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:(d3 ^ i),(d4 ^ j):> is Relation-like Function-like set
<:(d3 ^ i),(d4 ^ j):> * d2 is Relation-like D -valued Function-like set
(F,G,D,d2,i,j) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:i,j:> is Relation-like Function-like set
<:i,j:> * d2 is Relation-like D -valued Function-like set
(F,G,D,d2,d3,d4) ^ (F,G,D,d2,i,j) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
[:K155(),F:] is Relation-like non empty V42() set
[:K155(),G:] is Relation-like non empty V42() set
H is Relation-like non-empty empty-yielding K155() -defined F -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of F
<*> F is Relation-like non-empty empty-yielding K155() -defined F -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of F
i is Relation-like non-empty empty-yielding K155() -defined G -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of G
(F,G,D,d2,H,i) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:H,i:> is Relation-like Function-like set
<:H,i:> * d2 is Relation-like D -valued Function-like set
<*> D is Relation-like non-empty empty-yielding K155() -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
[:K155(),D:] is Relation-like non empty V42() set
d3 ^ H is Relation-like K155() -defined F -valued Function-like V42() V49(u + 0) FinSequence-like FinSubsequence-like FinSequence of F
u + 0 is V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
d4 ^ i is Relation-like K155() -defined G -valued Function-like V42() V49(u + 0) FinSequence-like FinSubsequence-like FinSequence of G
(F,G,D,d2,(d3 ^ H),(d4 ^ i)) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:(d3 ^ H),(d4 ^ i):> is Relation-like Function-like set
<:(d3 ^ H),(d4 ^ i):> * d2 is Relation-like D -valued Function-like set
(F,G,D,d2,d3,d4) ^ (F,G,D,d2,H,i) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
H is Relation-like non-empty empty-yielding K155() -defined F -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of F
d3 ^ H is Relation-like K155() -defined F -valued Function-like V42() V49(u + 0) FinSequence-like FinSubsequence-like FinSequence of F
i is Relation-like non-empty empty-yielding K155() -defined G -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of G
d4 ^ i is Relation-like K155() -defined G -valued Function-like V42() V49(u + 0) FinSequence-like FinSubsequence-like FinSequence of G
(F,G,D,d2,(d3 ^ H),(d4 ^ i)) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:(d3 ^ H),(d4 ^ i):> is Relation-like Function-like set
<:(d3 ^ H),(d4 ^ i):> * d2 is Relation-like D -valued Function-like set
(F,G,D,d2,H,i) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:H,i:> is Relation-like Function-like set
<:H,i:> * d2 is Relation-like D -valued Function-like set
(F,G,D,d2,d3,d4) ^ (F,G,D,d2,H,i) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
F is non empty set
G is non empty set
[:D,G:] is Relation-like non empty set
[:[:D,G:],F:] is Relation-like non empty set
bool [:[:D,G:],F:] is non empty set
u is Element of D
d1 is Element of G
<*d1*> is Relation-like K155() -defined G -valued Function-like constant non empty trivial V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of G
d2 is Relation-like [:D,G:] -defined F -valued Function-like non empty total V18([:D,G:],F) Element of bool [:[:D,G:],F:]
d2 . (u,d1) is Element of F
[u,d1] is set
d2 . [u,d1] is set
<*(d2 . (u,d1))*> is Relation-like K155() -defined F -valued Function-like constant non empty trivial V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of F
d3 is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of G
d3 ^ <*d1*> is Relation-like K155() -defined G -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of G
(D,G,F,d2,u,(d3 ^ <*d1*>)) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
dom (d3 ^ <*d1*>) is non empty set
(dom (d3 ^ <*d1*>)) --> u is Relation-like dom (d3 ^ <*d1*>) -defined D -valued Function-like constant non empty total set
{u} is non empty trivial V49(1) set
[:(dom (d3 ^ <*d1*>)),{u}:] is Relation-like non empty set
<:((dom (d3 ^ <*d1*>)) --> u),(d3 ^ <*d1*>):> is Relation-like Function-like set
<:((dom (d3 ^ <*d1*>)) --> u),(d3 ^ <*d1*>):> * d2 is Relation-like F -valued Function-like set
(D,G,F,d2,u,d3) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
dom d3 is set
(dom d3) --> u is Relation-like dom d3 -defined D -valued Function-like constant total set
[:(dom d3),{u}:] is Relation-like set
<:((dom d3) --> u),d3:> is Relation-like Function-like set
<:((dom d3) --> u),d3:> * d2 is Relation-like F -valued Function-like set
(D,G,F,d2,u,d3) ^ <*(d2 . (u,d1))*> is Relation-like K155() -defined F -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of F
len d3 is V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
len (D,G,F,d2,u,d3) is V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
len (d3 ^ <*d1*>) is non empty V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
(len d3) + 1 is non empty V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
len (D,G,F,d2,u,(d3 ^ <*d1*>)) is V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
dom (D,G,F,d2,u,(d3 ^ <*d1*>)) is Element of bool K155()
Seg ((len d3) + 1) is non empty V42() V49((len d3) + 1) Element of bool K155()
j is V31() V32() V33() V37() V38() V41() V42() V47() set
Seg (len d3) is V42() V49( len d3) Element of bool K155()
dom (D,G,F,d2,u,d3) is Element of bool K155()
Seg (len (D,G,F,d2,u,d3)) is V42() V49( len (D,G,F,d2,u,d3)) Element of bool K155()
dom d3 is Element of bool K155()
(d3 ^ <*d1*>) . j is set
d2 . (u,((d3 ^ <*d1*>) . j)) is set
[u,((d3 ^ <*d1*>) . j)] is set
d2 . [u,((d3 ^ <*d1*>) . j)] is set
d3 . j is set
d2 . (u,(d3 . j)) is set
[u,(d3 . j)] is set
d2 . [u,(d3 . j)] is set
(D,G,F,d2,u,d3) . j is set
((D,G,F,d2,u,d3) ^ <*(d2 . (u,d1))*>) . j is set
(d3 ^ <*d1*>) . j is set
d2 . (u,((d3 ^ <*d1*>) . j)) is set
[u,((d3 ^ <*d1*>) . j)] is set
d2 . [u,((d3 ^ <*d1*>) . j)] is set
((D,G,F,d2,u,d3) ^ <*(d2 . (u,d1))*>) . j is set
Seg (len d3) is V42() V49( len d3) Element of bool K155()
(d3 ^ <*d1*>) . j is set
d2 . (u,((d3 ^ <*d1*>) . j)) is set
[u,((d3 ^ <*d1*>) . j)] is set
d2 . [u,((d3 ^ <*d1*>) . j)] is set
((D,G,F,d2,u,d3) ^ <*(d2 . (u,d1))*>) . j is set
(d3 ^ <*d1*>) . j is set
d2 . (u,((d3 ^ <*d1*>) . j)) is set
[u,((d3 ^ <*d1*>) . j)] is set
d2 . [u,((d3 ^ <*d1*>) . j)] is set
((D,G,F,d2,u,d3) ^ <*(d2 . (u,d1))*>) . j is set
(D,G,F,d2,u,(d3 ^ <*d1*>)) . j is set
len ((D,G,F,d2,u,d3) ^ <*(d2 . (u,d1))*>) is non empty V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
(len (D,G,F,d2,u,d3)) + 1 is non empty V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
D is non empty set
F is non empty set
G is non empty set
[:D,G:] is Relation-like non empty set
[:[:D,G:],F:] is Relation-like non empty set
bool [:[:D,G:],F:] is non empty set
u is Element of D
d1 is Relation-like [:D,G:] -defined F -valued Function-like non empty total V18([:D,G:],F) Element of bool [:[:D,G:],F:]
d2 is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of G
(D,G,F,d1,u,d2) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
dom d2 is set
(dom d2) --> u is Relation-like dom d2 -defined D -valued Function-like constant total set
{u} is non empty trivial V49(1) set
[:(dom d2),{u}:] is Relation-like set
<:((dom d2) --> u),d2:> is Relation-like Function-like set
<:((dom d2) --> u),d2:> * d1 is Relation-like F -valued Function-like set
d3 is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of G
d2 ^ d3 is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of G
(D,G,F,d1,u,(d2 ^ d3)) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
dom (d2 ^ d3) is set
(dom (d2 ^ d3)) --> u is Relation-like dom (d2 ^ d3) -defined D -valued Function-like constant total set
[:(dom (d2 ^ d3)),{u}:] is Relation-like set
<:((dom (d2 ^ d3)) --> u),(d2 ^ d3):> is Relation-like Function-like set
<:((dom (d2 ^ d3)) --> u),(d2 ^ d3):> * d1 is Relation-like F -valued Function-like set
(D,G,F,d1,u,d3) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
dom d3 is set
(dom d3) --> u is Relation-like dom d3 -defined D -valued Function-like constant total set
[:(dom d3),{u}:] is Relation-like set
<:((dom d3) --> u),d3:> is Relation-like Function-like set
<:((dom d3) --> u),d3:> * d1 is Relation-like F -valued Function-like set
(D,G,F,d1,u,d2) ^ (D,G,F,d1,u,d3) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
d4 is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of G
d2 ^ d4 is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of G
(D,G,F,d1,u,(d2 ^ d4)) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
dom (d2 ^ d4) is set
(dom (d2 ^ d4)) --> u is Relation-like dom (d2 ^ d4) -defined D -valued Function-like constant total set
[:(dom (d2 ^ d4)),{u}:] is Relation-like set
<:((dom (d2 ^ d4)) --> u),(d2 ^ d4):> is Relation-like Function-like set
<:((dom (d2 ^ d4)) --> u),(d2 ^ d4):> * d1 is Relation-like F -valued Function-like set
(D,G,F,d1,u,d4) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
dom d4 is set
(dom d4) --> u is Relation-like dom d4 -defined D -valued Function-like constant total set
[:(dom d4),{u}:] is Relation-like set
<:((dom d4) --> u),d4:> is Relation-like Function-like set
<:((dom d4) --> u),d4:> * d1 is Relation-like F -valued Function-like set
(D,G,F,d1,u,d2) ^ (D,G,F,d1,u,d4) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
f is Element of G
<*f*> is Relation-like K155() -defined G -valued Function-like constant non empty trivial V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of G
d4 ^ <*f*> is Relation-like K155() -defined G -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of G
d2 ^ (d4 ^ <*f*>) is Relation-like K155() -defined G -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of G
(D,G,F,d1,u,(d2 ^ (d4 ^ <*f*>))) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
dom (d2 ^ (d4 ^ <*f*>)) is non empty set
(dom (d2 ^ (d4 ^ <*f*>))) --> u is Relation-like dom (d2 ^ (d4 ^ <*f*>)) -defined D -valued Function-like constant non empty total set
[:(dom (d2 ^ (d4 ^ <*f*>))),{u}:] is Relation-like non empty set
<:((dom (d2 ^ (d4 ^ <*f*>))) --> u),(d2 ^ (d4 ^ <*f*>)):> is Relation-like Function-like set
<:((dom (d2 ^ (d4 ^ <*f*>))) --> u),(d2 ^ (d4 ^ <*f*>)):> * d1 is Relation-like F -valued Function-like set
(D,G,F,d1,u,(d4 ^ <*f*>)) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
dom (d4 ^ <*f*>) is non empty set
(dom (d4 ^ <*f*>)) --> u is Relation-like dom (d4 ^ <*f*>) -defined D -valued Function-like constant non empty total set
[:(dom (d4 ^ <*f*>)),{u}:] is Relation-like non empty set
<:((dom (d4 ^ <*f*>)) --> u),(d4 ^ <*f*>):> is Relation-like Function-like set
<:((dom (d4 ^ <*f*>)) --> u),(d4 ^ <*f*>):> * d1 is Relation-like F -valued Function-like set
(D,G,F,d1,u,d2) ^ (D,G,F,d1,u,(d4 ^ <*f*>)) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
(d2 ^ d4) ^ <*f*> is Relation-like K155() -defined G -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of G
(D,G,F,d1,u,((d2 ^ d4) ^ <*f*>)) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
dom ((d2 ^ d4) ^ <*f*>) is non empty set
(dom ((d2 ^ d4) ^ <*f*>)) --> u is Relation-like dom ((d2 ^ d4) ^ <*f*>) -defined D -valued Function-like constant non empty total set
[:(dom ((d2 ^ d4) ^ <*f*>)),{u}:] is Relation-like non empty set
<:((dom ((d2 ^ d4) ^ <*f*>)) --> u),((d2 ^ d4) ^ <*f*>):> is Relation-like Function-like set
<:((dom ((d2 ^ d4) ^ <*f*>)) --> u),((d2 ^ d4) ^ <*f*>):> * d1 is Relation-like F -valued Function-like set
d1 . (u,f) is Element of F
[u,f] is set
d1 . [u,f] is set
<*(d1 . (u,f))*> is Relation-like K155() -defined F -valued Function-like constant non empty trivial V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of F
(D,G,F,d1,u,(d2 ^ d4)) ^ <*(d1 . (u,f))*> is Relation-like K155() -defined F -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of F
(D,G,F,d1,u,d4) ^ <*(d1 . (u,f))*> is Relation-like K155() -defined F -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of F
(D,G,F,d1,u,d2) ^ ((D,G,F,d1,u,d4) ^ <*(d1 . (u,f))*>) is Relation-like K155() -defined F -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of F
<*> G is Relation-like non-empty empty-yielding K155() -defined G -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of G
[:K155(),G:] is Relation-like non empty V42() set
d2 ^ (<*> G) is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of G
(D,G,F,d1,u,(d2 ^ (<*> G))) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
dom (d2 ^ (<*> G)) is set
(dom (d2 ^ (<*> G))) --> u is Relation-like dom (d2 ^ (<*> G)) -defined D -valued Function-like constant total set
[:(dom (d2 ^ (<*> G))),{u}:] is Relation-like set
<:((dom (d2 ^ (<*> G))) --> u),(d2 ^ (<*> G)):> is Relation-like Function-like set
<:((dom (d2 ^ (<*> G))) --> u),(d2 ^ (<*> G)):> * d1 is Relation-like F -valued Function-like set
<*> F is Relation-like non-empty empty-yielding K155() -defined F -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of F
[:K155(),F:] is Relation-like non empty V42() set
(D,G,F,d1,u,d2) ^ (<*> F) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
(D,G,F,d1,u,(<*> G)) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
dom (<*> G) is Relation-like non-empty empty-yielding K155() -defined Function-like one-to-one constant functional empty Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set
(dom (<*> G)) --> u is Relation-like non-empty empty-yielding dom (<*> G) -defined D -valued Function-like one-to-one constant functional empty total Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set
[:(dom (<*> G)),{u}:] is Relation-like set
<:((dom (<*> G)) --> u),(<*> G):> is Relation-like Function-like set
<:((dom (<*> G)) --> u),(<*> G):> * d1 is Relation-like F -valued Function-like set
(D,G,F,d1,u,d2) ^ (D,G,F,d1,u,(<*> G)) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
D is non empty set
F is non empty set
G is non empty set
[:G,D:] is Relation-like non empty set
[:[:G,D:],F:] is Relation-like non empty set
bool [:[:G,D:],F:] is non empty set
u is Element of G
<*u*> is Relation-like K155() -defined G -valued Function-like constant non empty trivial V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of G
d1 is Element of D
d2 is Relation-like [:G,D:] -defined F -valued Function-like non empty total V18([:G,D:],F) Element of bool [:[:G,D:],F:]
d2 . (u,d1) is Element of F
[u,d1] is set
d2 . [u,d1] is set
<*(d2 . (u,d1))*> is Relation-like K155() -defined F -valued Function-like constant non empty trivial V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of F
d3 is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of G
d3 ^ <*u*> is Relation-like K155() -defined G -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of G
(G,D,F,d2,(d3 ^ <*u*>),d1) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
dom (d3 ^ <*u*>) is non empty set
(dom (d3 ^ <*u*>)) --> d1 is Relation-like dom (d3 ^ <*u*>) -defined D -valued Function-like constant non empty total set
{d1} is non empty trivial V49(1) set
[:(dom (d3 ^ <*u*>)),{d1}:] is Relation-like non empty set
<:(d3 ^ <*u*>),((dom (d3 ^ <*u*>)) --> d1):> is Relation-like Function-like set
<:(d3 ^ <*u*>),((dom (d3 ^ <*u*>)) --> d1):> * d2 is Relation-like F -valued Function-like set
(G,D,F,d2,d3,d1) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
dom d3 is set
(dom d3) --> d1 is Relation-like dom d3 -defined D -valued Function-like constant total set
[:(dom d3),{d1}:] is Relation-like set
<:d3,((dom d3) --> d1):> is Relation-like Function-like set
<:d3,((dom d3) --> d1):> * d2 is Relation-like F -valued Function-like set
(G,D,F,d2,d3,d1) ^ <*(d2 . (u,d1))*> is Relation-like K155() -defined F -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of F
len d3 is V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
len (G,D,F,d2,d3,d1) is V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
len (d3 ^ <*u*>) is non empty V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
(len d3) + 1 is non empty V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
len (G,D,F,d2,(d3 ^ <*u*>),d1) is V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
dom (G,D,F,d2,(d3 ^ <*u*>),d1) is Element of bool K155()
Seg ((len d3) + 1) is non empty V42() V49((len d3) + 1) Element of bool K155()
j is V31() V32() V33() V37() V38() V41() V42() V47() set
Seg (len d3) is V42() V49( len d3) Element of bool K155()
dom (G,D,F,d2,d3,d1) is Element of bool K155()
dom d3 is Element of bool K155()
(d3 ^ <*u*>) . j is set
d2 . (((d3 ^ <*u*>) . j),d1) is set
[((d3 ^ <*u*>) . j),d1] is set
d2 . [((d3 ^ <*u*>) . j),d1] is set
d3 . j is set
d2 . ((d3 . j),d1) is set
[(d3 . j),d1] is set
d2 . [(d3 . j),d1] is set
(G,D,F,d2,d3,d1) . j is set
((G,D,F,d2,d3,d1) ^ <*(d2 . (u,d1))*>) . j is set
(d3 ^ <*u*>) . j is set
d2 . (((d3 ^ <*u*>) . j),d1) is set
[((d3 ^ <*u*>) . j),d1] is set
d2 . [((d3 ^ <*u*>) . j),d1] is set
((G,D,F,d2,d3,d1) ^ <*(d2 . (u,d1))*>) . j is set
Seg (len d3) is V42() V49( len d3) Element of bool K155()
(d3 ^ <*u*>) . j is set
d2 . (((d3 ^ <*u*>) . j),d1) is set
[((d3 ^ <*u*>) . j),d1] is set
d2 . [((d3 ^ <*u*>) . j),d1] is set
((G,D,F,d2,d3,d1) ^ <*(d2 . (u,d1))*>) . j is set
(d3 ^ <*u*>) . j is set
d2 . (((d3 ^ <*u*>) . j),d1) is set
[((d3 ^ <*u*>) . j),d1] is set
d2 . [((d3 ^ <*u*>) . j),d1] is set
((G,D,F,d2,d3,d1) ^ <*(d2 . (u,d1))*>) . j is set
(G,D,F,d2,(d3 ^ <*u*>),d1) . j is set
len ((G,D,F,d2,d3,d1) ^ <*(d2 . (u,d1))*>) is non empty V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
(len (G,D,F,d2,d3,d1)) + 1 is non empty V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
D is non empty set
F is non empty set
G is non empty set
[:G,D:] is Relation-like non empty set
[:[:G,D:],F:] is Relation-like non empty set
bool [:[:G,D:],F:] is non empty set
u is Element of D
d1 is Relation-like [:G,D:] -defined F -valued Function-like non empty total V18([:G,D:],F) Element of bool [:[:G,D:],F:]
d2 is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of G
(G,D,F,d1,d2,u) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
dom d2 is set
(dom d2) --> u is Relation-like dom d2 -defined D -valued Function-like constant total set
{u} is non empty trivial V49(1) set
[:(dom d2),{u}:] is Relation-like set
<:d2,((dom d2) --> u):> is Relation-like Function-like set
<:d2,((dom d2) --> u):> * d1 is Relation-like F -valued Function-like set
d3 is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of G
d2 ^ d3 is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of G
(G,D,F,d1,(d2 ^ d3),u) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
dom (d2 ^ d3) is set
(dom (d2 ^ d3)) --> u is Relation-like dom (d2 ^ d3) -defined D -valued Function-like constant total set
[:(dom (d2 ^ d3)),{u}:] is Relation-like set
<:(d2 ^ d3),((dom (d2 ^ d3)) --> u):> is Relation-like Function-like set
<:(d2 ^ d3),((dom (d2 ^ d3)) --> u):> * d1 is Relation-like F -valued Function-like set
(G,D,F,d1,d3,u) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
dom d3 is set
(dom d3) --> u is Relation-like dom d3 -defined D -valued Function-like constant total set
[:(dom d3),{u}:] is Relation-like set
<:d3,((dom d3) --> u):> is Relation-like Function-like set
<:d3,((dom d3) --> u):> * d1 is Relation-like F -valued Function-like set
(G,D,F,d1,d2,u) ^ (G,D,F,d1,d3,u) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
d4 is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of G
d2 ^ d4 is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of G
(G,D,F,d1,(d2 ^ d4),u) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
dom (d2 ^ d4) is set
(dom (d2 ^ d4)) --> u is Relation-like dom (d2 ^ d4) -defined D -valued Function-like constant total set
[:(dom (d2 ^ d4)),{u}:] is Relation-like set
<:(d2 ^ d4),((dom (d2 ^ d4)) --> u):> is Relation-like Function-like set
<:(d2 ^ d4),((dom (d2 ^ d4)) --> u):> * d1 is Relation-like F -valued Function-like set
(G,D,F,d1,d4,u) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
dom d4 is set
(dom d4) --> u is Relation-like dom d4 -defined D -valued Function-like constant total set
[:(dom d4),{u}:] is Relation-like set
<:d4,((dom d4) --> u):> is Relation-like Function-like set
<:d4,((dom d4) --> u):> * d1 is Relation-like F -valued Function-like set
(G,D,F,d1,d2,u) ^ (G,D,F,d1,d4,u) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
f is Element of G
<*f*> is Relation-like K155() -defined G -valued Function-like constant non empty trivial V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of G
d4 ^ <*f*> is Relation-like K155() -defined G -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of G
d2 ^ (d4 ^ <*f*>) is Relation-like K155() -defined G -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of G
(G,D,F,d1,(d2 ^ (d4 ^ <*f*>)),u) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
dom (d2 ^ (d4 ^ <*f*>)) is non empty set
(dom (d2 ^ (d4 ^ <*f*>))) --> u is Relation-like dom (d2 ^ (d4 ^ <*f*>)) -defined D -valued Function-like constant non empty total set
[:(dom (d2 ^ (d4 ^ <*f*>))),{u}:] is Relation-like non empty set
<:(d2 ^ (d4 ^ <*f*>)),((dom (d2 ^ (d4 ^ <*f*>))) --> u):> is Relation-like Function-like set
<:(d2 ^ (d4 ^ <*f*>)),((dom (d2 ^ (d4 ^ <*f*>))) --> u):> * d1 is Relation-like F -valued Function-like set
(G,D,F,d1,(d4 ^ <*f*>),u) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
dom (d4 ^ <*f*>) is non empty set
(dom (d4 ^ <*f*>)) --> u is Relation-like dom (d4 ^ <*f*>) -defined D -valued Function-like constant non empty total set
[:(dom (d4 ^ <*f*>)),{u}:] is Relation-like non empty set
<:(d4 ^ <*f*>),((dom (d4 ^ <*f*>)) --> u):> is Relation-like Function-like set
<:(d4 ^ <*f*>),((dom (d4 ^ <*f*>)) --> u):> * d1 is Relation-like F -valued Function-like set
(G,D,F,d1,d2,u) ^ (G,D,F,d1,(d4 ^ <*f*>),u) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
(d2 ^ d4) ^ <*f*> is Relation-like K155() -defined G -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of G
(G,D,F,d1,((d2 ^ d4) ^ <*f*>),u) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
dom ((d2 ^ d4) ^ <*f*>) is non empty set
(dom ((d2 ^ d4) ^ <*f*>)) --> u is Relation-like dom ((d2 ^ d4) ^ <*f*>) -defined D -valued Function-like constant non empty total set
[:(dom ((d2 ^ d4) ^ <*f*>)),{u}:] is Relation-like non empty set
<:((d2 ^ d4) ^ <*f*>),((dom ((d2 ^ d4) ^ <*f*>)) --> u):> is Relation-like Function-like set
<:((d2 ^ d4) ^ <*f*>),((dom ((d2 ^ d4) ^ <*f*>)) --> u):> * d1 is Relation-like F -valued Function-like set
d1 . (f,u) is Element of F
[f,u] is set
d1 . [f,u] is set
<*(d1 . (f,u))*> is Relation-like K155() -defined F -valued Function-like constant non empty trivial V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of F
(G,D,F,d1,(d2 ^ d4),u) ^ <*(d1 . (f,u))*> is Relation-like K155() -defined F -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of F
(G,D,F,d1,d4,u) ^ <*(d1 . (f,u))*> is Relation-like K155() -defined F -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of F
(G,D,F,d1,d2,u) ^ ((G,D,F,d1,d4,u) ^ <*(d1 . (f,u))*>) is Relation-like K155() -defined F -valued Function-like non empty V42() FinSequence-like FinSubsequence-like FinSequence of F
<*> G is Relation-like non-empty empty-yielding K155() -defined G -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of G
[:K155(),G:] is Relation-like non empty V42() set
d2 ^ (<*> G) is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of G
(G,D,F,d1,(d2 ^ (<*> G)),u) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
dom (d2 ^ (<*> G)) is set
(dom (d2 ^ (<*> G))) --> u is Relation-like dom (d2 ^ (<*> G)) -defined D -valued Function-like constant total set
[:(dom (d2 ^ (<*> G))),{u}:] is Relation-like set
<:(d2 ^ (<*> G)),((dom (d2 ^ (<*> G))) --> u):> is Relation-like Function-like set
<:(d2 ^ (<*> G)),((dom (d2 ^ (<*> G))) --> u):> * d1 is Relation-like F -valued Function-like set
<*> F is Relation-like non-empty empty-yielding K155() -defined F -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of F
[:K155(),F:] is Relation-like non empty V42() set
(G,D,F,d1,d2,u) ^ (<*> F) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
(G,D,F,d1,(<*> G),u) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
dom (<*> G) is Relation-like non-empty empty-yielding K155() -defined Function-like one-to-one constant functional empty Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set
(dom (<*> G)) --> u is Relation-like non-empty empty-yielding dom (<*> G) -defined D -valued Function-like one-to-one constant functional empty total Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set
[:(dom (<*> G)),{u}:] is Relation-like set
<:(<*> G),((dom (<*> G)) --> u):> is Relation-like Function-like set
<:(<*> G),((dom (<*> G)) --> u):> * d1 is Relation-like F -valued Function-like set
(G,D,F,d1,d2,u) ^ (G,D,F,d1,(<*> G),u) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
D is non empty set
F is non empty set
[:D,F:] is Relation-like non empty set
bool [:D,F:] is non empty set
G is Element of D
u is V31() V32() V33() V37() V38() V41() V42() V47() set
u |-> G is Relation-like K155() -defined D -valued Function-like V42() V49(u) FinSequence-like FinSubsequence-like Element of u -tuples_on D
u -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
D * is functional non empty FinSequence-membered FinSequenceSet of D
{ b₁ where b₁ is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like Element of D * : len b₁ = u } is set
Seg u is V42() V49(u) Element of bool K155()
(Seg u) --> G is Relation-like Seg u -defined Seg u -defined D -valued {G} -valued Function-like constant total total V18( Seg u,{G}) V42() FinSequence-like FinSubsequence-like Element of bool [:(Seg u),{G}:]
{G} is non empty trivial V49(1) set
[:(Seg u),{G}:] is Relation-like set
bool [:(Seg u),{G}:] is non empty set
d1 is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
(D,F,(u |-> G),d1) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
d1 . G is Element of F
u |-> (d1 . G) is Relation-like K155() -defined F -valued Function-like V42() V49(u) FinSequence-like FinSubsequence-like Element of u -tuples_on F
u -tuples_on F is functional non empty FinSequence-membered FinSequenceSet of F
F * is functional non empty FinSequence-membered FinSequenceSet of F
{ b₁ where b₁ is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like Element of F * : len b₁ = u } is set
(Seg u) --> (d1 . G) is Relation-like Seg u -defined Seg u -defined F -valued {(d1 . G)} -valued Function-like constant total total V18( Seg u,{(d1 . G)}) V42() FinSequence-like FinSubsequence-like Element of bool [:(Seg u),{(d1 . G)}:]
{(d1 . G)} is non empty trivial V49(1) set
[:(Seg u),{(d1 . G)}:] is Relation-like set
bool [:(Seg u),{(d1 . G)}:] is non empty set
dom d1 is non empty Element of bool D
bool D is non empty set
D is non empty set
F is non empty set
[:D,F:] is Relation-like non empty set
G is non empty set
[:[:D,F:],G:] is Relation-like non empty set
bool [:[:D,F:],G:] is non empty set
u is Element of D
d1 is Element of F
d2 is V31() V32() V33() V37() V38() V41() V42() V47() set
d2 |-> u is Relation-like K155() -defined D -valued Function-like V42() V49(d2) FinSequence-like FinSubsequence-like Element of d2 -tuples_on D
d2 -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
D * is functional non empty FinSequence-membered FinSequenceSet of D
{ b₁ where b₁ is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like Element of D * : len b₁ = d2 } is set
Seg d2 is V42() V49(d2) Element of bool K155()
(Seg d2) --> u is Relation-like Seg d2 -defined Seg d2 -defined D -valued {u} -valued Function-like constant total total V18( Seg d2,{u}) V42() FinSequence-like FinSubsequence-like Element of bool [:(Seg d2),{u}:]
{u} is non empty trivial V49(1) set
[:(Seg d2),{u}:] is Relation-like set
bool [:(Seg d2),{u}:] is non empty set
d2 |-> d1 is Relation-like K155() -defined F -valued Function-like V42() V49(d2) FinSequence-like FinSubsequence-like Element of d2 -tuples_on F
d2 -tuples_on F is functional non empty FinSequence-membered FinSequenceSet of F
F * is functional non empty FinSequence-membered FinSequenceSet of F
{ b₁ where b₁ is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like Element of F * : len b₁ = d2 } is set
(Seg d2) --> d1 is Relation-like Seg d2 -defined Seg d2 -defined F -valued {d1} -valued Function-like constant total total V18( Seg d2,{d1}) V42() FinSequence-like FinSubsequence-like Element of bool [:(Seg d2),{d1}:]
{d1} is non empty trivial V49(1) set
[:(Seg d2),{d1}:] is Relation-like set
bool [:(Seg d2),{d1}:] is non empty set
d3 is Relation-like [:D,F:] -defined G -valued Function-like non empty total V18([:D,F:],G) Element of bool [:[:D,F:],G:]
(D,F,G,d3,(d2 |-> u),(d2 |-> d1)) is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of G
<:(d2 |-> u),(d2 |-> d1):> is Relation-like Function-like set
<:(d2 |-> u),(d2 |-> d1):> * d3 is Relation-like G -valued Function-like set
d3 . (u,d1) is Element of G
[u,d1] is set
d3 . [u,d1] is set
d2 |-> (d3 . (u,d1)) is Relation-like K155() -defined G -valued Function-like V42() V49(d2) FinSequence-like FinSubsequence-like Element of d2 -tuples_on G
d2 -tuples_on G is functional non empty FinSequence-membered FinSequenceSet of G
G * is functional non empty FinSequence-membered FinSequenceSet of G
{ b₁ where b₁ is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like Element of G * : len b₁ = d2 } is set
(Seg d2) --> (d3 . (u,d1)) is Relation-like Seg d2 -defined Seg d2 -defined G -valued {(d3 . (u,d1))} -valued Function-like constant total total V18( Seg d2,{(d3 . (u,d1))}) V42() FinSequence-like FinSubsequence-like Element of bool [:(Seg d2),{(d3 . (u,d1))}:]
{(d3 . (u,d1))} is non empty trivial V49(1) set
[:(Seg d2),{(d3 . (u,d1))}:] is Relation-like set
bool [:(Seg d2),{(d3 . (u,d1))}:] is non empty set
dom d3 is Relation-like D -defined F -valued non empty Element of bool [:D,F:]
bool [:D,F:] is non empty set
D is non empty set
F is non empty set
[:D,F:] is Relation-like non empty set
G is non empty set
[:[:D,F:],G:] is Relation-like non empty set
bool [:[:D,F:],G:] is non empty set
u is Element of D
d1 is Element of F
d2 is V31() V32() V33() V37() V38() V41() V42() V47() set
d2 |-> d1 is Relation-like K155() -defined F -valued Function-like V42() V49(d2) FinSequence-like FinSubsequence-like Element of d2 -tuples_on F
d2 -tuples_on F is functional non empty FinSequence-membered FinSequenceSet of F
F * is functional non empty FinSequence-membered FinSequenceSet of F
{ b₁ where b₁ is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like Element of F * : len b₁ = d2 } is set
Seg d2 is V42() V49(d2) Element of bool K155()
(Seg d2) --> d1 is Relation-like Seg d2 -defined Seg d2 -defined F -valued {d1} -valued Function-like constant total total V18( Seg d2,{d1}) V42() FinSequence-like FinSubsequence-like Element of bool [:(Seg d2),{d1}:]
{d1} is non empty trivial V49(1) set
[:(Seg d2),{d1}:] is Relation-like set
bool [:(Seg d2),{d1}:] is non empty set
d3 is Relation-like [:D,F:] -defined G -valued Function-like non empty total V18([:D,F:],G) Element of bool [:[:D,F:],G:]
(D,F,G,d3,u,(d2 |-> d1)) is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of G
dom (d2 |-> d1) is V49(d2) set
(dom (d2 |-> d1)) --> u is Relation-like dom (d2 |-> d1) -defined D -valued Function-like constant total set
{u} is non empty trivial V49(1) set
[:(dom (d2 |-> d1)),{u}:] is Relation-like set
<:((dom (d2 |-> d1)) --> u),(d2 |-> d1):> is Relation-like Function-like set
<:((dom (d2 |-> d1)) --> u),(d2 |-> d1):> * d3 is Relation-like G -valued Function-like set
d3 . (u,d1) is Element of G
[u,d1] is set
d3 . [u,d1] is set
d2 |-> (d3 . (u,d1)) is Relation-like K155() -defined G -valued Function-like V42() V49(d2) FinSequence-like FinSubsequence-like Element of d2 -tuples_on G
d2 -tuples_on G is functional non empty FinSequence-membered FinSequenceSet of G
G * is functional non empty FinSequence-membered FinSequenceSet of G
{ b₁ where b₁ is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like Element of G * : len b₁ = d2 } is set
(Seg d2) --> (d3 . (u,d1)) is Relation-like Seg d2 -defined Seg d2 -defined G -valued {(d3 . (u,d1))} -valued Function-like constant total total V18( Seg d2,{(d3 . (u,d1))}) V42() FinSequence-like FinSubsequence-like Element of bool [:(Seg d2),{(d3 . (u,d1))}:]
{(d3 . (u,d1))} is non empty trivial V49(1) set
[:(Seg d2),{(d3 . (u,d1))}:] is Relation-like set
bool [:(Seg d2),{(d3 . (u,d1))}:] is non empty set
d2 |-> u is Relation-like K155() -defined D -valued Function-like V42() V49(d2) FinSequence-like FinSubsequence-like Element of d2 -tuples_on D
d2 -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
D * is functional non empty FinSequence-membered FinSequenceSet of D
{ b₁ where b₁ is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like Element of D * : len b₁ = d2 } is set
(Seg d2) --> u is Relation-like Seg d2 -defined Seg d2 -defined D -valued {u} -valued Function-like constant total total V18( Seg d2,{u}) V42() FinSequence-like FinSubsequence-like Element of bool [:(Seg d2),{u}:]
[:(Seg d2),{u}:] is Relation-like set
bool [:(Seg d2),{u}:] is non empty set
(D,F,G,d3,(d2 |-> u),(d2 |-> d1)) is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of G
<:(d2 |-> u),(d2 |-> d1):> is Relation-like Function-like set
<:(d2 |-> u),(d2 |-> d1):> * d3 is Relation-like G -valued Function-like set
D is non empty set
F is non empty set
[:D,F:] is Relation-like non empty set
G is non empty set
[:[:D,F:],G:] is Relation-like non empty set
bool [:[:D,F:],G:] is non empty set
u is Element of D
d1 is Element of F
d2 is V31() V32() V33() V37() V38() V41() V42() V47() set
d2 |-> u is Relation-like K155() -defined D -valued Function-like V42() V49(d2) FinSequence-like FinSubsequence-like Element of d2 -tuples_on D
d2 -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
D * is functional non empty FinSequence-membered FinSequenceSet of D
{ b₁ where b₁ is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like Element of D * : len b₁ = d2 } is set
Seg d2 is V42() V49(d2) Element of bool K155()
(Seg d2) --> u is Relation-like Seg d2 -defined Seg d2 -defined D -valued {u} -valued Function-like constant total total V18( Seg d2,{u}) V42() FinSequence-like FinSubsequence-like Element of bool [:(Seg d2),{u}:]
{u} is non empty trivial V49(1) set
[:(Seg d2),{u}:] is Relation-like set
bool [:(Seg d2),{u}:] is non empty set
d3 is Relation-like [:D,F:] -defined G -valued Function-like non empty total V18([:D,F:],G) Element of bool [:[:D,F:],G:]
(D,F,G,d3,(d2 |-> u),d1) is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of G
dom (d2 |-> u) is V49(d2) set
(dom (d2 |-> u)) --> d1 is Relation-like dom (d2 |-> u) -defined F -valued Function-like constant total set
{d1} is non empty trivial V49(1) set
[:(dom (d2 |-> u)),{d1}:] is Relation-like set
<:(d2 |-> u),((dom (d2 |-> u)) --> d1):> is Relation-like Function-like set
<:(d2 |-> u),((dom (d2 |-> u)) --> d1):> * d3 is Relation-like G -valued Function-like set
d3 . (u,d1) is Element of G
[u,d1] is set
d3 . [u,d1] is set
d2 |-> (d3 . (u,d1)) is Relation-like K155() -defined G -valued Function-like V42() V49(d2) FinSequence-like FinSubsequence-like Element of d2 -tuples_on G
d2 -tuples_on G is functional non empty FinSequence-membered FinSequenceSet of G
G * is functional non empty FinSequence-membered FinSequenceSet of G
{ b₁ where b₁ is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like Element of G * : len b₁ = d2 } is set
(Seg d2) --> (d3 . (u,d1)) is Relation-like Seg d2 -defined Seg d2 -defined G -valued {(d3 . (u,d1))} -valued Function-like constant total total V18( Seg d2,{(d3 . (u,d1))}) V42() FinSequence-like FinSubsequence-like Element of bool [:(Seg d2),{(d3 . (u,d1))}:]
{(d3 . (u,d1))} is non empty trivial V49(1) set
[:(Seg d2),{(d3 . (u,d1))}:] is Relation-like set
bool [:(Seg d2),{(d3 . (u,d1))}:] is non empty set
d2 |-> d1 is Relation-like K155() -defined F -valued Function-like V42() V49(d2) FinSequence-like FinSubsequence-like Element of d2 -tuples_on F
d2 -tuples_on F is functional non empty FinSequence-membered FinSequenceSet of F
F * is functional non empty FinSequence-membered FinSequenceSet of F
{ b₁ where b₁ is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like Element of F * : len b₁ = d2 } is set
(Seg d2) --> d1 is Relation-like Seg d2 -defined Seg d2 -defined F -valued {d1} -valued Function-like constant total total V18( Seg d2,{d1}) V42() FinSequence-like FinSubsequence-like Element of bool [:(Seg d2),{d1}:]
[:(Seg d2),{d1}:] is Relation-like set
bool [:(Seg d2),{d1}:] is non empty set
(D,F,G,d3,(d2 |-> u),(d2 |-> d1)) is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of G
<:(d2 |-> u),(d2 |-> d1):> is Relation-like Function-like set
<:(d2 |-> u),(d2 |-> d1):> * d3 is Relation-like G -valued Function-like set
D is non empty set
F is non empty set
G is non empty set
[:D,G:] is Relation-like non empty set
[:[:D,G:],F:] is Relation-like non empty set
bool [:[:D,G:],F:] is non empty set
u is Element of D
d1 is V31() V32() V33() V37() V38() V41() V42() V47() set
d1 |-> u is Relation-like K155() -defined D -valued Function-like V42() V49(d1) FinSequence-like FinSubsequence-like Element of d1 -tuples_on D
d1 -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
D * is functional non empty FinSequence-membered FinSequenceSet of D
{ b₁ where b₁ is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like Element of D * : len b₁ = d1 } is set
Seg d1 is V42() V49(d1) Element of bool K155()
(Seg d1) --> u is Relation-like Seg d1 -defined Seg d1 -defined D -valued {u} -valued Function-like constant total total V18( Seg d1,{u}) V42() FinSequence-like FinSubsequence-like Element of bool [:(Seg d1),{u}:]
{u} is non empty trivial V49(1) set
[:(Seg d1),{u}:] is Relation-like set
bool [:(Seg d1),{u}:] is non empty set
d2 is Relation-like [:D,G:] -defined F -valued Function-like non empty total V18([:D,G:],F) Element of bool [:[:D,G:],F:]
d3 is Relation-like K155() -defined G -valued Function-like V42() V49(d1) FinSequence-like FinSubsequence-like FinSequence of G
(D,G,F,d2,(d1 |-> u),d3) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
<:(d1 |-> u),d3:> is Relation-like Function-like set
<:(d1 |-> u),d3:> * d2 is Relation-like F -valued Function-like set
(D,G,F,d2,u,d3) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
dom d3 is V49(d1) set
(dom d3) --> u is Relation-like dom d3 -defined D -valued Function-like constant total set
[:(dom d3),{u}:] is Relation-like set
<:((dom d3) --> u),d3:> is Relation-like Function-like set
<:((dom d3) --> u),d3:> * d2 is Relation-like F -valued Function-like set
dom d3 is V49(d1) Element of bool K155()
len d3 is V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
Seg (len d3) is V42() V49( len d3) Element of bool K155()
D is non empty set
F is non empty set
G is non empty set
[:G,D:] is Relation-like non empty set
[:[:G,D:],F:] is Relation-like non empty set
bool [:[:G,D:],F:] is non empty set
u is Element of G
d1 is V31() V32() V33() V37() V38() V41() V42() V47() set
d1 |-> u is Relation-like K155() -defined G -valued Function-like V42() V49(d1) FinSequence-like FinSubsequence-like Element of d1 -tuples_on G
d1 -tuples_on G is functional non empty FinSequence-membered FinSequenceSet of G
G * is functional non empty FinSequence-membered FinSequenceSet of G
{ b₁ where b₁ is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like Element of G * : len b₁ = d1 } is set
Seg d1 is V42() V49(d1) Element of bool K155()
(Seg d1) --> u is Relation-like Seg d1 -defined Seg d1 -defined G -valued {u} -valued Function-like constant total total V18( Seg d1,{u}) V42() FinSequence-like FinSubsequence-like Element of bool [:(Seg d1),{u}:]
{u} is non empty trivial V49(1) set
[:(Seg d1),{u}:] is Relation-like set
bool [:(Seg d1),{u}:] is non empty set
d2 is Relation-like [:G,D:] -defined F -valued Function-like non empty total V18([:G,D:],F) Element of bool [:[:G,D:],F:]
d3 is Relation-like K155() -defined G -valued Function-like V42() V49(d1) FinSequence-like FinSubsequence-like FinSequence of G
d2 .: (d3,(d1 |-> u)) is Relation-like Function-like set
<:d3,(d1 |-> u):> is Relation-like Function-like set
<:d3,(d1 |-> u):> * d2 is Relation-like F -valued Function-like set
d2 [:] (d3,u) is Relation-like Function-like set
dom d3 is V49(d1) set
(dom d3) --> u is Relation-like dom d3 -defined G -valued Function-like constant total set
[:(dom d3),{u}:] is Relation-like set
<:d3,((dom d3) --> u):> is Relation-like Function-like set
<:d3,((dom d3) --> u):> * d2 is Relation-like F -valued Function-like set
dom d3 is V49(d1) Element of bool K155()
len d3 is V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
Seg (len d3) is V42() V49( len d3) Element of bool K155()
D is non empty set
F is non empty set
G is non empty set
[:D,G:] is Relation-like non empty set
[:[:D,G:],F:] is Relation-like non empty set
bool [:[:D,G:],F:] is non empty set
id G is Relation-like G -defined G -valued Function-like one-to-one non empty total V18(G,G) Element of bool [:G,G:]
[:G,G:] is Relation-like non empty set
bool [:G,G:] is non empty set
u is Element of D
d1 is V31() V32() V33() V37() V38() V41() V42() V47() set
d2 is Relation-like [:D,G:] -defined F -valued Function-like non empty total V18([:D,G:],F) Element of bool [:[:D,G:],F:]
d2 [;] (u,(id G)) is Relation-like Function-like set
dom (id G) is non empty set
(dom (id G)) --> u is Relation-like dom (id G) -defined D -valued Function-like constant non empty total set
{u} is non empty trivial V49(1) set
[:(dom (id G)),{u}:] is Relation-like non empty set
<:((dom (id G)) --> u),(id G):> is Relation-like Function-like set
<:((dom (id G)) --> u),(id G):> * d2 is Relation-like F -valued Function-like set
d3 is Relation-like K155() -defined G -valued Function-like V42() V49(d1) FinSequence-like FinSubsequence-like FinSequence of G
(D,G,F,d2,u,d3) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
dom d3 is V49(d1) set
(dom d3) --> u is Relation-like dom d3 -defined D -valued Function-like constant total set
[:(dom d3),{u}:] is Relation-like set
<:((dom d3) --> u),d3:> is Relation-like Function-like set
<:((dom d3) --> u),d3:> * d2 is Relation-like F -valued Function-like set
d3 * (d2 [;] (u,(id G))) is Relation-like K155() -defined Function-like set
rng d3 is Element of bool G
bool G is non empty set
(G,G,d3,(id G)) is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of G
(D,G,F,d2,u,(G,G,d3,(id G))) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
dom (G,G,d3,(id G)) is set
(dom (G,G,d3,(id G))) --> u is Relation-like dom (G,G,d3,(id G)) -defined D -valued Function-like constant total set
[:(dom (G,G,d3,(id G))),{u}:] is Relation-like set
<:((dom (G,G,d3,(id G))) --> u),(G,G,d3,(id G)):> is Relation-like Function-like set
<:((dom (G,G,d3,(id G))) --> u),(G,G,d3,(id G)):> * d2 is Relation-like F -valued Function-like set
D is non empty set
F is non empty set
G is non empty set
[:G,D:] is Relation-like non empty set
[:[:G,D:],F:] is Relation-like non empty set
bool [:[:G,D:],F:] is non empty set
id G is Relation-like G -defined G -valued Function-like one-to-one non empty total V18(G,G) Element of bool [:G,G:]
[:G,G:] is Relation-like non empty set
bool [:G,G:] is non empty set
u is Element of G
d1 is V31() V32() V33() V37() V38() V41() V42() V47() set
d2 is Relation-like [:G,D:] -defined F -valued Function-like non empty total V18([:G,D:],F) Element of bool [:[:G,D:],F:]
d2 [:] ((id G),u) is Relation-like Function-like set
dom (id G) is non empty set
(dom (id G)) --> u is Relation-like dom (id G) -defined G -valued Function-like constant non empty total set
{u} is non empty trivial V49(1) set
[:(dom (id G)),{u}:] is Relation-like non empty set
<:(id G),((dom (id G)) --> u):> is Relation-like Function-like set
<:(id G),((dom (id G)) --> u):> * d2 is Relation-like F -valued Function-like set
d3 is Relation-like K155() -defined G -valued Function-like V42() V49(d1) FinSequence-like FinSubsequence-like FinSequence of G
d2 [:] (d3,u) is Relation-like Function-like set
dom d3 is V49(d1) set
(dom d3) --> u is Relation-like dom d3 -defined G -valued Function-like constant total set
[:(dom d3),{u}:] is Relation-like set
<:d3,((dom d3) --> u):> is Relation-like Function-like set
<:d3,((dom d3) --> u):> * d2 is Relation-like F -valued Function-like set
d3 * (d2 [:] ((id G),u)) is Relation-like K155() -defined Function-like set
rng d3 is Element of bool G
bool G is non empty set
(G,G,d3,(id G)) is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of G
d2 [:] ((G,G,d3,(id G)),u) is Relation-like Function-like set
dom (G,G,d3,(id G)) is set
(dom (G,G,d3,(id G))) --> u is Relation-like dom (G,G,d3,(id G)) -defined G -valued Function-like constant total set
[:(dom (G,G,d3,(id G))),{u}:] is Relation-like set
<:(G,G,d3,(id G)),((dom (G,G,d3,(id G))) --> u):> is Relation-like Function-like set
<:(G,G,d3,(id G)),((dom (G,G,d3,(id G))) --> u):> * d2 is Relation-like F -valued Function-like set
D is non empty set
F is V31() V32() V33() V37() V38() V41() V42() V47() set
Seg F is V42() V49(F) Element of bool K155()
[:(Seg F),D:] is Relation-like set
bool [:(Seg F),D:] is non empty set
G is Relation-like K155() -defined D -valued Function-like V42() V49(F) FinSequence-like FinSubsequence-like FinSequence of D
len G is V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()
dom G is V49(F) Element of bool K155()
D is non empty set
F is non empty set
[:D,F:] is Relation-like non empty set
bool [:D,F:] is non empty set
[:F,F:] is Relation-like non empty set
[:[:F,F:],F:] is Relation-like non empty set
bool [:[:F,F:],F:] is non empty set
id F is Relation-like F -defined F -valued Function-like one-to-one non empty total V18(F,F) Element of bool [:F,F:]
bool [:F,F:] is non empty set
G is Element of F
u is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
d1 is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
d2 is Relation-like [:F,F:] -defined F -valued Function-like non empty total V18([:F,F:],F) Element of bool [:[:F,F:],F:]
d2 .: (u,d1) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
<:u,d1:> is Relation-like Function-like set
<:u,d1:> * d2 is Relation-like F -valued Function-like set
d2 [;] (G,(id F)) is Relation-like F -defined F -valued Function-like non empty total V18(F,F) Element of bool [:F,F:]
dom (id F) is non empty set
(dom (id F)) --> G is Relation-like dom (id F) -defined F -valued Function-like constant non empty total set
{G} is non empty trivial V49(1) set
[:(dom (id F)),{G}:] is Relation-like non empty set
<:((dom (id F)) --> G),(id F):> is Relation-like Function-like set
<:((dom (id F)) --> G),(id F):> * d2 is Relation-like F -valued Function-like set
(d2 [;] (G,(id F))) * (d2 .: (u,d1)) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
(d2 [;] (G,(id F))) * u is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
d2 .: (((d2 [;] (G,(id F))) * u),d1) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
<:((d2 [;] (G,(id F))) * u),d1:> is Relation-like Function-like set
<:((d2 [;] (G,(id F))) * u),d1:> * d2 is Relation-like F -valued Function-like set
d3 is Element of D
((d2 [;] (G,(id F))) * (d2 .: (u,d1))) . d3 is Element of F
(d2 .: (u,d1)) . d3 is Element of F
(d2 [;] (G,(id F))) . ((d2 .: (u,d1)) . d3) is Element of F
u . d3 is Element of F
d1 . d3 is Element of F
d2 . ((u . d3),(d1 . d3)) is Element of F
[(u . d3),(d1 . d3)] is set
d2 . [(u . d3),(d1 . d3)] is set
(d2 [;] (G,(id F))) . (d2 . ((u . d3),(d1 . d3))) is Element of F
(id F) . (d2 . ((u . d3),(d1 . d3))) is Element of F
d2 . (G,((id F) . (d2 . ((u . d3),(d1 . d3))))) is Element of F
[G,((id F) . (d2 . ((u . d3),(d1 . d3))))] is set
d2 . [G,((id F) . (d2 . ((u . d3),(d1 . d3))))] is set
d2 . (G,(d2 . ((u . d3),(d1 . d3)))) is Element of F
[G,(d2 . ((u . d3),(d1 . d3)))] is set
d2 . [G,(d2 . ((u . d3),(d1 . d3)))] is set
d2 . (G,(u . d3)) is Element of F
[G,(u . d3)] is set
d2 . [G,(u . d3)] is set
d2 . ((d2 . (G,(u . d3))),(d1 . d3)) is Element of F
[(d2 . (G,(u . d3))),(d1 . d3)] is set
d2 . [(d2 . (G,(u . d3))),(d1 . d3)] is set
d2 [;] (G,u) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
dom u is non empty set
(dom u) --> G is Relation-like dom u -defined F -valued Function-like constant non empty total set
[:(dom u),{G}:] is Relation-like non empty set
<:((dom u) --> G),u:> is Relation-like Function-like set
<:((dom u) --> G),u:> * d2 is Relation-like F -valued Function-like set
(d2 [;] (G,u)) . d3 is Element of F
d2 . (((d2 [;] (G,u)) . d3),(d1 . d3)) is Element of F
[((d2 [;] (G,u)) . d3),(d1 . d3)] is set
d2 . [((d2 [;] (G,u)) . d3),(d1 . d3)] is set
((d2 [;] (G,(id F))) * u) . d3 is Element of F
d2 . ((((d2 [;] (G,(id F))) * u) . d3),(d1 . d3)) is Element of F
[(((d2 [;] (G,(id F))) * u) . d3),(d1 . d3)] is set
d2 . [(((d2 [;] (G,(id F))) * u) . d3),(d1 . d3)] is set
(d2 .: (((d2 [;] (G,(id F))) * u),d1)) . d3 is Element of F
D is non empty set
F is non empty set
[:D,F:] is Relation-like non empty set
bool [:D,F:] is non empty set
[:F,F:] is Relation-like non empty set
[:[:F,F:],F:] is Relation-like non empty set
bool [:[:F,F:],F:] is non empty set
id F is Relation-like F -defined F -valued Function-like one-to-one non empty total V18(F,F) Element of bool [:F,F:]
bool [:F,F:] is non empty set
G is Element of F
u is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
d1 is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
d2 is Relation-like [:F,F:] -defined F -valued Function-like non empty total V18([:F,F:],F) Element of bool [:[:F,F:],F:]
d2 .: (u,d1) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
<:u,d1:> is Relation-like Function-like set
<:u,d1:> * d2 is Relation-like F -valued Function-like set
d2 [:] ((id F),G) is Relation-like F -defined F -valued Function-like non empty total V18(F,F) Element of bool [:F,F:]
dom (id F) is non empty set
(dom (id F)) --> G is Relation-like dom (id F) -defined F -valued Function-like constant non empty total set
{G} is non empty trivial V49(1) set
[:(dom (id F)),{G}:] is Relation-like non empty set
<:(id F),((dom (id F)) --> G):> is Relation-like Function-like set
<:(id F),((dom (id F)) --> G):> * d2 is Relation-like F -valued Function-like set
(d2 [:] ((id F),G)) * (d2 .: (u,d1)) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
(d2 [:] ((id F),G)) * d1 is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
d2 .: (u,((d2 [:] ((id F),G)) * d1)) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
<:u,((d2 [:] ((id F),G)) * d1):> is Relation-like Function-like set
<:u,((d2 [:] ((id F),G)) * d1):> * d2 is Relation-like F -valued Function-like set
d3 is Element of D
((d2 [:] ((id F),G)) * (d2 .: (u,d1))) . d3 is Element of F
(d2 .: (u,d1)) . d3 is Element of F
(d2 [:] ((id F),G)) . ((d2 .: (u,d1)) . d3) is Element of F
u . d3 is Element of F
d1 . d3 is Element of F
d2 . ((u . d3),(d1 . d3)) is Element of F
[(u . d3),(d1 . d3)] is set
d2 . [(u . d3),(d1 . d3)] is set
(d2 [:] ((id F),G)) . (d2 . ((u . d3),(d1 . d3))) is Element of F
(id F) . (d2 . ((u . d3),(d1 . d3))) is Element of F
d2 . (((id F) . (d2 . ((u . d3),(d1 . d3)))),G) is Element of F
[((id F) . (d2 . ((u . d3),(d1 . d3)))),G] is set
d2 . [((id F) . (d2 . ((u . d3),(d1 . d3)))),G] is set
d2 . ((d2 . ((u . d3),(d1 . d3))),G) is Element of F
[(d2 . ((u . d3),(d1 . d3))),G] is set
d2 . [(d2 . ((u . d3),(d1 . d3))),G] is set
d2 . ((d1 . d3),G) is Element of F
[(d1 . d3),G] is set
d2 . [(d1 . d3),G] is set
d2 . ((u . d3),(d2 . ((d1 . d3),G))) is Element of F
[(u . d3),(d2 . ((d1 . d3),G))] is set
d2 . [(u . d3),(d2 . ((d1 . d3),G))] is set
d2 [:] (d1,G) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
dom d1 is non empty set
(dom d1) --> G is Relation-like dom d1 -defined F -valued Function-like constant non empty total set
[:(dom d1),{G}:] is Relation-like non empty set
<:d1,((dom d1) --> G):> is Relation-like Function-like set
<:d1,((dom d1) --> G):> * d2 is Relation-like F -valued Function-like set
(d2 [:] (d1,G)) . d3 is Element of F
d2 . ((u . d3),((d2 [:] (d1,G)) . d3)) is Element of F
[(u . d3),((d2 [:] (d1,G)) . d3)] is set
d2 . [(u . d3),((d2 [:] (d1,G)) . d3)] is set
((d2 [:] ((id F),G)) * d1) . d3 is Element of F
d2 . ((u . d3),(((d2 [:] ((id F),G)) * d1) . d3)) is Element of F
[(u . d3),(((d2 [:] ((id F),G)) * d1) . d3)] is set
d2 . [(u . d3),(((d2 [:] ((id F),G)) * d1) . d3)] is set
(d2 .: (u,((d2 [:] ((id F),G)) * d1))) . d3 is Element of F
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
id D is Relation-like D -defined D -valued Function-like one-to-one non empty total V18(D,D) Element of bool [:D,D:]
bool [:D,D:] is non empty set
F is Element of D
G is V31() V32() V33() V37() V38() V41() V42() V47() set
u is Relation-like K155() -defined D -valued Function-like V42() V49(G) FinSequence-like FinSubsequence-like FinSequence of D
d1 is Relation-like K155() -defined D -valued Function-like V42() V49(G) FinSequence-like FinSubsequence-like FinSequence of D
d2 is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
(D,D,D,d2,u,d1) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:u,d1:> is Relation-like Function-like set
<:u,d1:> * d2 is Relation-like D -valued Function-like set
d2 [;] (F,(id D)) is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
dom (id D) is non empty set
(dom (id D)) --> F is Relation-like dom (id D) -defined D -valued Function-like constant non empty total set
{F} is non empty trivial V49(1) set
[:(dom (id D)),{F}:] is Relation-like non empty set
<:((dom (id D)) --> F),(id D):> is Relation-like Function-like set
<:((dom (id D)) --> F),(id D):> * d2 is Relation-like D -valued Function-like set
(D,D,(D,D,D,d2,u,d1),(d2 [;] (F,(id D)))) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
(D,D,u,(d2 [;] (F,(id D)))) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
(D,D,D,d2,(D,D,u,(d2 [;] (F,(id D)))),d1) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:(D,D,u,(d2 [;] (F,(id D)))),d1:> is Relation-like Function-like set
<:(D,D,u,(d2 [;] (F,(id D)))),d1:> * d2 is Relation-like D -valued Function-like set
<*> D is Relation-like non-empty empty-yielding K155() -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
[:K155(),D:] is Relation-like non empty V42() set
Seg G is V42() V49(G) Element of bool K155()
d3 is non empty set
[:d3,D:] is Relation-like non empty set
bool [:d3,D:] is non empty set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
id D is Relation-like D -defined D -valued Function-like one-to-one non empty total V18(D,D) Element of bool [:D,D:]
bool [:D,D:] is non empty set
F is Element of D
G is V31() V32() V33() V37() V38() V41() V42() V47() set
u is Relation-like K155() -defined D -valued Function-like V42() V49(G) FinSequence-like FinSubsequence-like FinSequence of D
d1 is Relation-like K155() -defined D -valued Function-like V42() V49(G) FinSequence-like FinSubsequence-like FinSequence of D
d2 is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
(D,D,D,d2,u,d1) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:u,d1:> is Relation-like Function-like set
<:u,d1:> * d2 is Relation-like D -valued Function-like set
d2 [:] ((id D),F) is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
dom (id D) is non empty set
(dom (id D)) --> F is Relation-like dom (id D) -defined D -valued Function-like constant non empty total set
{F} is non empty trivial V49(1) set
[:(dom (id D)),{F}:] is Relation-like non empty set
<:(id D),((dom (id D)) --> F):> is Relation-like Function-like set
<:(id D),((dom (id D)) --> F):> * d2 is Relation-like D -valued Function-like set
(D,D,(D,D,D,d2,u,d1),(d2 [:] ((id D),F))) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
(D,D,d1,(d2 [:] ((id D),F))) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
(D,D,D,d2,u,(D,D,d1,(d2 [:] ((id D),F)))) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:u,(D,D,d1,(d2 [:] ((id D),F))):> is Relation-like Function-like set
<:u,(D,D,d1,(d2 [:] ((id D),F))):> * d2 is Relation-like D -valued Function-like set
<*> D is Relation-like non-empty empty-yielding K155() -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
[:K155(),D:] is Relation-like non empty V42() set
Seg G is V42() V49(G) Element of bool K155()
d3 is non empty set
[:d3,D:] is Relation-like non empty set
bool [:d3,D:] is non empty set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is V31() V32() V33() V37() V38() V41() V42() V47() set
G is Relation-like K155() -defined D -valued Function-like V42() V49(F) FinSequence-like FinSubsequence-like FinSequence of D
u is Relation-like K155() -defined D -valued Function-like V42() V49(F) FinSequence-like FinSubsequence-like FinSequence of D
d1 is Relation-like K155() -defined D -valued Function-like V42() V49(F) FinSequence-like FinSubsequence-like FinSequence of D
d2 is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
(D,D,D,d2,G,u) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:G,u:> is Relation-like Function-like set
<:G,u:> * d2 is Relation-like D -valued Function-like set
(D,D,D,d2,(D,D,D,d2,G,u),d1) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:(D,D,D,d2,G,u),d1:> is Relation-like Function-like set
<:(D,D,D,d2,G,u),d1:> * d2 is Relation-like D -valued Function-like set
(D,D,D,d2,u,d1) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:u,d1:> is Relation-like Function-like set
<:u,d1:> * d2 is Relation-like D -valued Function-like set
(D,D,D,d2,G,(D,D,D,d2,u,d1)) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:G,(D,D,D,d2,u,d1):> is Relation-like Function-like set
<:G,(D,D,D,d2,u,d1):> * d2 is Relation-like D -valued Function-like set
<*> D is Relation-like non-empty empty-yielding K155() -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
[:K155(),D:] is Relation-like non empty V42() set
Seg F is V42() V49(F) Element of bool K155()
d3 is non empty set
[:d3,D:] is Relation-like non empty set
bool [:d3,D:] is non empty set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is Element of D
G is Element of D
u is V31() V32() V33() V37() V38() V41() V42() V47() set
d1 is Relation-like K155() -defined D -valued Function-like V42() V49(u) FinSequence-like FinSubsequence-like FinSequence of D
d2 is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
(D,D,D,d2,F,d1) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
dom d1 is V49(u) set
(dom d1) --> F is Relation-like dom d1 -defined D -valued Function-like constant total set
{F} is non empty trivial V49(1) set
[:(dom d1),{F}:] is Relation-like set
<:((dom d1) --> F),d1:> is Relation-like Function-like set
<:((dom d1) --> F),d1:> * d2 is Relation-like D -valued Function-like set
(D,D,D,d2,(D,D,D,d2,F,d1),G) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
dom (D,D,D,d2,F,d1) is set
(dom (D,D,D,d2,F,d1)) --> G is Relation-like dom (D,D,D,d2,F,d1) -defined D -valued Function-like constant total set
{G} is non empty trivial V49(1) set
[:(dom (D,D,D,d2,F,d1)),{G}:] is Relation-like set
<:(D,D,D,d2,F,d1),((dom (D,D,D,d2,F,d1)) --> G):> is Relation-like Function-like set
<:(D,D,D,d2,F,d1),((dom (D,D,D,d2,F,d1)) --> G):> * d2 is Relation-like D -valued Function-like set
(D,D,D,d2,d1,G) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
(dom d1) --> G is Relation-like dom d1 -defined D -valued Function-like constant total set
[:(dom d1),{G}:] is Relation-like set
<:d1,((dom d1) --> G):> is Relation-like Function-like set
<:d1,((dom d1) --> G):> * d2 is Relation-like D -valued Function-like set
(D,D,D,d2,F,(D,D,D,d2,d1,G)) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
dom (D,D,D,d2,d1,G) is set
(dom (D,D,D,d2,d1,G)) --> F is Relation-like dom (D,D,D,d2,d1,G) -defined D -valued Function-like constant total set
[:(dom (D,D,D,d2,d1,G)),{F}:] is Relation-like set
<:((dom (D,D,D,d2,d1,G)) --> F),(D,D,D,d2,d1,G):> is Relation-like Function-like set
<:((dom (D,D,D,d2,d1,G)) --> F),(D,D,D,d2,d1,G):> * d2 is Relation-like D -valued Function-like set
<*> D is Relation-like non-empty empty-yielding K155() -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
[:K155(),D:] is Relation-like non empty V42() set
Seg u is V42() V49(u) Element of bool K155()
d3 is non empty set
[:d3,D:] is Relation-like non empty set
bool [:d3,D:] is non empty set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is Element of D
G is V31() V32() V33() V37() V38() V41() V42() V47() set
u is Relation-like K155() -defined D -valued Function-like V42() V49(G) FinSequence-like FinSubsequence-like FinSequence of D
d1 is Relation-like K155() -defined D -valued Function-like V42() V49(G) FinSequence-like FinSubsequence-like FinSequence of D
d2 is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
(D,D,D,d2,u,F) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
dom u is V49(G) set
(dom u) --> F is Relation-like dom u -defined D -valued Function-like constant total set
{F} is non empty trivial V49(1) set
[:(dom u),{F}:] is Relation-like set
<:u,((dom u) --> F):> is Relation-like Function-like set
<:u,((dom u) --> F):> * d2 is Relation-like D -valued Function-like set
(D,D,D,d2,(D,D,D,d2,u,F),d1) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:(D,D,D,d2,u,F),d1:> is Relation-like Function-like set
<:(D,D,D,d2,u,F),d1:> * d2 is Relation-like D -valued Function-like set
(D,D,D,d2,F,d1) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
dom d1 is V49(G) set
(dom d1) --> F is Relation-like dom d1 -defined D -valued Function-like constant total set
[:(dom d1),{F}:] is Relation-like set
<:((dom d1) --> F),d1:> is Relation-like Function-like set
<:((dom d1) --> F),d1:> * d2 is Relation-like D -valued Function-like set
(D,D,D,d2,u,(D,D,D,d2,F,d1)) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:u,(D,D,D,d2,F,d1):> is Relation-like Function-like set
<:u,(D,D,D,d2,F,d1):> * d2 is Relation-like D -valued Function-like set
<*> D is Relation-like non-empty empty-yielding K155() -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
[:K155(),D:] is Relation-like non empty V42() set
Seg G is V42() V49(G) Element of bool K155()
d3 is non empty set
[:d3,D:] is Relation-like non empty set
bool [:d3,D:] is non empty set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is Element of D
G is Element of D
u is V31() V32() V33() V37() V38() V41() V42() V47() set
d1 is Relation-like K155() -defined D -valued Function-like V42() V49(u) FinSequence-like FinSubsequence-like FinSequence of D
d2 is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
d2 . (F,G) is Element of D
[F,G] is set
d2 . [F,G] is set
(D,D,D,d2,(d2 . (F,G)),d1) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
dom d1 is V49(u) set
(dom d1) --> (d2 . (F,G)) is Relation-like dom d1 -defined D -valued Function-like constant total set
{(d2 . (F,G))} is non empty trivial V49(1) set
[:(dom d1),{(d2 . (F,G))}:] is Relation-like set
<:((dom d1) --> (d2 . (F,G))),d1:> is Relation-like Function-like set
<:((dom d1) --> (d2 . (F,G))),d1:> * d2 is Relation-like D -valued Function-like set
(D,D,D,d2,G,d1) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
(dom d1) --> G is Relation-like dom d1 -defined D -valued Function-like constant total set
{G} is non empty trivial V49(1) set
[:(dom d1),{G}:] is Relation-like set
<:((dom d1) --> G),d1:> is Relation-like Function-like set
<:((dom d1) --> G),d1:> * d2 is Relation-like D -valued Function-like set
(D,D,D,d2,F,(D,D,D,d2,G,d1)) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
dom (D,D,D,d2,G,d1) is set
(dom (D,D,D,d2,G,d1)) --> F is Relation-like dom (D,D,D,d2,G,d1) -defined D -valued Function-like constant total set
{F} is non empty trivial V49(1) set
[:(dom (D,D,D,d2,G,d1)),{F}:] is Relation-like set
<:((dom (D,D,D,d2,G,d1)) --> F),(D,D,D,d2,G,d1):> is Relation-like Function-like set
<:((dom (D,D,D,d2,G,d1)) --> F),(D,D,D,d2,G,d1):> * d2 is Relation-like D -valued Function-like set
<*> D is Relation-like non-empty empty-yielding K155() -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
[:K155(),D:] is Relation-like non empty V42() set
Seg u is V42() V49(u) Element of bool K155()
d3 is non empty set
[:d3,D:] is Relation-like non empty set
bool [:d3,D:] is non empty set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is Element of D
G is Element of D
u is V31() V32() V33() V37() V38() V41() V42() V47() set
d1 is Relation-like K155() -defined D -valued Function-like V42() V49(u) FinSequence-like FinSubsequence-like FinSequence of D
d2 is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
d2 . (F,G) is Element of D
[F,G] is set
d2 . [F,G] is set
(D,D,D,d2,d1,(d2 . (F,G))) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
dom d1 is V49(u) set
(dom d1) --> (d2 . (F,G)) is Relation-like dom d1 -defined D -valued Function-like constant total set
{(d2 . (F,G))} is non empty trivial V49(1) set
[:(dom d1),{(d2 . (F,G))}:] is Relation-like set
<:d1,((dom d1) --> (d2 . (F,G))):> is Relation-like Function-like set
<:d1,((dom d1) --> (d2 . (F,G))):> * d2 is Relation-like D -valued Function-like set
(D,D,D,d2,d1,F) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
(dom d1) --> F is Relation-like dom d1 -defined D -valued Function-like constant total set
{F} is non empty trivial V49(1) set
[:(dom d1),{F}:] is Relation-like set
<:d1,((dom d1) --> F):> is Relation-like Function-like set
<:d1,((dom d1) --> F):> * d2 is Relation-like D -valued Function-like set
(D,D,D,d2,(D,D,D,d2,d1,F),G) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
dom (D,D,D,d2,d1,F) is set
(dom (D,D,D,d2,d1,F)) --> G is Relation-like dom (D,D,D,d2,d1,F) -defined D -valued Function-like constant total set
{G} is non empty trivial V49(1) set
[:(dom (D,D,D,d2,d1,F)),{G}:] is Relation-like set
<:(D,D,D,d2,d1,F),((dom (D,D,D,d2,d1,F)) --> G):> is Relation-like Function-like set
<:(D,D,D,d2,d1,F),((dom (D,D,D,d2,d1,F)) --> G):> * d2 is Relation-like D -valued Function-like set
<*> D is Relation-like non-empty empty-yielding K155() -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
[:K155(),D:] is Relation-like non empty V42() set
Seg u is V42() V49(u) Element of bool K155()
d3 is non empty set
[:d3,D:] is Relation-like non empty set
bool [:d3,D:] is non empty set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is V31() V32() V33() V37() V38() V41() V42() V47() set
G is Relation-like K155() -defined D -valued Function-like V42() V49(F) FinSequence-like FinSubsequence-like FinSequence of D
u is Relation-like K155() -defined D -valued Function-like V42() V49(F) FinSequence-like FinSubsequence-like FinSequence of D
d1 is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
(D,D,D,d1,G,u) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:G,u:> is Relation-like Function-like set
<:G,u:> * d1 is Relation-like D -valued Function-like set
(D,D,D,d1,u,G) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:u,G:> is Relation-like Function-like set
<:u,G:> * d1 is Relation-like D -valued Function-like set
<*> D is Relation-like non-empty empty-yielding K155() -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
[:K155(),D:] is Relation-like non empty V42() set
Seg F is V42() V49(F) Element of bool K155()
d2 is non empty set
[:d2,D:] is Relation-like non empty set
bool [:d2,D:] is non empty set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is Element of D
G is V31() V32() V33() V37() V38() V41() V42() V47() set
u is Relation-like K155() -defined D -valued Function-like V42() V49(G) FinSequence-like FinSubsequence-like FinSequence of D
d1 is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
(D,D,D,d1,F,u) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
dom u is V49(G) set
(dom u) --> F is Relation-like dom u -defined D -valued Function-like constant total set
{F} is non empty trivial V49(1) set
[:(dom u),{F}:] is Relation-like set
<:((dom u) --> F),u:> is Relation-like Function-like set
<:((dom u) --> F),u:> * d1 is Relation-like D -valued Function-like set
(D,D,D,d1,u,F) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:u,((dom u) --> F):> is Relation-like Function-like set
<:u,((dom u) --> F):> * d1 is Relation-like D -valued Function-like set
<*> D is Relation-like non-empty empty-yielding K155() -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
[:K155(),D:] is Relation-like non empty V42() set
Seg G is V42() V49(G) Element of bool K155()
d2 is non empty set
[:d2,D:] is Relation-like non empty set
bool [:d2,D:] is non empty set
D is non empty set
F is non empty set
[:D,F:] is Relation-like non empty set
bool [:D,F:] is non empty set
[:F,F:] is Relation-like non empty set
[:[:F,F:],F:] is Relation-like non empty set
bool [:[:F,F:],F:] is non empty set
G is Element of F
u is Element of F
d1 is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
d2 is Relation-like [:F,F:] -defined F -valued Function-like non empty total V18([:F,F:],F) Element of bool [:[:F,F:],F:]
d2 [;] (G,d1) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
dom d1 is non empty set
(dom d1) --> G is Relation-like dom d1 -defined F -valued Function-like constant non empty total set
{G} is non empty trivial V49(1) set
[:(dom d1),{G}:] is Relation-like non empty set
<:((dom d1) --> G),d1:> is Relation-like Function-like set
<:((dom d1) --> G),d1:> * d2 is Relation-like F -valued Function-like set
d2 [;] (u,d1) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
(dom d1) --> u is Relation-like dom d1 -defined F -valued Function-like constant non empty total set
{u} is non empty trivial V49(1) set
[:(dom d1),{u}:] is Relation-like non empty set
<:((dom d1) --> u),d1:> is Relation-like Function-like set
<:((dom d1) --> u),d1:> * d2 is Relation-like F -valued Function-like set
d3 is Relation-like [:F,F:] -defined F -valued Function-like non empty total V18([:F,F:],F) Element of bool [:[:F,F:],F:]
d3 . (G,u) is Element of F
[G,u] is set
d3 . [G,u] is set
d2 [;] ((d3 . (G,u)),d1) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
(dom d1) --> (d3 . (G,u)) is Relation-like dom d1 -defined F -valued Function-like constant non empty total set
{(d3 . (G,u))} is non empty trivial V49(1) set
[:(dom d1),{(d3 . (G,u))}:] is Relation-like non empty set
<:((dom d1) --> (d3 . (G,u))),d1:> is Relation-like Function-like set
<:((dom d1) --> (d3 . (G,u))),d1:> * d2 is Relation-like F -valued Function-like set
d3 .: ((d2 [;] (G,d1)),(d2 [;] (u,d1))) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
<:(d2 [;] (G,d1)),(d2 [;] (u,d1)):> is Relation-like Function-like set
<:(d2 [;] (G,d1)),(d2 [;] (u,d1)):> * d3 is Relation-like F -valued Function-like set
d4 is Element of D
(d2 [;] ((d3 . (G,u)),d1)) . d4 is Element of F
d1 . d4 is Element of F
d2 . ((d3 . (G,u)),(d1 . d4)) is Element of F
[(d3 . (G,u)),(d1 . d4)] is set
d2 . [(d3 . (G,u)),(d1 . d4)] is set
d2 . (G,(d1 . d4)) is Element of F
[G,(d1 . d4)] is set
d2 . [G,(d1 . d4)] is set
d2 . (u,(d1 . d4)) is Element of F
[u,(d1 . d4)] is set
d2 . [u,(d1 . d4)] is set
d3 . ((d2 . (G,(d1 . d4))),(d2 . (u,(d1 . d4)))) is Element of F
[(d2 . (G,(d1 . d4))),(d2 . (u,(d1 . d4)))] is set
d3 . [(d2 . (G,(d1 . d4))),(d2 . (u,(d1 . d4)))] is set
(d2 [;] (G,d1)) . d4 is Element of F
d3 . (((d2 [;] (G,d1)) . d4),(d2 . (u,(d1 . d4)))) is Element of F
[((d2 [;] (G,d1)) . d4),(d2 . (u,(d1 . d4)))] is set
d3 . [((d2 [;] (G,d1)) . d4),(d2 . (u,(d1 . d4)))] is set
(d2 [;] (u,d1)) . d4 is Element of F
d3 . (((d2 [;] (G,d1)) . d4),((d2 [;] (u,d1)) . d4)) is Element of F
[((d2 [;] (G,d1)) . d4),((d2 [;] (u,d1)) . d4)] is set
d3 . [((d2 [;] (G,d1)) . d4),((d2 [;] (u,d1)) . d4)] is set
(d3 .: ((d2 [;] (G,d1)),(d2 [;] (u,d1)))) . d4 is Element of F
D is non empty set
F is non empty set
[:D,F:] is Relation-like non empty set
bool [:D,F:] is non empty set
[:F,F:] is Relation-like non empty set
[:[:F,F:],F:] is Relation-like non empty set
bool [:[:F,F:],F:] is non empty set
G is Element of F
u is Element of F
d1 is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
d2 is Relation-like [:F,F:] -defined F -valued Function-like non empty total V18([:F,F:],F) Element of bool [:[:F,F:],F:]
d2 [:] (d1,G) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
dom d1 is non empty set
(dom d1) --> G is Relation-like dom d1 -defined F -valued Function-like constant non empty total set
{G} is non empty trivial V49(1) set
[:(dom d1),{G}:] is Relation-like non empty set
<:d1,((dom d1) --> G):> is Relation-like Function-like set
<:d1,((dom d1) --> G):> * d2 is Relation-like F -valued Function-like set
d2 [:] (d1,u) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
(dom d1) --> u is Relation-like dom d1 -defined F -valued Function-like constant non empty total set
{u} is non empty trivial V49(1) set
[:(dom d1),{u}:] is Relation-like non empty set
<:d1,((dom d1) --> u):> is Relation-like Function-like set
<:d1,((dom d1) --> u):> * d2 is Relation-like F -valued Function-like set
d3 is Relation-like [:F,F:] -defined F -valued Function-like non empty total V18([:F,F:],F) Element of bool [:[:F,F:],F:]
d3 . (G,u) is Element of F
[G,u] is set
d3 . [G,u] is set
d2 [:] (d1,(d3 . (G,u))) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
(dom d1) --> (d3 . (G,u)) is Relation-like dom d1 -defined F -valued Function-like constant non empty total set
{(d3 . (G,u))} is non empty trivial V49(1) set
[:(dom d1),{(d3 . (G,u))}:] is Relation-like non empty set
<:d1,((dom d1) --> (d3 . (G,u))):> is Relation-like Function-like set
<:d1,((dom d1) --> (d3 . (G,u))):> * d2 is Relation-like F -valued Function-like set
d3 .: ((d2 [:] (d1,G)),(d2 [:] (d1,u))) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
<:(d2 [:] (d1,G)),(d2 [:] (d1,u)):> is Relation-like Function-like set
<:(d2 [:] (d1,G)),(d2 [:] (d1,u)):> * d3 is Relation-like F -valued Function-like set
d4 is Element of D
(d2 [:] (d1,(d3 . (G,u)))) . d4 is Element of F
d1 . d4 is Element of F
d2 . ((d1 . d4),(d3 . (G,u))) is Element of F
[(d1 . d4),(d3 . (G,u))] is set
d2 . [(d1 . d4),(d3 . (G,u))] is set
d2 . ((d1 . d4),G) is Element of F
[(d1 . d4),G] is set
d2 . [(d1 . d4),G] is set
d2 . ((d1 . d4),u) is Element of F
[(d1 . d4),u] is set
d2 . [(d1 . d4),u] is set
d3 . ((d2 . ((d1 . d4),G)),(d2 . ((d1 . d4),u))) is Element of F
[(d2 . ((d1 . d4),G)),(d2 . ((d1 . d4),u))] is set
d3 . [(d2 . ((d1 . d4),G)),(d2 . ((d1 . d4),u))] is set
(d2 [:] (d1,G)) . d4 is Element of F
d3 . (((d2 [:] (d1,G)) . d4),(d2 . ((d1 . d4),u))) is Element of F
[((d2 [:] (d1,G)) . d4),(d2 . ((d1 . d4),u))] is set
d3 . [((d2 [:] (d1,G)) . d4),(d2 . ((d1 . d4),u))] is set
(d2 [:] (d1,u)) . d4 is Element of F
d3 . (((d2 [:] (d1,G)) . d4),((d2 [:] (d1,u)) . d4)) is Element of F
[((d2 [:] (d1,G)) . d4),((d2 [:] (d1,u)) . d4)] is set
d3 . [((d2 [:] (d1,G)) . d4),((d2 [:] (d1,u)) . d4)] is set
(d3 .: ((d2 [:] (d1,G)),(d2 [:] (d1,u)))) . d4 is Element of F
D is non empty set
F is non empty set
[:F,F:] is Relation-like non empty set
[:[:F,F:],F:] is Relation-like non empty set
bool [:[:F,F:],F:] is non empty set
G is non empty set
[:D,G:] is Relation-like non empty set
bool [:D,G:] is non empty set
[:G,F:] is Relation-like non empty set
bool [:G,F:] is non empty set
[:G,G:] is Relation-like non empty set
[:[:G,G:],G:] is Relation-like non empty set
bool [:[:G,G:],G:] is non empty set
u is Relation-like D -defined G -valued Function-like non empty total V18(D,G) Element of bool [:D,G:]
d1 is Relation-like D -defined G -valued Function-like non empty total V18(D,G) Element of bool [:D,G:]
d2 is Relation-like G -defined F -valued Function-like non empty total V18(G,F) Element of bool [:G,F:]
d2 * u is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
[:D,F:] is Relation-like non empty set
bool [:D,F:] is non empty set
d2 * d1 is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
d3 is Relation-like [:G,G:] -defined G -valued Function-like non empty total V18([:G,G:],G) Element of bool [:[:G,G:],G:]
d3 .: (u,d1) is Relation-like D -defined G -valued Function-like non empty total V18(D,G) Element of bool [:D,G:]
<:u,d1:> is Relation-like Function-like set
<:u,d1:> * d3 is Relation-like G -valued Function-like set
d2 * (d3 .: (u,d1)) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
d4 is Relation-like [:F,F:] -defined F -valued Function-like non empty total V18([:F,F:],F) Element of bool [:[:F,F:],F:]
d4 .: ((d2 * u),(d2 * d1)) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
<:(d2 * u),(d2 * d1):> is Relation-like Function-like set
<:(d2 * u),(d2 * d1):> * d4 is Relation-like F -valued Function-like set
f is Element of D
(d2 * (d3 .: (u,d1))) . f is Element of F
(d3 .: (u,d1)) . f is Element of G
d2 . ((d3 .: (u,d1)) . f) is Element of F
u . f is Element of G
d1 . f is Element of G
d3 . ((u . f),(d1 . f)) is Element of G
[(u . f),(d1 . f)] is set
d3 . [(u . f),(d1 . f)] is set
d2 . (d3 . ((u . f),(d1 . f))) is Element of F
d2 . (u . f) is Element of F
d2 . (d1 . f) is Element of F
d4 . ((d2 . (u . f)),(d2 . (d1 . f))) is Element of F
[(d2 . (u . f)),(d2 . (d1 . f))] is set
d4 . [(d2 . (u . f)),(d2 . (d1 . f))] is set
(d2 * u) . f is Element of F
d4 . (((d2 * u) . f),(d2 . (d1 . f))) is Element of F
[((d2 * u) . f),(d2 . (d1 . f))] is set
d4 . [((d2 * u) . f),(d2 . (d1 . f))] is set
(d2 * d1) . f is Element of F
d4 . (((d2 * u) . f),((d2 * d1) . f)) is Element of F
[((d2 * u) . f),((d2 * d1) . f)] is set
d4 . [((d2 * u) . f),((d2 * d1) . f)] is set
(d4 .: ((d2 * u),(d2 * d1))) . f is Element of F
D is non empty set
F is non empty set
[:F,F:] is Relation-like non empty set
[:[:F,F:],F:] is Relation-like non empty set
bool [:[:F,F:],F:] is non empty set
G is non empty set
[:D,G:] is Relation-like non empty set
bool [:D,G:] is non empty set
[:G,F:] is Relation-like non empty set
bool [:G,F:] is non empty set
[:G,G:] is Relation-like non empty set
[:[:G,G:],G:] is Relation-like non empty set
bool [:[:G,G:],G:] is non empty set
u is Element of G
d1 is Relation-like D -defined G -valued Function-like non empty total V18(D,G) Element of bool [:D,G:]
d2 is Relation-like G -defined F -valued Function-like non empty total V18(G,F) Element of bool [:G,F:]
d2 . u is Element of F
d2 * d1 is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
[:D,F:] is Relation-like non empty set
bool [:D,F:] is non empty set
d3 is Relation-like [:G,G:] -defined G -valued Function-like non empty total V18([:G,G:],G) Element of bool [:[:G,G:],G:]
d3 [;] (u,d1) is Relation-like D -defined G -valued Function-like non empty total V18(D,G) Element of bool [:D,G:]
dom d1 is non empty set
(dom d1) --> u is Relation-like dom d1 -defined G -valued Function-like constant non empty total set
{u} is non empty trivial V49(1) set
[:(dom d1),{u}:] is Relation-like non empty set
<:((dom d1) --> u),d1:> is Relation-like Function-like set
<:((dom d1) --> u),d1:> * d3 is Relation-like G -valued Function-like set
d2 * (d3 [;] (u,d1)) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
d4 is Relation-like [:F,F:] -defined F -valued Function-like non empty total V18([:F,F:],F) Element of bool [:[:F,F:],F:]
d4 [;] ((d2 . u),(d2 * d1)) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
dom (d2 * d1) is non empty set
(dom (d2 * d1)) --> (d2 . u) is Relation-like dom (d2 * d1) -defined F -valued Function-like constant non empty total set
{(d2 . u)} is non empty trivial V49(1) set
[:(dom (d2 * d1)),{(d2 . u)}:] is Relation-like non empty set
<:((dom (d2 * d1)) --> (d2 . u)),(d2 * d1):> is Relation-like Function-like set
<:((dom (d2 * d1)) --> (d2 . u)),(d2 * d1):> * d4 is Relation-like F -valued Function-like set
D --> u is Relation-like D -defined G -valued Function-like constant non empty total V18(D,G) Element of bool [:D,G:]
[:D,{u}:] is Relation-like non empty set
dom d2 is non empty Element of bool G
bool G is non empty set
dom (d2 * d1) is non empty Element of bool D
bool D is non empty set
f is Relation-like D -defined G -valued Function-like non empty total V18(D,G) Element of bool [:D,G:]
d3 .: (f,d1) is Relation-like D -defined G -valued Function-like non empty total V18(D,G) Element of bool [:D,G:]
<:f,d1:> is Relation-like Function-like set
<:f,d1:> * d3 is Relation-like G -valued Function-like set
d2 * (d3 .: (f,d1)) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
d2 * f is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
d4 .: ((d2 * f),(d2 * d1)) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
<:(d2 * f),(d2 * d1):> is Relation-like Function-like set
<:(d2 * f),(d2 * d1):> * d4 is Relation-like F -valued Function-like set
D is non empty set
F is non empty set
[:F,F:] is Relation-like non empty set
[:[:F,F:],F:] is Relation-like non empty set
bool [:[:F,F:],F:] is non empty set
G is non empty set
[:D,G:] is Relation-like non empty set
bool [:D,G:] is non empty set
[:G,F:] is Relation-like non empty set
bool [:G,F:] is non empty set
[:G,G:] is Relation-like non empty set
[:[:G,G:],G:] is Relation-like non empty set
bool [:[:G,G:],G:] is non empty set
u is Element of G
d1 is Relation-like D -defined G -valued Function-like non empty total V18(D,G) Element of bool [:D,G:]
d2 is Relation-like G -defined F -valued Function-like non empty total V18(G,F) Element of bool [:G,F:]
d2 * d1 is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
[:D,F:] is Relation-like non empty set
bool [:D,F:] is non empty set
d2 . u is Element of F
d3 is Relation-like [:G,G:] -defined G -valued Function-like non empty total V18([:G,G:],G) Element of bool [:[:G,G:],G:]
d3 [:] (d1,u) is Relation-like D -defined G -valued Function-like non empty total V18(D,G) Element of bool [:D,G:]
dom d1 is non empty set
(dom d1) --> u is Relation-like dom d1 -defined G -valued Function-like constant non empty total set
{u} is non empty trivial V49(1) set
[:(dom d1),{u}:] is Relation-like non empty set
<:d1,((dom d1) --> u):> is Relation-like Function-like set
<:d1,((dom d1) --> u):> * d3 is Relation-like G -valued Function-like set
d2 * (d3 [:] (d1,u)) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
d4 is Relation-like [:F,F:] -defined F -valued Function-like non empty total V18([:F,F:],F) Element of bool [:[:F,F:],F:]
d4 [:] ((d2 * d1),(d2 . u)) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
dom (d2 * d1) is non empty set
(dom (d2 * d1)) --> (d2 . u) is Relation-like dom (d2 * d1) -defined F -valued Function-like constant non empty total set
{(d2 . u)} is non empty trivial V49(1) set
[:(dom (d2 * d1)),{(d2 . u)}:] is Relation-like non empty set
<:(d2 * d1),((dom (d2 * d1)) --> (d2 . u)):> is Relation-like Function-like set
<:(d2 * d1),((dom (d2 * d1)) --> (d2 . u)):> * d4 is Relation-like F -valued Function-like set
D --> u is Relation-like D -defined G -valued Function-like constant non empty total V18(D,G) Element of bool [:D,G:]
[:D,{u}:] is Relation-like non empty set
dom d2 is non empty Element of bool G
bool G is non empty set
dom (d2 * d1) is non empty Element of bool D
bool D is non empty set
f is Relation-like D -defined G -valued Function-like non empty total V18(D,G) Element of bool [:D,G:]
d3 .: (d1,f) is Relation-like D -defined G -valued Function-like non empty total V18(D,G) Element of bool [:D,G:]
<:d1,f:> is Relation-like Function-like set
<:d1,f:> * d3 is Relation-like G -valued Function-like set
d2 * (d3 .: (d1,f)) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
d2 * f is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
d4 .: ((d2 * d1),(d2 * f)) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
<:(d2 * d1),(d2 * f):> is Relation-like Function-like set
<:(d2 * d1),(d2 * f):> * d4 is Relation-like F -valued Function-like set
D is non empty set
F is non empty set
[:D,F:] is Relation-like non empty set
bool [:D,F:] is non empty set
[:F,F:] is Relation-like non empty set
[:[:F,F:],F:] is Relation-like non empty set
bool [:[:F,F:],F:] is non empty set
bool [:F,F:] is non empty set
G is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
u is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
d1 is Relation-like [:F,F:] -defined F -valued Function-like non empty total V18([:F,F:],F) Element of bool [:[:F,F:],F:]
d1 .: (G,u) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
<:G,u:> is Relation-like Function-like set
<:G,u:> * d1 is Relation-like F -valued Function-like set
d2 is Relation-like F -defined F -valued Function-like non empty total V18(F,F) Element of bool [:F,F:]
d2 * (d1 .: (G,u)) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
d2 * G is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
d2 * u is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
d1 .: ((d2 * G),(d2 * u)) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
<:(d2 * G),(d2 * u):> is Relation-like Function-like set
<:(d2 * G),(d2 * u):> * d1 is Relation-like F -valued Function-like set
D is non empty set
F is non empty set
[:D,F:] is Relation-like non empty set
bool [:D,F:] is non empty set
[:F,F:] is Relation-like non empty set
[:[:F,F:],F:] is Relation-like non empty set
bool [:[:F,F:],F:] is non empty set
bool [:F,F:] is non empty set
G is Element of F
u is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
d1 is Relation-like [:F,F:] -defined F -valued Function-like non empty total V18([:F,F:],F) Element of bool [:[:F,F:],F:]
d1 [;] (G,u) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
dom u is non empty set
(dom u) --> G is Relation-like dom u -defined F -valued Function-like constant non empty total set
{G} is non empty trivial V49(1) set
[:(dom u),{G}:] is Relation-like non empty set
<:((dom u) --> G),u:> is Relation-like Function-like set
<:((dom u) --> G),u:> * d1 is Relation-like F -valued Function-like set
d2 is Relation-like F -defined F -valued Function-like non empty total V18(F,F) Element of bool [:F,F:]
d2 * (d1 [;] (G,u)) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
d2 . G is Element of F
d2 * u is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
d1 [;] ((d2 . G),(d2 * u)) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
dom (d2 * u) is non empty set
(dom (d2 * u)) --> (d2 . G) is Relation-like dom (d2 * u) -defined F -valued Function-like constant non empty total set
{(d2 . G)} is non empty trivial V49(1) set
[:(dom (d2 * u)),{(d2 . G)}:] is Relation-like non empty set
<:((dom (d2 * u)) --> (d2 . G)),(d2 * u):> is Relation-like Function-like set
<:((dom (d2 * u)) --> (d2 . G)),(d2 * u):> * d1 is Relation-like F -valued Function-like set
D is non empty set
F is non empty set
[:D,F:] is Relation-like non empty set
bool [:D,F:] is non empty set
[:F,F:] is Relation-like non empty set
[:[:F,F:],F:] is Relation-like non empty set
bool [:[:F,F:],F:] is non empty set
bool [:F,F:] is non empty set
G is Element of F
u is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
d1 is Relation-like [:F,F:] -defined F -valued Function-like non empty total V18([:F,F:],F) Element of bool [:[:F,F:],F:]
d1 [:] (u,G) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
dom u is non empty set
(dom u) --> G is Relation-like dom u -defined F -valued Function-like constant non empty total set
{G} is non empty trivial V49(1) set
[:(dom u),{G}:] is Relation-like non empty set
<:u,((dom u) --> G):> is Relation-like Function-like set
<:u,((dom u) --> G):> * d1 is Relation-like F -valued Function-like set
d2 is Relation-like F -defined F -valued Function-like non empty total V18(F,F) Element of bool [:F,F:]
d2 * (d1 [:] (u,G)) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
d2 * u is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
d2 . G is Element of F
d1 [:] ((d2 * u),(d2 . G)) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
dom (d2 * u) is non empty set
(dom (d2 * u)) --> (d2 . G) is Relation-like dom (d2 * u) -defined F -valued Function-like constant non empty total set
{(d2 . G)} is non empty trivial V49(1) set
[:(dom (d2 * u)),{(d2 . G)}:] is Relation-like non empty set
<:(d2 * u),((dom (d2 * u)) --> (d2 . G)):> is Relation-like Function-like set
<:(d2 * u),((dom (d2 * u)) --> (d2 . G)):> * d1 is Relation-like F -valued Function-like set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is non empty set
[:F,D:] is Relation-like non empty set
bool [:F,D:] is non empty set
G is Relation-like F -defined D -valued Function-like non empty total V18(F,D) Element of bool [:F,D:]
u is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
the_unity_wrt u is Element of D
F --> (the_unity_wrt u) is Relation-like F -defined D -valued Function-like constant non empty total V18(F,D) Element of bool [:F,D:]
{(the_unity_wrt u)} is non empty trivial V49(1) set
[:F,{(the_unity_wrt u)}:] is Relation-like non empty set
u .: ((F --> (the_unity_wrt u)),G) is Relation-like F -defined D -valued Function-like non empty total V18(F,D) Element of bool [:F,D:]
<:(F --> (the_unity_wrt u)),G:> is Relation-like Function-like set
<:(F --> (the_unity_wrt u)),G:> * u is Relation-like D -valued Function-like set
u .: (G,(F --> (the_unity_wrt u))) is Relation-like F -defined D -valued Function-like non empty total V18(F,D) Element of bool [:F,D:]
<:G,(F --> (the_unity_wrt u)):> is Relation-like Function-like set
<:G,(F --> (the_unity_wrt u)):> * u is Relation-like D -valued Function-like set
d2 is Relation-like F -defined D -valued Function-like non empty total V18(F,D) Element of bool [:F,D:]
u .: (d2,G) is Relation-like F -defined D -valued Function-like non empty total V18(F,D) Element of bool [:F,D:]
<:d2,G:> is Relation-like Function-like set
<:d2,G:> * u is Relation-like D -valued Function-like set
d3 is Element of F
(u .: (d2,G)) . d3 is Element of D
d2 . d3 is Element of D
G . d3 is Element of D
u . ((d2 . d3),(G . d3)) is Element of D
[(d2 . d3),(G . d3)] is set
u . [(d2 . d3),(G . d3)] is set
u . ((the_unity_wrt u),(G . d3)) is Element of D
[(the_unity_wrt u),(G . d3)] is set
u . [(the_unity_wrt u),(G . d3)] is set
u .: (G,d2) is Relation-like F -defined D -valued Function-like non empty total V18(F,D) Element of bool [:F,D:]
<:G,d2:> is Relation-like Function-like set
<:G,d2:> * u is Relation-like D -valued Function-like set
d3 is Element of F
(u .: (G,d2)) . d3 is Element of D
G . d3 is Element of D
d2 . d3 is Element of D
u . ((G . d3),(d2 . d3)) is Element of D
[(G . d3),(d2 . d3)] is set
u . [(G . d3),(d2 . d3)] is set
u . ((G . d3),(the_unity_wrt u)) is Element of D
[(G . d3),(the_unity_wrt u)] is set
u . [(G . d3),(the_unity_wrt u)] is set
D is non empty set
F is non empty set
[:D,F:] is Relation-like non empty set
bool [:D,F:] is non empty set
[:F,F:] is Relation-like non empty set
[:[:F,F:],F:] is Relation-like non empty set
bool [:[:F,F:],F:] is non empty set
G is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
u is Relation-like [:F,F:] -defined F -valued Function-like non empty total V18([:F,F:],F) Element of bool [:[:F,F:],F:]
the_unity_wrt u is Element of F
u [;] ((the_unity_wrt u),G) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
dom G is non empty set
(dom G) --> (the_unity_wrt u) is Relation-like dom G -defined F -valued Function-like constant non empty total set
{(the_unity_wrt u)} is non empty trivial V49(1) set
[:(dom G),{(the_unity_wrt u)}:] is Relation-like non empty set
<:((dom G) --> (the_unity_wrt u)),G:> is Relation-like Function-like set
<:((dom G) --> (the_unity_wrt u)),G:> * u is Relation-like F -valued Function-like set
d2 is Element of D
(u [;] ((the_unity_wrt u),G)) . d2 is Element of F
G . d2 is Element of F
u . ((the_unity_wrt u),(G . d2)) is Element of F
[(the_unity_wrt u),(G . d2)] is set
u . [(the_unity_wrt u),(G . d2)] is set
D is non empty set
F is non empty set
[:D,F:] is Relation-like non empty set
bool [:D,F:] is non empty set
[:F,F:] is Relation-like non empty set
[:[:F,F:],F:] is Relation-like non empty set
bool [:[:F,F:],F:] is non empty set
G is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
u is Relation-like [:F,F:] -defined F -valued Function-like non empty total V18([:F,F:],F) Element of bool [:[:F,F:],F:]
the_unity_wrt u is Element of F
u [:] (G,(the_unity_wrt u)) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
dom G is non empty set
(dom G) --> (the_unity_wrt u) is Relation-like dom G -defined F -valued Function-like constant non empty total set
{(the_unity_wrt u)} is non empty trivial V49(1) set
[:(dom G),{(the_unity_wrt u)}:] is Relation-like non empty set
<:G,((dom G) --> (the_unity_wrt u)):> is Relation-like Function-like set
<:G,((dom G) --> (the_unity_wrt u)):> * u is Relation-like F -valued Function-like set
d2 is Element of D
(u [:] (G,(the_unity_wrt u))) . d2 is Element of F
G . d2 is Element of F
u . ((G . d2),(the_unity_wrt u)) is Element of F
[(G . d2),(the_unity_wrt u)] is set
u . [(G . d2),(the_unity_wrt u)] is set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is Element of D
G is Element of D
u is V31() V32() V33() V37() V38() V41() V42() V47() set
d1 is Relation-like K155() -defined D -valued Function-like V42() V49(u) FinSequence-like FinSubsequence-like FinSequence of D
d2 is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
(D,D,D,d2,F,d1) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
dom d1 is V49(u) set
(dom d1) --> F is Relation-like dom d1 -defined D -valued Function-like constant total set
{F} is non empty trivial V49(1) set
[:(dom d1),{F}:] is Relation-like set
<:((dom d1) --> F),d1:> is Relation-like Function-like set
<:((dom d1) --> F),d1:> * d2 is Relation-like D -valued Function-like set
(D,D,D,d2,G,d1) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
(dom d1) --> G is Relation-like dom d1 -defined D -valued Function-like constant total set
{G} is non empty trivial V49(1) set
[:(dom d1),{G}:] is Relation-like set
<:((dom d1) --> G),d1:> is Relation-like Function-like set
<:((dom d1) --> G),d1:> * d2 is Relation-like D -valued Function-like set
d3 is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
d3 . (F,G) is Element of D
[F,G] is set
d3 . [F,G] is set
(D,D,D,d2,(d3 . (F,G)),d1) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
(dom d1) --> (d3 . (F,G)) is Relation-like dom d1 -defined D -valued Function-like constant total set
{(d3 . (F,G))} is non empty trivial V49(1) set
[:(dom d1),{(d3 . (F,G))}:] is Relation-like set
<:((dom d1) --> (d3 . (F,G))),d1:> is Relation-like Function-like set
<:((dom d1) --> (d3 . (F,G))),d1:> * d2 is Relation-like D -valued Function-like set
(D,D,D,d3,(D,D,D,d2,F,d1),(D,D,D,d2,G,d1)) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:(D,D,D,d2,F,d1),(D,D,D,d2,G,d1):> is Relation-like Function-like set
<:(D,D,D,d2,F,d1),(D,D,D,d2,G,d1):> * d3 is Relation-like D -valued Function-like set
<*> D is Relation-like non-empty empty-yielding K155() -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
[:K155(),D:] is Relation-like non empty V42() set
Seg u is V42() V49(u) Element of bool K155()
d4 is non empty set
[:d4,D:] is Relation-like non empty set
bool [:d4,D:] is non empty set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is Element of D
G is Element of D
u is V31() V32() V33() V37() V38() V41() V42() V47() set
d1 is Relation-like K155() -defined D -valued Function-like V42() V49(u) FinSequence-like FinSubsequence-like FinSequence of D
d2 is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
(D,D,D,d2,d1,F) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
dom d1 is V49(u) set
(dom d1) --> F is Relation-like dom d1 -defined D -valued Function-like constant total set
{F} is non empty trivial V49(1) set
[:(dom d1),{F}:] is Relation-like set
<:d1,((dom d1) --> F):> is Relation-like Function-like set
<:d1,((dom d1) --> F):> * d2 is Relation-like D -valued Function-like set
(D,D,D,d2,d1,G) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
(dom d1) --> G is Relation-like dom d1 -defined D -valued Function-like constant total set
{G} is non empty trivial V49(1) set
[:(dom d1),{G}:] is Relation-like set
<:d1,((dom d1) --> G):> is Relation-like Function-like set
<:d1,((dom d1) --> G):> * d2 is Relation-like D -valued Function-like set
d3 is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
d3 . (F,G) is Element of D
[F,G] is set
d3 . [F,G] is set
(D,D,D,d2,d1,(d3 . (F,G))) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
(dom d1) --> (d3 . (F,G)) is Relation-like dom d1 -defined D -valued Function-like constant total set
{(d3 . (F,G))} is non empty trivial V49(1) set
[:(dom d1),{(d3 . (F,G))}:] is Relation-like set
<:d1,((dom d1) --> (d3 . (F,G))):> is Relation-like Function-like set
<:d1,((dom d1) --> (d3 . (F,G))):> * d2 is Relation-like D -valued Function-like set
(D,D,D,d3,(D,D,D,d2,d1,F),(D,D,D,d2,d1,G)) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:(D,D,D,d2,d1,F),(D,D,D,d2,d1,G):> is Relation-like Function-like set
<:(D,D,D,d2,d1,F),(D,D,D,d2,d1,G):> * d3 is Relation-like D -valued Function-like set
<*> D is Relation-like non-empty empty-yielding K155() -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
[:K155(),D:] is Relation-like non empty V42() set
Seg u is V42() V49(u) Element of bool K155()
d4 is non empty set
[:d4,D:] is Relation-like non empty set
bool [:d4,D:] is non empty set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is non empty set
[:F,D:] is Relation-like non empty set
bool [:F,D:] is non empty set
[:F,F:] is Relation-like non empty set
[:[:F,F:],F:] is Relation-like non empty set
bool [:[:F,F:],F:] is non empty set
G is V31() V32() V33() V37() V38() V41() V42() V47() set
u is Relation-like F -defined D -valued Function-like non empty total V18(F,D) Element of bool [:F,D:]
d1 is Relation-like K155() -defined F -valued Function-like V42() V49(G) FinSequence-like FinSubsequence-like FinSequence of F
(F,D,d1,u) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
d2 is Relation-like K155() -defined F -valued Function-like V42() V49(G) FinSequence-like FinSubsequence-like FinSequence of F
(F,D,d2,u) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
d3 is Relation-like [:F,F:] -defined F -valued Function-like non empty total V18([:F,F:],F) Element of bool [:[:F,F:],F:]
(F,F,F,d3,d1,d2) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
<:d1,d2:> is Relation-like Function-like set
<:d1,d2:> * d3 is Relation-like F -valued Function-like set
(F,D,(F,F,F,d3,d1,d2),u) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
d4 is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
(D,D,D,d4,(F,D,d1,u),(F,D,d2,u)) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:(F,D,d1,u),(F,D,d2,u):> is Relation-like Function-like set
<:(F,D,d1,u),(F,D,d2,u):> * d4 is Relation-like D -valued Function-like set
<*> F is Relation-like non-empty empty-yielding K155() -defined F -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of F
[:K155(),F:] is Relation-like non empty V42() set
<*> D is Relation-like non-empty empty-yielding K155() -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
[:K155(),D:] is Relation-like non empty V42() set
Seg G is V42() V49(G) Element of bool K155()
f is non empty set
[:f,F:] is Relation-like non empty set
bool [:f,F:] is non empty set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is non empty set
[:F,D:] is Relation-like non empty set
bool [:F,D:] is non empty set
[:F,F:] is Relation-like non empty set
[:[:F,F:],F:] is Relation-like non empty set
bool [:[:F,F:],F:] is non empty set
G is Element of F
u is V31() V32() V33() V37() V38() V41() V42() V47() set
d1 is Relation-like F -defined D -valued Function-like non empty total V18(F,D) Element of bool [:F,D:]
d1 . G is Element of D
d2 is Relation-like K155() -defined F -valued Function-like V42() V49(u) FinSequence-like FinSubsequence-like FinSequence of F
(F,D,d2,d1) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
d3 is Relation-like [:F,F:] -defined F -valued Function-like non empty total V18([:F,F:],F) Element of bool [:[:F,F:],F:]
(F,F,F,d3,G,d2) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
dom d2 is V49(u) set
(dom d2) --> G is Relation-like dom d2 -defined F -valued Function-like constant total set
{G} is non empty trivial V49(1) set
[:(dom d2),{G}:] is Relation-like set
<:((dom d2) --> G),d2:> is Relation-like Function-like set
<:((dom d2) --> G),d2:> * d3 is Relation-like F -valued Function-like set
(F,D,(F,F,F,d3,G,d2),d1) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
d4 is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
(D,D,D,d4,(d1 . G),(F,D,d2,d1)) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
dom (F,D,d2,d1) is set
(dom (F,D,d2,d1)) --> (d1 . G) is Relation-like dom (F,D,d2,d1) -defined D -valued Function-like constant total set
{(d1 . G)} is non empty trivial V49(1) set
[:(dom (F,D,d2,d1)),{(d1 . G)}:] is Relation-like set
<:((dom (F,D,d2,d1)) --> (d1 . G)),(F,D,d2,d1):> is Relation-like Function-like set
<:((dom (F,D,d2,d1)) --> (d1 . G)),(F,D,d2,d1):> * d4 is Relation-like D -valued Function-like set
<*> F is Relation-like non-empty empty-yielding K155() -defined F -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of F
[:K155(),F:] is Relation-like non empty V42() set
<*> D is Relation-like non-empty empty-yielding K155() -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
[:K155(),D:] is Relation-like non empty V42() set
Seg u is V42() V49(u) Element of bool K155()
f is non empty set
[:f,F:] is Relation-like non empty set
bool [:f,F:] is non empty set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is non empty set
[:F,D:] is Relation-like non empty set
bool [:F,D:] is non empty set
[:F,F:] is Relation-like non empty set
[:[:F,F:],F:] is Relation-like non empty set
bool [:[:F,F:],F:] is non empty set
G is Element of F
u is V31() V32() V33() V37() V38() V41() V42() V47() set
d1 is Relation-like F -defined D -valued Function-like non empty total V18(F,D) Element of bool [:F,D:]
d1 . G is Element of D
d2 is Relation-like K155() -defined F -valued Function-like V42() V49(u) FinSequence-like FinSubsequence-like FinSequence of F
(F,D,d2,d1) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
d3 is Relation-like [:F,F:] -defined F -valued Function-like non empty total V18([:F,F:],F) Element of bool [:[:F,F:],F:]
(F,F,F,d3,d2,G) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F
dom d2 is V49(u) set
(dom d2) --> G is Relation-like dom d2 -defined F -valued Function-like constant total set
{G} is non empty trivial V49(1) set
[:(dom d2),{G}:] is Relation-like set
<:d2,((dom d2) --> G):> is Relation-like Function-like set
<:d2,((dom d2) --> G):> * d3 is Relation-like F -valued Function-like set
(F,D,(F,F,F,d3,d2,G),d1) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
d4 is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
(D,D,D,d4,(F,D,d2,d1),(d1 . G)) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
dom (F,D,d2,d1) is set
(dom (F,D,d2,d1)) --> (d1 . G) is Relation-like dom (F,D,d2,d1) -defined D -valued Function-like constant total set
{(d1 . G)} is non empty trivial V49(1) set
[:(dom (F,D,d2,d1)),{(d1 . G)}:] is Relation-like set
<:(F,D,d2,d1),((dom (F,D,d2,d1)) --> (d1 . G)):> is Relation-like Function-like set
<:(F,D,d2,d1),((dom (F,D,d2,d1)) --> (d1 . G)):> * d4 is Relation-like D -valued Function-like set
<*> F is Relation-like non-empty empty-yielding K155() -defined F -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of F
[:K155(),F:] is Relation-like non empty V42() set
<*> D is Relation-like non-empty empty-yielding K155() -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
[:K155(),D:] is Relation-like non empty V42() set
Seg u is V42() V49(u) Element of bool K155()
f is non empty set
[:f,F:] is Relation-like non empty set
bool [:f,F:] is non empty set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
bool [:D,D:] is non empty set
F is V31() V32() V33() V37() V38() V41() V42() V47() set
G is Relation-like K155() -defined D -valued Function-like V42() V49(F) FinSequence-like FinSubsequence-like FinSequence of D
u is Relation-like K155() -defined D -valued Function-like V42() V49(F) FinSequence-like FinSubsequence-like FinSequence of D
d1 is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
(D,D,D,d1,G,u) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:G,u:> is Relation-like Function-like set
<:G,u:> * d1 is Relation-like D -valued Function-like set
d2 is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
(D,D,(D,D,D,d1,G,u),d2) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
(D,D,G,d2) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
(D,D,u,d2) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
(D,D,D,d1,(D,D,G,d2),(D,D,u,d2)) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:(D,D,G,d2),(D,D,u,d2):> is Relation-like Function-like set
<:(D,D,G,d2),(D,D,u,d2):> * d1 is Relation-like D -valued Function-like set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
bool [:D,D:] is non empty set
F is Element of D
G is V31() V32() V33() V37() V38() V41() V42() V47() set
u is Relation-like K155() -defined D -valued Function-like V42() V49(G) FinSequence-like FinSubsequence-like FinSequence of D
d1 is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
(D,D,D,d1,F,u) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
dom u is V49(G) set
(dom u) --> F is Relation-like dom u -defined D -valued Function-like constant total set
{F} is non empty trivial V49(1) set
[:(dom u),{F}:] is Relation-like set
<:((dom u) --> F),u:> is Relation-like Function-like set
<:((dom u) --> F),u:> * d1 is Relation-like D -valued Function-like set
d2 is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
(D,D,(D,D,D,d1,F,u),d2) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
d2 . F is Element of D
(D,D,u,d2) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
(D,D,D,d1,(d2 . F),(D,D,u,d2)) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
dom (D,D,u,d2) is set
(dom (D,D,u,d2)) --> (d2 . F) is Relation-like dom (D,D,u,d2) -defined D -valued Function-like constant total set
{(d2 . F)} is non empty trivial V49(1) set
[:(dom (D,D,u,d2)),{(d2 . F)}:] is Relation-like set
<:((dom (D,D,u,d2)) --> (d2 . F)),(D,D,u,d2):> is Relation-like Function-like set
<:((dom (D,D,u,d2)) --> (d2 . F)),(D,D,u,d2):> * d1 is Relation-like D -valued Function-like set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
bool [:D,D:] is non empty set
F is Element of D
G is V31() V32() V33() V37() V38() V41() V42() V47() set
u is Relation-like K155() -defined D -valued Function-like V42() V49(G) FinSequence-like FinSubsequence-like FinSequence of D
d1 is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
(D,D,D,d1,u,F) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
dom u is V49(G) set
(dom u) --> F is Relation-like dom u -defined D -valued Function-like constant total set
{F} is non empty trivial V49(1) set
[:(dom u),{F}:] is Relation-like set
<:u,((dom u) --> F):> is Relation-like Function-like set
<:u,((dom u) --> F):> * d1 is Relation-like D -valued Function-like set
d2 is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
(D,D,(D,D,D,d1,u,F),d2) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
(D,D,u,d2) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
d2 . F is Element of D
(D,D,D,d1,(D,D,u,d2),(d2 . F)) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
dom (D,D,u,d2) is set
(dom (D,D,u,d2)) --> (d2 . F) is Relation-like dom (D,D,u,d2) -defined D -valued Function-like constant total set
{(d2 . F)} is non empty trivial V49(1) set
[:(dom (D,D,u,d2)),{(d2 . F)}:] is Relation-like set
<:(D,D,u,d2),((dom (D,D,u,d2)) --> (d2 . F)):> is Relation-like Function-like set
<:(D,D,u,d2),((dom (D,D,u,d2)) --> (d2 . F)):> * d1 is Relation-like D -valued Function-like set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
bool [:D,D:] is non empty set
id D is Relation-like D -defined D -valued Function-like one-to-one non empty total V18(D,D) Element of bool [:D,D:]
F is Element of D
G is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
G [;] (F,(id D)) is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
dom (id D) is non empty set
(dom (id D)) --> F is Relation-like dom (id D) -defined D -valued Function-like constant non empty total set
{F} is non empty trivial V49(1) set
[:(dom (id D)),{F}:] is Relation-like non empty set
<:((dom (id D)) --> F),(id D):> is Relation-like Function-like set
<:((dom (id D)) --> F),(id D):> * G is Relation-like D -valued Function-like set
u is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
d1 is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
d2 is Element of D
d1 . d2 is Element of D
d3 is Element of D
u . (d2,d3) is Element of D
[d2,d3] is set
u . [d2,d3] is set
d1 . (u . (d2,d3)) is Element of D
d1 . d3 is Element of D
u . ((d1 . d2),(d1 . d3)) is Element of D
[(d1 . d2),(d1 . d3)] is set
u . [(d1 . d2),(d1 . d3)] is set
u . (d2,d3) is Element of D
d1 . (u . (d2,d3)) is Element of D
(id D) . (u . (d2,d3)) is Element of D
G . (F,((id D) . (u . (d2,d3)))) is Element of D
[F,((id D) . (u . (d2,d3)))] is set
G . [F,((id D) . (u . (d2,d3)))] is set
G . (F,(u . (d2,d3))) is Element of D
[F,(u . (d2,d3))] is set
G . [F,(u . (d2,d3))] is set
G . (F,d2) is Element of D
[F,d2] is set
G . [F,d2] is set
G . (F,d3) is Element of D
[F,d3] is set
G . [F,d3] is set
u . ((G . (F,d2)),(G . (F,d3))) is Element of D
[(G . (F,d2)),(G . (F,d3))] is set
u . [(G . (F,d2)),(G . (F,d3))] is set
(id D) . d2 is Element of D
G . (F,((id D) . d2)) is Element of D
[F,((id D) . d2)] is set
G . [F,((id D) . d2)] is set
u . ((G . (F,((id D) . d2))),(G . (F,d3))) is Element of D
[(G . (F,((id D) . d2))),(G . (F,d3))] is set
u . [(G . (F,((id D) . d2))),(G . (F,d3))] is set
(id D) . d3 is Element of D
G . (F,((id D) . d3)) is Element of D
[F,((id D) . d3)] is set
G . [F,((id D) . d3)] is set
u . ((G . (F,((id D) . d2))),(G . (F,((id D) . d3)))) is Element of D
[(G . (F,((id D) . d2))),(G . (F,((id D) . d3)))] is set
u . [(G . (F,((id D) . d2))),(G . (F,((id D) . d3)))] is set
u . ((d1 . d2),(G . (F,((id D) . d3)))) is Element of D
[(d1 . d2),(G . (F,((id D) . d3)))] is set
u . [(d1 . d2),(G . (F,((id D) . d3)))] is set
u . ((d1 . d2),(d1 . d3)) is Element of D
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
bool [:D,D:] is non empty set
id D is Relation-like D -defined D -valued Function-like one-to-one non empty total V18(D,D) Element of bool [:D,D:]
F is Element of D
G is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
G [:] ((id D),F) is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
dom (id D) is non empty set
(dom (id D)) --> F is Relation-like dom (id D) -defined D -valued Function-like constant non empty total set
{F} is non empty trivial V49(1) set
[:(dom (id D)),{F}:] is Relation-like non empty set
<:(id D),((dom (id D)) --> F):> is Relation-like Function-like set
<:(id D),((dom (id D)) --> F):> * G is Relation-like D -valued Function-like set
u is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
d1 is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
d2 is Element of D
d1 . d2 is Element of D
d3 is Element of D
u . (d2,d3) is Element of D
[d2,d3] is set
u . [d2,d3] is set
d1 . (u . (d2,d3)) is Element of D
d1 . d3 is Element of D
u . ((d1 . d2),(d1 . d3)) is Element of D
[(d1 . d2),(d1 . d3)] is set
u . [(d1 . d2),(d1 . d3)] is set
u . (d2,d3) is Element of D
d1 . (u . (d2,d3)) is Element of D
(id D) . (u . (d2,d3)) is Element of D
G . (((id D) . (u . (d2,d3))),F) is Element of D
[((id D) . (u . (d2,d3))),F] is set
G . [((id D) . (u . (d2,d3))),F] is set
G . ((u . (d2,d3)),F) is Element of D
[(u . (d2,d3)),F] is set
G . [(u . (d2,d3)),F] is set
G . (d2,F) is Element of D
[d2,F] is set
G . [d2,F] is set
G . (d3,F) is Element of D
[d3,F] is set
G . [d3,F] is set
u . ((G . (d2,F)),(G . (d3,F))) is Element of D
[(G . (d2,F)),(G . (d3,F))] is set
u . [(G . (d2,F)),(G . (d3,F))] is set
(id D) . d2 is Element of D
G . (((id D) . d2),F) is Element of D
[((id D) . d2),F] is set
G . [((id D) . d2),F] is set
u . ((G . (((id D) . d2),F)),(G . (d3,F))) is Element of D
[(G . (((id D) . d2),F)),(G . (d3,F))] is set
u . [(G . (((id D) . d2),F)),(G . (d3,F))] is set
(id D) . d3 is Element of D
G . (((id D) . d3),F) is Element of D
[((id D) . d3),F] is set
G . [((id D) . d3),F] is set
u . ((G . (((id D) . d2),F)),(G . (((id D) . d3),F))) is Element of D
[(G . (((id D) . d2),F)),(G . (((id D) . d3),F))] is set
u . [(G . (((id D) . d2),F)),(G . (((id D) . d3),F))] is set
u . ((d1 . d2),(G . (((id D) . d3),F))) is Element of D
[(d1 . d2),(G . (((id D) . d3),F))] is set
u . [(d1 . d2),(G . (((id D) . d3),F))] is set
u . ((d1 . d2),(d1 . d3)) is Element of D
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is V31() V32() V33() V37() V38() V41() V42() V47() set
G is Relation-like K155() -defined D -valued Function-like V42() V49(F) FinSequence-like FinSubsequence-like FinSequence of D
u is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
the_unity_wrt u is Element of D
F |-> (the_unity_wrt u) is Relation-like K155() -defined D -valued Function-like V42() V49(F) FinSequence-like FinSubsequence-like Element of F -tuples_on D
F -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
D * is functional non empty FinSequence-membered FinSequenceSet of D
{ b₁ where b₁ is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like Element of D * : len b₁ = F } is set
Seg F is V42() V49(F) Element of bool K155()
(Seg F) --> (the_unity_wrt u) is Relation-like Seg F -defined Seg F -defined D -valued {(the_unity_wrt u)} -valued Function-like constant total total V18( Seg F,{(the_unity_wrt u)}) V42() FinSequence-like FinSubsequence-like Element of bool [:(Seg F),{(the_unity_wrt u)}:]
{(the_unity_wrt u)} is non empty trivial V49(1) set
[:(Seg F),{(the_unity_wrt u)}:] is Relation-like set
bool [:(Seg F),{(the_unity_wrt u)}:] is non empty set
(D,D,D,u,(F |-> (the_unity_wrt u)),G) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:(F |-> (the_unity_wrt u)),G:> is Relation-like Function-like set
<:(F |-> (the_unity_wrt u)),G:> * u is Relation-like D -valued Function-like set
(D,D,D,u,G,(F |-> (the_unity_wrt u))) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:G,(F |-> (the_unity_wrt u)):> is Relation-like Function-like set
<:G,(F |-> (the_unity_wrt u)):> * u is Relation-like D -valued Function-like set
<*> D is Relation-like non-empty empty-yielding K155() -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
[:K155(),D:] is Relation-like non empty V42() set
d1 is non empty set
[:d1,D:] is Relation-like non empty set
bool [:d1,D:] is non empty set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is V31() V32() V33() V37() V38() V41() V42() V47() set
G is Relation-like K155() -defined D -valued Function-like V42() V49(F) FinSequence-like FinSubsequence-like FinSequence of D
u is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
the_unity_wrt u is Element of D
(D,D,D,u,(the_unity_wrt u),G) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
dom G is V49(F) set
(dom G) --> (the_unity_wrt u) is Relation-like dom G -defined D -valued Function-like constant total set
{(the_unity_wrt u)} is non empty trivial V49(1) set
[:(dom G),{(the_unity_wrt u)}:] is Relation-like set
<:((dom G) --> (the_unity_wrt u)),G:> is Relation-like Function-like set
<:((dom G) --> (the_unity_wrt u)),G:> * u is Relation-like D -valued Function-like set
<*> D is Relation-like non-empty empty-yielding K155() -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
[:K155(),D:] is Relation-like non empty V42() set
Seg F is V42() V49(F) Element of bool K155()
d1 is non empty set
[:d1,D:] is Relation-like non empty set
bool [:d1,D:] is non empty set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is V31() V32() V33() V37() V38() V41() V42() V47() set
G is Relation-like K155() -defined D -valued Function-like V42() V49(F) FinSequence-like FinSubsequence-like FinSequence of D
u is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
the_unity_wrt u is Element of D
(D,D,D,u,G,(the_unity_wrt u)) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
dom G is V49(F) set
(dom G) --> (the_unity_wrt u) is Relation-like dom G -defined D -valued Function-like constant total set
{(the_unity_wrt u)} is non empty trivial V49(1) set
[:(dom G),{(the_unity_wrt u)}:] is Relation-like set
<:G,((dom G) --> (the_unity_wrt u)):> is Relation-like Function-like set
<:G,((dom G) --> (the_unity_wrt u)):> * u is Relation-like D -valued Function-like set
<*> D is Relation-like non-empty empty-yielding K155() -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
[:K155(),D:] is Relation-like non empty V42() set
Seg F is V42() V49(F) Element of bool K155()
d1 is non empty set
[:d1,D:] is Relation-like non empty set
bool [:d1,D:] is non empty set
D is non empty set
[:D,D:] is Relation-like non empty set
bool [:D,D:] is non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
bool [:D,D:] is non empty set
the_unity_wrt F is Element of D
u is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
d1 is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
d2 is Element of D
u . d2 is Element of D
d1 . d2 is Element of D
F . ((u . d2),(the_unity_wrt F)) is Element of D
[(u . d2),(the_unity_wrt F)] is set
F . [(u . d2),(the_unity_wrt F)] is set
F . (d2,(d1 . d2)) is Element of D
[d2,(d1 . d2)] is set
F . [d2,(d1 . d2)] is set
F . ((u . d2),(F . (d2,(d1 . d2)))) is Element of D
[(u . d2),(F . (d2,(d1 . d2)))] is set
F . [(u . d2),(F . (d2,(d1 . d2)))] is set
F . ((u . d2),d2) is Element of D
[(u . d2),d2] is set
F . [(u . d2),d2] is set
F . ((F . ((u . d2),d2)),(d1 . d2)) is Element of D
[(F . ((u . d2),d2)),(d1 . d2)] is set
F . [(F . ((u . d2),d2)),(d1 . d2)] is set
F . ((the_unity_wrt F),(d1 . d2)) is Element of D
[(the_unity_wrt F),(d1 . d2)] is set
F . [(the_unity_wrt F),(d1 . d2)] is set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is Element of D
G is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
(D,G) is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
bool [:D,D:] is non empty set
(D,G) . F is Element of D
G . (((D,G) . F),F) is Element of D
[((D,G) . F),F] is set
G . [((D,G) . F),F] is set
the_unity_wrt G is Element of D
G . (F,((D,G) . F)) is Element of D
[F,((D,G) . F)] is set
G . [F,((D,G) . F)] is set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is Element of D
G is Element of D
u is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
u . (F,G) is Element of D
[F,G] is set
u . [F,G] is set
the_unity_wrt u is Element of D
(D,u) is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
bool [:D,D:] is non empty set
(D,u) . G is Element of D
(D,u) . F is Element of D
u . ((u . (F,G)),((D,u) . G)) is Element of D
[(u . (F,G)),((D,u) . G)] is set
u . [(u . (F,G)),((D,u) . G)] is set
u . (G,((D,u) . G)) is Element of D
[G,((D,u) . G)] is set
u . [G,((D,u) . G)] is set
u . (F,(u . (G,((D,u) . G)))) is Element of D
[F,(u . (G,((D,u) . G)))] is set
u . [F,(u . (G,((D,u) . G)))] is set
u . (F,(the_unity_wrt u)) is Element of D
[F,(the_unity_wrt u)] is set
u . [F,(the_unity_wrt u)] is set
u . (((D,u) . F),(u . (F,G))) is Element of D
[((D,u) . F),(u . (F,G))] is set
u . [((D,u) . F),(u . (F,G))] is set
u . (((D,u) . F),F) is Element of D
[((D,u) . F),F] is set
u . [((D,u) . F),F] is set
u . ((u . (((D,u) . F),F)),G) is Element of D
[(u . (((D,u) . F),F)),G] is set
u . [(u . (((D,u) . F),F)),G] is set
u . ((the_unity_wrt u),G) is Element of D
[(the_unity_wrt u),G] is set
u . [(the_unity_wrt u),G] is set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
(D,F) is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
bool [:D,D:] is non empty set
the_unity_wrt F is Element of D
(D,F) . (the_unity_wrt F) is Element of D
F . ((the_unity_wrt F),(the_unity_wrt F)) is Element of D
[(the_unity_wrt F),(the_unity_wrt F)] is set
F . [(the_unity_wrt F),(the_unity_wrt F)] is set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is Element of D
G is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
(D,G) is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
bool [:D,D:] is non empty set
(D,G) . F is Element of D
(D,G) . ((D,G) . F) is Element of D
G . (F,((D,G) . F)) is Element of D
[F,((D,G) . F)] is set
G . [F,((D,G) . F)] is set
the_unity_wrt G is Element of D
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
(D,F) is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
bool [:D,D:] is non empty set
G is Element of D
(D,F) . G is Element of D
u is Element of D
F . (G,u) is Element of D
[G,u] is set
F . [G,u] is set
(D,F) . (F . (G,u)) is Element of D
(D,F) . u is Element of D
F . (((D,F) . G),((D,F) . u)) is Element of D
[((D,F) . G),((D,F) . u)] is set
F . [((D,F) . G),((D,F) . u)] is set
the_unity_wrt F is Element of D
F . (((D,F) . G),((D,F) . u)) is Element of D
F . (G,u) is Element of D
F . ((F . (((D,F) . G),((D,F) . u))),(F . (G,u))) is Element of D
[(F . (((D,F) . G),((D,F) . u))),(F . (G,u))] is set
F . [(F . (((D,F) . G),((D,F) . u))),(F . (G,u))] is set
F . (((D,F) . u),(F . (G,u))) is Element of D
[((D,F) . u),(F . (G,u))] is set
F . [((D,F) . u),(F . (G,u))] is set
F . (((D,F) . G),(F . (((D,F) . u),(F . (G,u))))) is Element of D
[((D,F) . G),(F . (((D,F) . u),(F . (G,u))))] is set
F . [((D,F) . G),(F . (((D,F) . u),(F . (G,u))))] is set
F . (((D,F) . u),G) is Element of D
[((D,F) . u),G] is set
F . [((D,F) . u),G] is set
F . ((F . (((D,F) . u),G)),u) is Element of D
[(F . (((D,F) . u),G)),u] is set
F . [(F . (((D,F) . u),G)),u] is set
F . (((D,F) . G),(F . ((F . (((D,F) . u),G)),u))) is Element of D
[((D,F) . G),(F . ((F . (((D,F) . u),G)),u))] is set
F . [((D,F) . G),(F . ((F . (((D,F) . u),G)),u))] is set
F . (G,((D,F) . u)) is Element of D
[G,((D,F) . u)] is set
F . [G,((D,F) . u)] is set
F . ((F . (G,((D,F) . u))),u) is Element of D
[(F . (G,((D,F) . u))),u] is set
F . [(F . (G,((D,F) . u))),u] is set
F . (((D,F) . G),(F . ((F . (G,((D,F) . u))),u))) is Element of D
[((D,F) . G),(F . ((F . (G,((D,F) . u))),u))] is set
F . [((D,F) . G),(F . ((F . (G,((D,F) . u))),u))] is set
F . (((D,F) . u),u) is Element of D
[((D,F) . u),u] is set
F . [((D,F) . u),u] is set
F . (G,(F . (((D,F) . u),u))) is Element of D
[G,(F . (((D,F) . u),u))] is set
F . [G,(F . (((D,F) . u),u))] is set
F . (((D,F) . G),(F . (G,(F . (((D,F) . u),u))))) is Element of D
[((D,F) . G),(F . (G,(F . (((D,F) . u),u))))] is set
F . [((D,F) . G),(F . (G,(F . (((D,F) . u),u))))] is set
F . (G,(the_unity_wrt F)) is Element of D
[G,(the_unity_wrt F)] is set
F . [G,(the_unity_wrt F)] is set
F . (((D,F) . G),(F . (G,(the_unity_wrt F)))) is Element of D
[((D,F) . G),(F . (G,(the_unity_wrt F)))] is set
F . [((D,F) . G),(F . (G,(the_unity_wrt F)))] is set
F . (((D,F) . G),G) is Element of D
[((D,F) . G),G] is set
F . [((D,F) . G),G] is set
F . ((F . (((D,F) . G),G)),(the_unity_wrt F)) is Element of D
[(F . (((D,F) . G),G)),(the_unity_wrt F)] is set
F . [(F . (((D,F) . G),G)),(the_unity_wrt F)] is set
F . ((the_unity_wrt F),(the_unity_wrt F)) is Element of D
[(the_unity_wrt F),(the_unity_wrt F)] is set
F . [(the_unity_wrt F),(the_unity_wrt F)] is set
(D,F) . (F . (G,u)) is Element of D
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is Element of D
G is Element of D
u is Element of D
d1 is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
d1 . (F,G) is Element of D
[F,G] is set
d1 . [F,G] is set
d1 . (F,u) is Element of D
[F,u] is set
d1 . [F,u] is set
d1 . (G,F) is Element of D
[G,F] is set
d1 . [G,F] is set
d1 . (u,F) is Element of D
[u,F] is set
d1 . [u,F] is set
the_unity_wrt d1 is Element of D
(D,d1) is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
bool [:D,D:] is non empty set
d1 . ((the_unity_wrt d1),G) is Element of D
[(the_unity_wrt d1),G] is set
d1 . [(the_unity_wrt d1),G] is set
(D,d1) . F is Element of D
d1 . (((D,d1) . F),F) is Element of D
[((D,d1) . F),F] is set
d1 . [((D,d1) . F),F] is set
d1 . ((d1 . (((D,d1) . F),F)),G) is Element of D
[(d1 . (((D,d1) . F),F)),G] is set
d1 . [(d1 . (((D,d1) . F),F)),G] is set
d1 . (((D,d1) . F),(d1 . (F,u))) is Element of D
[((D,d1) . F),(d1 . (F,u))] is set
d1 . [((D,d1) . F),(d1 . (F,u))] is set
d1 . ((d1 . (((D,d1) . F),F)),u) is Element of D
[(d1 . (((D,d1) . F),F)),u] is set
d1 . [(d1 . (((D,d1) . F),F)),u] is set
d1 . ((the_unity_wrt d1),u) is Element of D
[(the_unity_wrt d1),u] is set
d1 . [(the_unity_wrt d1),u] is set
d1 . (G,(the_unity_wrt d1)) is Element of D
[G,(the_unity_wrt d1)] is set
d1 . [G,(the_unity_wrt d1)] is set
(D,d1) . F is Element of D
d1 . (F,((D,d1) . F)) is Element of D
[F,((D,d1) . F)] is set
d1 . [F,((D,d1) . F)] is set
d1 . (G,(d1 . (F,((D,d1) . F)))) is Element of D
[G,(d1 . (F,((D,d1) . F)))] is set
d1 . [G,(d1 . (F,((D,d1) . F)))] is set
d1 . ((d1 . (u,F)),((D,d1) . F)) is Element of D
[(d1 . (u,F)),((D,d1) . F)] is set
d1 . [(d1 . (u,F)),((D,d1) . F)] is set
d1 . (u,(d1 . (F,((D,d1) . F)))) is Element of D
[u,(d1 . (F,((D,d1) . F)))] is set
d1 . [u,(d1 . (F,((D,d1) . F)))] is set
d1 . (u,(the_unity_wrt d1)) is Element of D
[u,(the_unity_wrt d1)] is set
d1 . [u,(the_unity_wrt d1)] is set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is Element of D
G is Element of D
u is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
u . (F,G) is Element of D
[F,G] is set
u . [F,G] is set
u . (G,F) is Element of D
[G,F] is set
u . [G,F] is set
the_unity_wrt u is Element of D
u . ((the_unity_wrt u),G) is Element of D
[(the_unity_wrt u),G] is set
u . [(the_unity_wrt u),G] is set
u . (G,(the_unity_wrt u)) is Element of D
[G,(the_unity_wrt u)] is set
u . [G,(the_unity_wrt u)] is set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is Element of D
G is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
the_unity_wrt G is Element of D
u is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
d1 is Element of D
u . (F,d1) is Element of D
[F,d1] is set
u . [F,d1] is set
u . (d1,F) is Element of D
[d1,F] is set
u . [d1,F] is set
G . ((u . (F,d1)),(u . (F,d1))) is Element of D
[(u . (F,d1)),(u . (F,d1))] is set
G . [(u . (F,d1)),(u . (F,d1))] is set
G . (F,F) is Element of D
[F,F] is set
G . [F,F] is set
u . ((G . (F,F)),d1) is Element of D
[(G . (F,F)),d1] is set
u . [(G . (F,F)),d1] is set
G . ((u . (d1,F)),(u . (d1,F))) is Element of D
[(u . (d1,F)),(u . (d1,F))] is set
G . [(u . (d1,F)),(u . (d1,F))] is set
u . (d1,(G . (F,F))) is Element of D
[d1,(G . (F,F))] is set
u . [d1,(G . (F,F))] is set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
bool [:D,D:] is non empty set
F is Element of D
G is Element of D
u is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
(D,u) is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
d1 is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
d1 . (F,G) is Element of D
[F,G] is set
d1 . [F,G] is set
d2 is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
d2 . (d1 . (F,G)) is Element of D
d2 . F is Element of D
d1 . ((d2 . F),G) is Element of D
[(d2 . F),G] is set
d1 . [(d2 . F),G] is set
d2 . G is Element of D
d1 . (F,(d2 . G)) is Element of D
[F,(d2 . G)] is set
d1 . [F,(d2 . G)] is set
the_unity_wrt u is Element of D
u . ((d1 . (F,G)),(d1 . ((d2 . F),G))) is Element of D
[(d1 . (F,G)),(d1 . ((d2 . F),G))] is set
u . [(d1 . (F,G)),(d1 . ((d2 . F),G))] is set
u . (F,(d2 . F)) is Element of D
[F,(d2 . F)] is set
u . [F,(d2 . F)] is set
d1 . ((u . (F,(d2 . F))),G) is Element of D
[(u . (F,(d2 . F))),G] is set
d1 . [(u . (F,(d2 . F))),G] is set
d1 . ((the_unity_wrt u),G) is Element of D
[(the_unity_wrt u),G] is set
d1 . [(the_unity_wrt u),G] is set
u . ((d1 . (F,G)),(d1 . (F,(d2 . G)))) is Element of D
[(d1 . (F,G)),(d1 . (F,(d2 . G)))] is set
u . [(d1 . (F,G)),(d1 . (F,(d2 . G)))] is set
u . (G,(d2 . G)) is Element of D
[G,(d2 . G)] is set
u . [G,(d2 . G)] is set
d1 . (F,(u . (G,(d2 . G)))) is Element of D
[F,(u . (G,(d2 . G)))] is set
d1 . [F,(u . (G,(d2 . G)))] is set
d1 . (F,(the_unity_wrt u)) is Element of D
[F,(the_unity_wrt u)] is set
d1 . [F,(the_unity_wrt u)] is set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
bool [:D,D:] is non empty set
id D is Relation-like D -defined D -valued Function-like one-to-one non empty total V18(D,D) Element of bool [:D,D:]
F is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
(D,F) is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
G is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
the_unity_wrt G is Element of D
u is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
u . (the_unity_wrt G) is Element of D
G [;] ((u . (the_unity_wrt G)),(id D)) is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
dom (id D) is non empty set
(dom (id D)) --> (u . (the_unity_wrt G)) is Relation-like dom (id D) -defined D -valued Function-like constant non empty total set
{(u . (the_unity_wrt G))} is non empty trivial V49(1) set
[:(dom (id D)),{(u . (the_unity_wrt G))}:] is Relation-like non empty set
<:((dom (id D)) --> (u . (the_unity_wrt G))),(id D):> is Relation-like Function-like set
<:((dom (id D)) --> (u . (the_unity_wrt G))),(id D):> * G is Relation-like D -valued Function-like set
d2 is Element of D
(G [;] ((u . (the_unity_wrt G)),(id D))) . d2 is Element of D
u . d2 is Element of D
(id D) . d2 is Element of D
G . ((u . (the_unity_wrt G)),((id D) . d2)) is Element of D
[(u . (the_unity_wrt G)),((id D) . d2)] is set
G . [(u . (the_unity_wrt G)),((id D) . d2)] is set
G . ((u . (the_unity_wrt G)),d2) is Element of D
[(u . (the_unity_wrt G)),d2] is set
G . [(u . (the_unity_wrt G)),d2] is set
G . ((the_unity_wrt G),d2) is Element of D
[(the_unity_wrt G),d2] is set
G . [(the_unity_wrt G),d2] is set
u . (G . ((the_unity_wrt G),d2)) is Element of D
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
id D is Relation-like D -defined D -valued Function-like one-to-one non empty total V18(D,D) Element of bool [:D,D:]
bool [:D,D:] is non empty set
F is Element of D
G is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
the_unity_wrt G is Element of D
u is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
u [;] (F,(id D)) is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
dom (id D) is non empty set
(dom (id D)) --> F is Relation-like dom (id D) -defined D -valued Function-like constant non empty total set
{F} is non empty trivial V49(1) set
[:(dom (id D)),{F}:] is Relation-like non empty set
<:((dom (id D)) --> F),(id D):> is Relation-like Function-like set
<:((dom (id D)) --> F),(id D):> * u is Relation-like D -valued Function-like set
(u [;] (F,(id D))) . (the_unity_wrt G) is Element of D
(D,G) is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
u . (F,(the_unity_wrt G)) is Element of D
[F,(the_unity_wrt G)] is set
u . [F,(the_unity_wrt G)] is set
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
u . (F,(G . ((the_unity_wrt G),(the_unity_wrt G)))) is Element of D
[F,(G . ((the_unity_wrt G),(the_unity_wrt G)))] is set
u . [F,(G . ((the_unity_wrt G),(the_unity_wrt G)))] is set
G . ((u . (F,(the_unity_wrt G))),(u . (F,(the_unity_wrt G)))) is Element of D
[(u . (F,(the_unity_wrt G))),(u . (F,(the_unity_wrt G)))] is set
G . [(u . (F,(the_unity_wrt G))),(u . (F,(the_unity_wrt G)))] is set
(D,G) . (u . (F,(the_unity_wrt G))) is Element of D
G . ((G . ((u . (F,(the_unity_wrt G))),(u . (F,(the_unity_wrt G))))),((D,G) . (u . (F,(the_unity_wrt G))))) is Element of D
[(G . ((u . (F,(the_unity_wrt G))),(u . (F,(the_unity_wrt G))))),((D,G) . (u . (F,(the_unity_wrt G))))] is set
G . [(G . ((u . (F,(the_unity_wrt G))),(u . (F,(the_unity_wrt G))))),((D,G) . (u . (F,(the_unity_wrt G))))] is set
G . ((u . (F,(the_unity_wrt G))),((D,G) . (u . (F,(the_unity_wrt G))))) is Element of D
[(u . (F,(the_unity_wrt G))),((D,G) . (u . (F,(the_unity_wrt G))))] is set
G . [(u . (F,(the_unity_wrt G))),((D,G) . (u . (F,(the_unity_wrt G))))] is set
G . ((u . (F,(the_unity_wrt G))),(G . ((u . (F,(the_unity_wrt G))),((D,G) . (u . (F,(the_unity_wrt G))))))) is Element of D
[(u . (F,(the_unity_wrt G))),(G . ((u . (F,(the_unity_wrt G))),((D,G) . (u . (F,(the_unity_wrt G))))))] is set
G . [(u . (F,(the_unity_wrt G))),(G . ((u . (F,(the_unity_wrt G))),((D,G) . (u . (F,(the_unity_wrt G))))))] is set
G . ((u . (F,(the_unity_wrt G))),(the_unity_wrt G)) is Element of D
[(u . (F,(the_unity_wrt G))),(the_unity_wrt G)] is set
G . [(u . (F,(the_unity_wrt G))),(the_unity_wrt G)] is set
(id D) . (the_unity_wrt G) is Element of D
u . (F,((id D) . (the_unity_wrt G))) is Element of D
[F,((id D) . (the_unity_wrt G))] is set
u . [F,((id D) . (the_unity_wrt G))] is set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
id D is Relation-like D -defined D -valued Function-like one-to-one non empty total V18(D,D) Element of bool [:D,D:]
bool [:D,D:] is non empty set
F is Element of D
G is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
the_unity_wrt G is Element of D
u is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
u [:] ((id D),F) is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
dom (id D) is non empty set
(dom (id D)) --> F is Relation-like dom (id D) -defined D -valued Function-like constant non empty total set
{F} is non empty trivial V49(1) set
[:(dom (id D)),{F}:] is Relation-like non empty set
<:(id D),((dom (id D)) --> F):> is Relation-like Function-like set
<:(id D),((dom (id D)) --> F):> * u is Relation-like D -valued Function-like set
(u [:] ((id D),F)) . (the_unity_wrt G) is Element of D
(D,G) is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
u . ((the_unity_wrt G),F) is Element of D
[(the_unity_wrt G),F] is set
u . [(the_unity_wrt G),F] is set
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
u . ((G . ((the_unity_wrt G),(the_unity_wrt G))),F) is Element of D
[(G . ((the_unity_wrt G),(the_unity_wrt G))),F] is set
u . [(G . ((the_unity_wrt G),(the_unity_wrt G))),F] is set
G . ((u . ((the_unity_wrt G),F)),(u . ((the_unity_wrt G),F))) is Element of D
[(u . ((the_unity_wrt G),F)),(u . ((the_unity_wrt G),F))] is set
G . [(u . ((the_unity_wrt G),F)),(u . ((the_unity_wrt G),F))] is set
(D,G) . (u . ((the_unity_wrt G),F)) is Element of D
G . ((G . ((u . ((the_unity_wrt G),F)),(u . ((the_unity_wrt G),F)))),((D,G) . (u . ((the_unity_wrt G),F)))) is Element of D
[(G . ((u . ((the_unity_wrt G),F)),(u . ((the_unity_wrt G),F)))),((D,G) . (u . ((the_unity_wrt G),F)))] is set
G . [(G . ((u . ((the_unity_wrt G),F)),(u . ((the_unity_wrt G),F)))),((D,G) . (u . ((the_unity_wrt G),F)))] is set
G . ((u . ((the_unity_wrt G),F)),((D,G) . (u . ((the_unity_wrt G),F)))) is Element of D
[(u . ((the_unity_wrt G),F)),((D,G) . (u . ((the_unity_wrt G),F)))] is set
G . [(u . ((the_unity_wrt G),F)),((D,G) . (u . ((the_unity_wrt G),F)))] is set
G . ((u . ((the_unity_wrt G),F)),(G . ((u . ((the_unity_wrt G),F)),((D,G) . (u . ((the_unity_wrt G),F)))))) is Element of D
[(u . ((the_unity_wrt G),F)),(G . ((u . ((the_unity_wrt G),F)),((D,G) . (u . ((the_unity_wrt G),F)))))] is set
G . [(u . ((the_unity_wrt G),F)),(G . ((u . ((the_unity_wrt G),F)),((D,G) . (u . ((the_unity_wrt G),F)))))] is set
G . ((u . ((the_unity_wrt G),F)),(the_unity_wrt G)) is Element of D
[(u . ((the_unity_wrt G),F)),(the_unity_wrt G)] is set
G . [(u . ((the_unity_wrt G),F)),(the_unity_wrt G)] is set
(id D) . (the_unity_wrt G) is Element of D
u . (((id D) . (the_unity_wrt G)),F) is Element of D
[((id D) . (the_unity_wrt G)),F] is set
u . [((id D) . (the_unity_wrt G)),F] is set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is non empty set
[:F,D:] is Relation-like non empty set
bool [:F,D:] is non empty set
G is Relation-like F -defined D -valued Function-like non empty total V18(F,D) Element of bool [:F,D:]
u is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
(D,u) is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
bool [:D,D:] is non empty set
(D,u) * G is Relation-like F -defined D -valued Function-like non empty total V18(F,D) Element of bool [:F,D:]
u .: (G,((D,u) * G)) is Relation-like F -defined D -valued Function-like non empty total V18(F,D) Element of bool [:F,D:]
<:G,((D,u) * G):> is Relation-like Function-like set
<:G,((D,u) * G):> * u is Relation-like D -valued Function-like set
the_unity_wrt u is Element of D
F --> (the_unity_wrt u) is Relation-like F -defined D -valued Function-like constant non empty total V18(F,D) Element of bool [:F,D:]
{(the_unity_wrt u)} is non empty trivial V49(1) set
[:F,{(the_unity_wrt u)}:] is Relation-like non empty set
u .: (((D,u) * G),G) is Relation-like F -defined D -valued Function-like non empty total V18(F,D) Element of bool [:F,D:]
<:((D,u) * G),G:> is Relation-like Function-like set
<:((D,u) * G),G:> * u is Relation-like D -valued Function-like set
d3 is Element of F
(u .: (G,((D,u) * G))) . d3 is Element of D
G . d3 is Element of D
((D,u) * G) . d3 is Element of D
u . ((G . d3),(((D,u) * G) . d3)) is Element of D
[(G . d3),(((D,u) * G) . d3)] is set
u . [(G . d3),(((D,u) * G) . d3)] is set
(D,u) . (G . d3) is Element of D
u . ((G . d3),((D,u) . (G . d3))) is Element of D
[(G . d3),((D,u) . (G . d3))] is set
u . [(G . d3),((D,u) . (G . d3))] is set
d2 is Relation-like F -defined D -valued Function-like non empty total V18(F,D) Element of bool [:F,D:]
d2 . d3 is Element of D
d3 is Element of F
(u .: (((D,u) * G),G)) . d3 is Element of D
((D,u) * G) . d3 is Element of D
G . d3 is Element of D
u . ((((D,u) * G) . d3),(G . d3)) is Element of D
[(((D,u) * G) . d3),(G . d3)] is set
u . [(((D,u) * G) . d3),(G . d3)] is set
(D,u) . (G . d3) is Element of D
u . (((D,u) . (G . d3)),(G . d3)) is Element of D
[((D,u) . (G . d3)),(G . d3)] is set
u . [((D,u) . (G . d3)),(G . d3)] is set
d2 . d3 is Element of D
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is non empty set
[:F,D:] is Relation-like non empty set
bool [:F,D:] is non empty set
G is Relation-like F -defined D -valued Function-like non empty total V18(F,D) Element of bool [:F,D:]
u is Relation-like F -defined D -valued Function-like non empty total V18(F,D) Element of bool [:F,D:]
d1 is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
d1 .: (G,u) is Relation-like F -defined D -valued Function-like non empty total V18(F,D) Element of bool [:F,D:]
<:G,u:> is Relation-like Function-like set
<:G,u:> * d1 is Relation-like D -valued Function-like set
the_unity_wrt d1 is Element of D
F --> (the_unity_wrt d1) is Relation-like F -defined D -valued Function-like constant non empty total V18(F,D) Element of bool [:F,D:]
{(the_unity_wrt d1)} is non empty trivial V49(1) set
[:F,{(the_unity_wrt d1)}:] is Relation-like non empty set
(D,d1) is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
bool [:D,D:] is non empty set
(D,d1) * u is Relation-like F -defined D -valued Function-like non empty total V18(F,D) Element of bool [:F,D:]
(D,d1) * G is Relation-like F -defined D -valued Function-like non empty total V18(F,D) Element of bool [:F,D:]
f is Element of F
G . f is Element of D
u . f is Element of D
d1 . ((G . f),(u . f)) is Element of D
[(G . f),(u . f)] is set
d1 . [(G . f),(u . f)] is set
d4 is Relation-like F -defined D -valued Function-like non empty total V18(F,D) Element of bool [:F,D:]
d4 . f is Element of D
(D,d1) . (u . f) is Element of D
((D,d1) * u) . f is Element of D
f is Element of F
G . f is Element of D
u . f is Element of D
d1 . ((G . f),(u . f)) is Element of D
[(G . f),(u . f)] is set
d1 . [(G . f),(u . f)] is set
d4 . f is Element of D
(D,d1) . (G . f) is Element of D
((D,d1) * G) . f is Element of D
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is V31() V32() V33() V37() V38() V41() V42() V47() set
G is Relation-like K155() -defined D -valued Function-like V42() V49(F) FinSequence-like FinSubsequence-like FinSequence of D
u is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
(D,u) is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
bool [:D,D:] is non empty set
(D,D,G,(D,u)) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
(D,D,D,u,G,(D,D,G,(D,u))) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:G,(D,D,G,(D,u)):> is Relation-like Function-like set
<:G,(D,D,G,(D,u)):> * u is Relation-like D -valued Function-like set
the_unity_wrt u is Element of D
F |-> (the_unity_wrt u) is Relation-like K155() -defined D -valued Function-like V42() V49(F) FinSequence-like FinSubsequence-like Element of F -tuples_on D
F -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
D * is functional non empty FinSequence-membered FinSequenceSet of D
{ b₁ where b₁ is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like Element of D * : len b₁ = F } is set
Seg F is V42() V49(F) Element of bool K155()
(Seg F) --> (the_unity_wrt u) is Relation-like Seg F -defined Seg F -defined D -valued {(the_unity_wrt u)} -valued Function-like constant total total V18( Seg F,{(the_unity_wrt u)}) V42() FinSequence-like FinSubsequence-like Element of bool [:(Seg F),{(the_unity_wrt u)}:]
{(the_unity_wrt u)} is non empty trivial V49(1) set
[:(Seg F),{(the_unity_wrt u)}:] is Relation-like set
bool [:(Seg F),{(the_unity_wrt u)}:] is non empty set
(D,D,D,u,(D,D,G,(D,u)),G) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:(D,D,G,(D,u)),G:> is Relation-like Function-like set
<:(D,D,G,(D,u)),G:> * u is Relation-like D -valued Function-like set
d1 is Relation-like K155() -defined D -valued Function-like V42() V49(F) FinSequence-like FinSubsequence-like Element of F -tuples_on D
(D,D,D,u,G,d1) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:G,d1:> is Relation-like Function-like set
<:G,d1:> * u is Relation-like D -valued Function-like set
<*> D is Relation-like non-empty empty-yielding K155() -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
[:K155(),D:] is Relation-like non empty V42() set
(D,D,D,u,d1,G) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:d1,G:> is Relation-like Function-like set
<:d1,G:> * u is Relation-like D -valued Function-like set
d2 is non empty set
[:d2,D:] is Relation-like non empty set
bool [:d2,D:] is non empty set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is V31() V32() V33() V37() V38() V41() V42() V47() set
G is Relation-like K155() -defined D -valued Function-like V42() V49(F) FinSequence-like FinSubsequence-like FinSequence of D
u is Relation-like K155() -defined D -valued Function-like V42() V49(F) FinSequence-like FinSubsequence-like FinSequence of D
d1 is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
(D,D,D,d1,G,u) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:G,u:> is Relation-like Function-like set
<:G,u:> * d1 is Relation-like D -valued Function-like set
the_unity_wrt d1 is Element of D
F |-> (the_unity_wrt d1) is Relation-like K155() -defined D -valued Function-like V42() V49(F) FinSequence-like FinSubsequence-like Element of F -tuples_on D
F -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
D * is functional non empty FinSequence-membered FinSequenceSet of D
{ b₁ where b₁ is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like Element of D * : len b₁ = F } is set
Seg F is V42() V49(F) Element of bool K155()
(Seg F) --> (the_unity_wrt d1) is Relation-like Seg F -defined Seg F -defined D -valued {(the_unity_wrt d1)} -valued Function-like constant total total V18( Seg F,{(the_unity_wrt d1)}) V42() FinSequence-like FinSubsequence-like Element of bool [:(Seg F),{(the_unity_wrt d1)}:]
{(the_unity_wrt d1)} is non empty trivial V49(1) set
[:(Seg F),{(the_unity_wrt d1)}:] is Relation-like set
bool [:(Seg F),{(the_unity_wrt d1)}:] is non empty set
(D,d1) is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
bool [:D,D:] is non empty set
(D,D,u,(D,d1)) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
(D,D,G,(D,d1)) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<*> D is Relation-like non-empty empty-yielding K155() -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
[:K155(),D:] is Relation-like non empty V42() set
d2 is non empty set
[:d2,D:] is Relation-like non empty set
bool [:d2,D:] is non empty set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is non empty set
[:F,D:] is Relation-like non empty set
bool [:F,D:] is non empty set
G is Element of D
F --> G is Relation-like F -defined D -valued Function-like constant non empty total V18(F,D) Element of bool [:F,D:]
{G} is non empty trivial V49(1) set
[:F,{G}:] is Relation-like non empty set
u is Relation-like F -defined D -valued Function-like non empty total V18(F,D) Element of bool [:F,D:]
d1 is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
the_unity_wrt d1 is Element of D
d2 is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
d2 [;] (G,u) is Relation-like F -defined D -valued Function-like non empty total V18(F,D) Element of bool [:F,D:]
dom u is non empty set
(dom u) --> G is Relation-like dom u -defined D -valued Function-like constant non empty total set
[:(dom u),{G}:] is Relation-like non empty set
<:((dom u) --> G),u:> is Relation-like Function-like set
<:((dom u) --> G),u:> * d2 is Relation-like D -valued Function-like set
d4 is Element of F
(d2 [;] (G,u)) . d4 is Element of D
u . d4 is Element of D
d2 . (G,(u . d4)) is Element of D
[G,(u . d4)] is set
d2 . [G,(u . d4)] is set
d3 is Relation-like F -defined D -valued Function-like non empty total V18(F,D) Element of bool [:F,D:]
d3 . d4 is Element of D
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
F is Element of D
G is V31() V32() V33() V37() V38() V41() V42() V47() set
G |-> F is Relation-like K155() -defined D -valued Function-like V42() V49(G) FinSequence-like FinSubsequence-like Element of G -tuples_on D
G -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
D * is functional non empty FinSequence-membered FinSequenceSet of D
{ b₁ where b₁ is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like Element of D * : len b₁ = G } is set
Seg G is V42() V49(G) Element of bool K155()
(Seg G) --> F is Relation-like Seg G -defined Seg G -defined D -valued {F} -valued Function-like constant total total V18( Seg G,{F}) V42() FinSequence-like FinSubsequence-like Element of bool [:(Seg G),{F}:]
{F} is non empty trivial V49(1) set
[:(Seg G),{F}:] is Relation-like set
bool [:(Seg G),{F}:] is non empty set
u is Relation-like K155() -defined D -valued Function-like V42() V49(G) FinSequence-like FinSubsequence-like FinSequence of D
d1 is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
the_unity_wrt d1 is Element of D
d2 is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
(D,D,D,d2,F,u) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
dom u is V49(G) set
(dom u) --> F is Relation-like dom u -defined D -valued Function-like constant total set
[:(dom u),{F}:] is Relation-like set
<:((dom u) --> F),u:> is Relation-like Function-like set
<:((dom u) --> F),u:> * d2 is Relation-like D -valued Function-like set
<*> D is Relation-like non-empty empty-yielding K155() -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
[:K155(),D:] is Relation-like non empty V42() set
d3 is non empty set
[:d3,D:] is Relation-like non empty set
bool [:d3,D:] is non empty set
F is Relation-like Function-like set
G is Relation-like Function-like set
[:F,G:] is Relation-like Function-like set
D is Relation-like Function-like set
[:F,G:] * D is Relation-like Function-like set
D is set
F is set
[D,F] is set
G is Relation-like Function-like set
u is Relation-like Function-like set
d1 is Relation-like Function-like set
(G,u,d1) is Relation-like Function-like set
[:u,d1:] is Relation-like Function-like set
[:u,d1:] * G is Relation-like Function-like set
dom (G,u,d1) is set
(G,u,d1) . (D,F) is set
(G,u,d1) . [D,F] is set
u . D is set
d1 . F is set
G . ((u . D),(d1 . F)) is set
[(u . D),(d1 . F)] is set
G . [(u . D),(d1 . F)] is set
dom [:u,d1:] is set
dom u is set
dom d1 is set
[:(dom u),(dom d1):] is Relation-like set
[:u,d1:] . (D,F) is set
[:u,d1:] . [D,F] is set
D is set
F is set
[D,F] is set
G is Relation-like Function-like set
u is Relation-like Function-like set
d1 is Relation-like Function-like set
(G,u,d1) is Relation-like Function-like set
[:u,d1:] is Relation-like Function-like set
[:u,d1:] * G is Relation-like Function-like set
dom (G,u,d1) is set
(G,u,d1) . (D,F) is set
(G,u,d1) . [D,F] is set
u . D is set
d1 . F is set
G . ((u . D),(d1 . F)) is set
[(u . D),(d1 . F)] is set
G . [(u . D),(d1 . F)] is set
D is non empty set
F is non empty set
[:D,F:] is Relation-like non empty set
G is non empty set
[:[:D,F:],G:] is Relation-like non empty set
bool [:[:D,F:],G:] is non empty set
u is non empty set
[:u,D:] is Relation-like non empty set
bool [:u,D:] is non empty set
d1 is non empty set
[:d1,F:] is Relation-like non empty set
bool [:d1,F:] is non empty set
[:u,d1:] is Relation-like non empty set
[:[:u,d1:],G:] is Relation-like non empty set
bool [:[:u,d1:],G:] is non empty set
d2 is Relation-like [:D,F:] -defined G -valued Function-like non empty total V18([:D,F:],G) Element of bool [:[:D,F:],G:]
d3 is Relation-like u -defined D -valued Function-like non empty total V18(u,D) Element of bool [:u,D:]
d4 is Relation-like d1 -defined F -valued Function-like non empty total V18(d1,F) Element of bool [:d1,F:]
(d2,d3,d4) is Relation-like Function-like set
[:d3,d4:] is Relation-like Function-like set
[:d3,d4:] * d2 is Relation-like G -valued Function-like set
[:d3,d4:] is Relation-like [:u,d1:] -defined [:D,F:] -valued Function-like non empty total V18([:u,d1:],[:D,F:]) Element of bool [:[:u,d1:],[:D,F:]:]
[:[:u,d1:],[:D,F:]:] is Relation-like non empty set
bool [:[:u,d1:],[:D,F:]:] is non empty set
d2 * [:d3,d4:] is Relation-like [:u,d1:] -defined G -valued Function-like non empty total V18([:u,d1:],G) Element of bool [:[:u,d1:],G:]
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
bool [:D,D:] is non empty set
F is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
G is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
u is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
(F,G,u) is Relation-like Function-like set
[:G,u:] is Relation-like Function-like set
[:G,u:] * F is Relation-like D -valued Function-like set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
bool [:D,D:] is non empty set
F is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
G is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
u is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
(F,G,u) is Relation-like Function-like set
[:G,u:] is Relation-like Function-like set
[:G,u:] * F is Relation-like D -valued Function-like set
D is non empty set
F is non empty set
[:D,F:] is Relation-like non empty set
G is non empty set
[:[:D,F:],G:] is Relation-like non empty set
bool [:[:D,F:],G:] is non empty set
u is non empty set
[:u,D:] is Relation-like non empty set
bool [:u,D:] is non empty set
d1 is non empty set
[:d1,F:] is Relation-like non empty set
bool [:d1,F:] is non empty set
d2 is Element of u
d3 is Element of d1
d4 is Relation-like [:D,F:] -defined G -valued Function-like non empty total V18([:D,F:],G) Element of bool [:[:D,F:],G:]
f is Relation-like u -defined D -valued Function-like non empty total V18(u,D) Element of bool [:u,D:]
f . d2 is Element of D
g is Relation-like d1 -defined F -valued Function-like non empty total V18(d1,F) Element of bool [:d1,F:]
(d4,f,g) is Relation-like Function-like set
[:f,g:] is Relation-like Function-like set
[:f,g:] * d4 is Relation-like G -valued Function-like set
(d4,f,g) . (d2,d3) is set
[d2,d3] is set
(d4,f,g) . [d2,d3] is set
g . d3 is Element of F
d4 . ((f . d2),(g . d3)) is Element of G
[(f . d2),(g . d3)] is set
d4 . [(f . d2),(g . d3)] is set
[:u,d1:] is Relation-like non empty set
[:[:u,d1:],G:] is Relation-like non empty set
bool [:[:u,d1:],G:] is non empty set
dom (d4,f,g) is set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
bool [:D,D:] is non empty set
id D is Relation-like D -defined D -valued Function-like one-to-one non empty total V18(D,D) Element of bool [:D,D:]
F is Element of D
G is Element of D
u is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
d1 is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
(D,u,(id D),d1) is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
[:(id D),d1:] is Relation-like Function-like set
[:(id D),d1:] * u is Relation-like D -valued Function-like set
(D,u,(id D),d1) . (F,G) is Element of D
[F,G] is set
(D,u,(id D),d1) . [F,G] is set
d1 . G is Element of D
u . (F,(d1 . G)) is Element of D
[F,(d1 . G)] is set
u . [F,(d1 . G)] is set
(D,u,d1,(id D)) is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
[:d1,(id D):] is Relation-like Function-like set
[:d1,(id D):] * u is Relation-like D -valued Function-like set
(D,u,d1,(id D)) . (F,G) is Element of D
(D,u,d1,(id D)) . [F,G] is set
d1 . F is Element of D
u . ((d1 . F),G) is Element of D
[(d1 . F),G] is set
u . [(d1 . F),G] is set
(id D) . F is Element of D
(id D) . G is Element of D
D is non empty set
F is non empty set
[:D,F:] is Relation-like non empty set
bool [:D,F:] is non empty set
[:F,F:] is Relation-like non empty set
[:[:F,F:],F:] is Relation-like non empty set
bool [:[:F,F:],F:] is non empty set
bool [:F,F:] is non empty set
id F is Relation-like F -defined F -valued Function-like one-to-one non empty total V18(F,F) Element of bool [:F,F:]
G is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
u is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
d1 is Relation-like [:F,F:] -defined F -valued Function-like non empty total V18([:F,F:],F) Element of bool [:[:F,F:],F:]
d2 is Relation-like F -defined F -valued Function-like non empty total V18(F,F) Element of bool [:F,F:]
(F,d1,(id F),d2) is Relation-like [:F,F:] -defined F -valued Function-like non empty total V18([:F,F:],F) Element of bool [:[:F,F:],F:]
[:(id F),d2:] is Relation-like Function-like set
[:(id F),d2:] * d1 is Relation-like F -valued Function-like set
(F,d1,(id F),d2) .: (G,u) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
<:G,u:> is Relation-like Function-like set
<:G,u:> * (F,d1,(id F),d2) is Relation-like F -valued Function-like set
d2 * u is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
d1 .: (G,(d2 * u)) is Relation-like D -defined F -valued Function-like non empty total V18(D,F) Element of bool [:D,F:]
<:G,(d2 * u):> is Relation-like Function-like set
<:G,(d2 * u):> * d1 is Relation-like F -valued Function-like set
d3 is Element of D
((F,d1,(id F),d2) .: (G,u)) . d3 is Element of F
G . d3 is Element of F
u . d3 is Element of F
(F,d1,(id F),d2) . ((G . d3),(u . d3)) is Element of F
[(G . d3),(u . d3)] is set
(F,d1,(id F),d2) . [(G . d3),(u . d3)] is set
d2 . (u . d3) is Element of F
d1 . ((G . d3),(d2 . (u . d3))) is Element of F
[(G . d3),(d2 . (u . d3))] is set
d1 . [(G . d3),(d2 . (u . d3))] is set
(d2 * u) . d3 is Element of F
d1 . ((G . d3),((d2 * u) . d3)) is Element of F
[(G . d3),((d2 * u) . d3)] is set
d1 . [(G . d3),((d2 * u) . d3)] is set
(d1 .: (G,(d2 * u))) . d3 is Element of F
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
bool [:D,D:] is non empty set
id D is Relation-like D -defined D -valued Function-like one-to-one non empty total V18(D,D) Element of bool [:D,D:]
F is V31() V32() V33() V37() V38() V41() V42() V47() set
G is Relation-like K155() -defined D -valued Function-like V42() V49(F) FinSequence-like FinSubsequence-like FinSequence of D
u is Relation-like K155() -defined D -valued Function-like V42() V49(F) FinSequence-like FinSubsequence-like FinSequence of D
d1 is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
d2 is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
(D,d1,(id D),d2) is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
[:(id D),d2:] is Relation-like Function-like set
[:(id D),d2:] * d1 is Relation-like D -valued Function-like set
(D,D,D,(D,d1,(id D),d2),G,u) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:G,u:> is Relation-like Function-like set
<:G,u:> * (D,d1,(id D),d2) is Relation-like D -valued Function-like set
(D,D,u,d2) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
(D,D,D,d1,G,(D,D,u,d2)) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D
<:G,(D,D,u,d2):> is Relation-like Function-like set
<:G,(D,D,u,d2):> * d1 is Relation-like D -valued Function-like set
<*> D is Relation-like non-empty empty-yielding K155() -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V25() V31() V32() V33() V35() V36() V37() V38() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
[:K155(),D:] is Relation-like non empty V42() set
Seg F is V42() V49(F) Element of bool K155()
d3 is non empty set
[:d3,D:] is Relation-like non empty set
bool [:d3,D:] is non empty set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
bool [:D,D:] is non empty set
id D is Relation-like D -defined D -valued Function-like one-to-one non empty total V18(D,D) Element of bool [:D,D:]
F is Element of D
G is Element of D
u is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
(D,u) is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
d1 is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
(D,u,(id D),d1) is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
[:(id D),d1:] is Relation-like Function-like set
[:(id D),d1:] * u is Relation-like D -valued Function-like set
(D,u,(id D),d1) . (F,G) is Element of D
[F,G] is set
(D,u,(id D),d1) . [F,G] is set
d1 . ((D,u,(id D),d1) . (F,G)) is Element of D
(D,u,d1,(id D)) is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
[:d1,(id D):] is Relation-like Function-like set
[:d1,(id D):] * u is Relation-like D -valued Function-like set
(D,u,d1,(id D)) . (F,G) is Element of D
(D,u,d1,(id D)) . [F,G] is set
d1 . ((D,u,d1,(id D)) . (F,G)) is Element of D
d1 . G is Element of D
u . (F,(d1 . G)) is Element of D
[F,(d1 . G)] is set
u . [F,(d1 . G)] is set
d1 . (u . (F,(d1 . G))) is Element of D
d1 . F is Element of D
d1 . (d1 . G) is Element of D
u . ((d1 . F),(d1 . (d1 . G))) is Element of D
[(d1 . F),(d1 . (d1 . G))] is set
u . [(d1 . F),(d1 . (d1 . G))] is set
u . ((d1 . F),G) is Element of D
[(d1 . F),G] is set
u . [(d1 . F),G] is set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
id D is Relation-like D -defined D -valued Function-like one-to-one non empty total V18(D,D) Element of bool [:D,D:]
bool [:D,D:] is non empty set
F is Element of D
G is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
(D,G) is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
(D,G,(id D),(D,G)) is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
[:(id D),(D,G):] is Relation-like Function-like set
[:(id D),(D,G):] * G is Relation-like D -valued Function-like set
(D,G,(id D),(D,G)) . (F,F) is Element of D
[F,F] is set
(D,G,(id D),(D,G)) . [F,F] is set
the_unity_wrt G is Element of D
(D,G) . F is Element of D
G . (F,((D,G) . F)) is Element of D
[F,((D,G) . F)] is set
G . [F,((D,G) . F)] is set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
id D is Relation-like D -defined D -valued Function-like one-to-one non empty total V18(D,D) Element of bool [:D,D:]
bool [:D,D:] is non empty set
F is Element of D
G is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
(D,G) is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
(D,G,(id D),(D,G)) is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
[:(id D),(D,G):] is Relation-like Function-like set
[:(id D),(D,G):] * G is Relation-like D -valued Function-like set
the_unity_wrt G is Element of D
(D,G,(id D),(D,G)) . (F,(the_unity_wrt G)) is Element of D
[F,(the_unity_wrt G)] is set
(D,G,(id D),(D,G)) . [F,(the_unity_wrt G)] is set
(D,G) . (the_unity_wrt G) is Element of D
G . (F,((D,G) . (the_unity_wrt G))) is Element of D
[F,((D,G) . (the_unity_wrt G))] is set
G . [F,((D,G) . (the_unity_wrt G))] is set
G . (F,(the_unity_wrt G)) is Element of D
G . [F,(the_unity_wrt G)] is set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
bool [:D,D:] is non empty set
id D is Relation-like D -defined D -valued Function-like one-to-one non empty total V18(D,D) Element of bool [:D,D:]
F is Element of D
G is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
the_unity_wrt G is Element of D
u is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
(D,G,(id D),u) is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
[:(id D),u:] is Relation-like Function-like set
[:(id D),u:] * G is Relation-like D -valued Function-like set
(D,G,(id D),u) . ((the_unity_wrt G),F) is Element of D
[(the_unity_wrt G),F] is set
(D,G,(id D),u) . [(the_unity_wrt G),F] is set
u . F is Element of D
G . ((the_unity_wrt G),(u . F)) is Element of D
[(the_unity_wrt G),(u . F)] is set
G . [(the_unity_wrt G),(u . F)] is set
D is non empty set
[:D,D:] is Relation-like non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
id D is Relation-like D -defined D -valued Function-like one-to-one non empty total V18(D,D) Element of bool [:D,D:]
bool [:D,D:] is non empty set
F is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
(D,F) is Relation-like D -defined D -valued Function-like non empty total V18(D,D) Element of bool [:D,D:]
(D,F,(id D),(D,F)) is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
[:(id D),(D,F):] is Relation-like Function-like set
[:(id D),(D,F):] * F is Relation-like D -valued Function-like set
G is Relation-like [:D,D:] -defined D -valued Function-like non empty total V18([:D,D:],D) Element of bool [:[:D,D:],D:]
d1 is Element of D
d2 is Element of D
G . (d1,d2) is Element of D
[d1,d2] is set
G . [d1,d2] is set
d3 is Element of D
F . (d1,d3) is Element of D
[d1,d3] is set
F . [d1,d3] is set
d4 is Element of D
G . (d3,d4) is Element of D
[d3,d4] is set
G . [d3,d4] is set
F . ((G . (d1,d2)),(G . (d3,d4))) is Element of D
[(G . (d1,d2)),(G . (d3,d4))] is set
F . [(G . (d1,d2)),(G . (d3,d4))] is set
F . (d2,d4) is Element of D
[d2,d4] is set
F . [d2,d4] is set
G . ((F . (d1,d3)),(F . (d2,d4))) is Element of D
[(F . (d1,d3)),(F . (d2,d4))] is set
G . [(F . (d1,d3)),(F . (d2,d4))] is set
(D,F) . d2 is Element of D
F . (d1,((D,F) . d2)) is Element of D
[d1,((D,F) . d2)] is set
F . [d1,((D,F) . d2)] is set
F . ((F . (d1,((D,F) . d2))),(G . (d3,d4))) is Element of D
[(F . (d1,((D,F) . d2))),(G . (d3,d4))] is set
F . [(F . (d1,((D,F) . d2))),(G . (d3,d4))] is set
(D,F) . d4 is Element of D
F . (d3,((D,F) . d4)) is Element of D
[d3,((D,F) . d4)] is set
F . [d3,((D,F) . d4)] is set
F . ((F . (d1,((D,F) . d2))),(F . (d3,((D,F) . d4)))) is Element of D
[(F . (d1,((D,F) . d2))),(F . (d3,((D,F) . d4)))] is set
F . [(F . (d1,((D,F) . d2))),(F . (d3,((D,F) . d4)))] is set
F . (((D,F) . d2),(F . (d3,((D,F) . d4)))) is Element of D
[((D,F) . d2),(F . (d3,((D,F) . d4)))] is set
F . [((D,F) . d2),(F . (d3,((D,F) . d4)))] is set
F . (d1,(F . (((D,F) . d2),(F . (d3,((D,F) . d4)))))) is Element of D
[d1,(F . (((D,F) . d2),(F . (d3,((D,F) . d4)))))] is set
F . [d1,(F . (((D,F) . d2),(F . (d3,((D,F) . d4)))))] is set
F . (((D,F) . d2),d3) is Element of D
[((D,F) . d2),d3] is set
F . [((D,F) . d2),d3] is set
F . ((F . (((D,F) . d2),d3)),((D,F) . d4)) is Element of D
[(F . (((D,F) . d2),d3)),((D,F) . d4)] is set
F . [(F . (((D,F) . d2),d3)),((D,F) . d4)] is set
F . (d1,(F . ((F . (((D,F) . d2),d3)),((D,F) . d4)))) is Element of D
[d1,(F . ((F . (((D,F) . d2),d3)),((D,F) . d4)))] is set
F . [d1,(F . ((F . (((D,F) . d2),d3)),((D,F) . d4)))] is set
F . (d3,((D,F) . d2)) is Element of D
[d3,((D,F) . d2)] is set
F . [d3,((D,F) . d2)] is set
F . ((F . (d3,((D,F) . d2))),((D,F) . d4)) is Element of D
[(F . (d3,((D,F) . d2))),((D,F) . d4)] is set
F . [(F . (d3,((D,F) . d2))),((D,F) . d4)] is set
F . (d1,(F . ((F . (d3,((D,F) . d2))),((D,F) . d4)))) is Element of D
[d1,(F . ((F . (d3,((D,F) . d2))),((D,F) . d4)))] is set
F . [d1,(F . ((F . (d3,((D,F) . d2))),((D,F) . d4)))] is set
F . (((D,F) . d2),((D,F) . d4)) is Element of D
[((D,F) . d2),((D,F) . d4)] is set
F . [((D,F) . d2),((D,F) . d4)] is set
F . (d3,(F . (((D,F) . d2),((D,F) . d4)))) is Element of D
[d3,(F . (((D,F) . d2),((D,F) . d4)))] is set
F . [d3,(F . (((D,F) . d2),((D,F) . d4)))] is set
F . (d1,(F . (d3,(F . (((D,F) . d2),((D,F) . d4)))))) is Element of D
[d1,(F . (d3,(F . (((D,F) . d2),((D,F) . d4)))))] is set
F . [d1,(F . (d3,(F . (((D,F) . d2),((D,F) . d4)))))] is set
F . ((F . (d1,d3)),(F . (((D,F) . d2),((D,F) . d4)))) is Element of D
[(F . (d1,d3)),(F . (((D,F) . d2),((D,F) . d4)))] is set
F . [(F . (d1,d3)),(F . (((D,F) . d2),((D,F) . d4)))] is set
(D,F) . (F . (d2,d4)) is Element of D
F . ((F . (d1,d3)),((D,F) . (F . (d2,d4)))) is Element of D
[(F . (d1,d3)),((D,F) . (F . (d2,d4)))] is set
F . [(F . (d1,d3)),((D,F) . (F . (d2,d4)))] is set