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