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

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

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()

dom <:{},D:> is set

dom D is set
() /\ (dom D) is Relation-like Element of bool K155()
dom <:D,{}:> is set
(dom D) /\ () is Relation-like Element of bool K155()

dom [:{},D:] is set

dom D is set
[:(),(dom D):] is Relation-like set
dom [:D,{}:] is set
[:(dom D),():] is Relation-like set

D is set

{D} is non empty trivial V49(1) set
[:(),{D}:] is Relation-like set
<:{},(() --> D):> is Relation-like Function-like set
<:{},(() --> D):> * F is Relation-like Function-like set

[:(),{D}:] is Relation-like set
bool [:(),{D}:] is non empty set
F .: ({},(() --> D)) is Relation-like Function-like set
<:{},(() --> D):> is Relation-like Function-like set
<:{},(() --> D):> * F is Relation-like Function-like set
D is set

{D} is non empty trivial V49(1) set
[:(),{D}:] is Relation-like set
<:(() --> D),{}:> is Relation-like Function-like set
<:(() --> D),{}:> * F is Relation-like Function-like set

[:(),{D}:] is Relation-like set
bool [:(),{D}:] is non empty set
F .: ((() --> D),{}) is Relation-like Function-like set
<:(() --> D),{}:> is Relation-like Function-like set
<:(() --> 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

bool [:D,{F}:] is non empty 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

dom D is set
F is set
G is set
u is set
[G,u] is set

{G} is non empty trivial V49(1) set

bool [:F,{G}:] is non empty set

{u} is non empty trivial V49(1) 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]}:]

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

u .: (d1,d2) is Relation-like 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:]

d2 is Element of F
u [:] (d1,d2) is Relation-like Function-like set
dom d1 is 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

u [;] (d1,d2) is Relation-like Function-like set
dom d2 is 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

u is Relation-like D -defined F -valued Function-like V18(D,F) Element of bool [:D,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

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

(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

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) ^ (D,F,u,d1) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of F

(D,F,(G ^ 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

(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

(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

(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

[:K155(),D:] is Relation-like non empty V42() set

(D,F,(G ^ (<*> D)),d1) is Relation-like K155() -defined F -valued Function-like V42() FinSequence-like FinSubsequence-like 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

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

(F,D,G,d1,d3,d2) is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of G

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

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

(D,F,G,d1,u,d2) is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of G

{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

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

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

(F,D,G,d1,d2,u) is Relation-like K155() -defined G -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of G

{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

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

d1 is Element 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

d2 + 1 is non empty V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()

(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

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

(F,G,D,d2,d3,d4) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D

(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,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()

{ } is set

d is Element of F

u + (H + 1) is non empty V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()

{ } is set

d9 is Element of G

u + H is V31() V32() V33() V37() V38() V41() V42() V47() set

(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

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

(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()

u + (H + 1) is non empty V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()

(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

(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

(F,G,D,d2,H,i) is Relation-like K155() -defined D -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of D

[:K155(),D:] is Relation-like non empty V42() set

u + 0 is V31() V32() V33() V37() V38() V41() V42() V47() Element of K155()

(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

(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

(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

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

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

(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

{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

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

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

(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

(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

(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

[:K155(),G:] is Relation-like non empty V42() set

(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

[: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)),{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

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

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