:: PNPROC_1 semantic presentation

REAL is V69() V70() V71() V75() set
NAT is V6() V7() V8() non empty V17() non finite cardinal limit_cardinal V69() V70() V71() V72() V73() V74() V75() Element of K48(REAL)
K48(REAL) is set
NAT is V6() V7() V8() non empty V17() non finite cardinal limit_cardinal V69() V70() V71() V72() V73() V74() V75() set
K48(NAT) is V17() non finite set
K48(NAT) is V17() non finite set
INT is V69() V70() V71() V72() V73() V75() set
COMPLEX is V69() V75() set
RAT is V69() V70() V71() V72() V75() set
{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued V6() V7() V8() V10() V11() V12() empty Function-like one-to-one constant functional V24() V25() Function-yielding finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FuncSeq-like integer ext-real V59() V60() V61() V62() V69() V70() V71() V72() V73() V74() V75() set
the Relation-like non-empty empty-yielding NAT -defined RAT -valued V6() V7() V8() V10() V11() V12() empty Function-like one-to-one constant functional V24() V25() Function-yielding finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FuncSeq-like integer ext-real V59() V60() V61() V62() V69() V70() V71() V72() V73() V74() V75() set is Relation-like non-empty empty-yielding NAT -defined RAT -valued V6() V7() V8() V10() V11() V12() empty Function-like one-to-one constant functional V24() V25() Function-yielding finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FuncSeq-like integer ext-real V59() V60() V61() V62() V69() V70() V71() V72() V73() V74() V75() set
2 is V6() V7() V8() V12() non empty V24() V25() finite cardinal integer ext-real positive V58() V69() V70() V71() V72() V73() V74() Element of NAT
1 is V6() V7() V8() V12() non empty V24() V25() finite cardinal integer ext-real positive V58() V69() V70() V71() V72() V73() V74() Element of NAT
3 is V6() V7() V8() V12() non empty V24() V25() finite cardinal integer ext-real positive V58() V69() V70() V71() V72() V73() V74() Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued V6() V7() V8() V10() V11() V12() empty Function-like one-to-one constant functional V24() V25() Function-yielding finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FuncSeq-like integer ext-real V58() V59() V60() V61() V62() V69() V70() V71() V72() V73() V74() V75() Element of NAT
Seg 1 is non empty V17() finite 1 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
{1} is non empty V17() finite V36() 1 -element V69() V70() V71() V72() V73() V74() set
Seg 2 is non empty finite 2 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
{1,2} is non empty finite V36() V69() V70() V71() V72() V73() V74() set
P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N is set
[P,N] is V13() set
{P,N} is non empty finite set
{P} is non empty V17() finite V36() 1 -element V69() V70() V71() V72() V73() V74() set
{{P,N},{P}} is non empty finite V36() set
{[P,N]} is Relation-like non empty V17() Function-like constant finite 1 -element set
proj1 {[P,N]} is non empty V17() finite 1 -element set
{P} is non empty V17() finite V36() 1 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
Seg P is finite P -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
R is set
P is Relation-like NAT -defined Function-like FinSubsequence-like set
Seq P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
proj1 P is V69() V70() V71() V72() V73() V74() set
Sgm (proj1 P) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm (proj1 P)) (#) P is Relation-like NAT -defined Function-like finite set
proj2 (Sgm (proj1 P)) is finite V69() V70() V71() V72() V73() V74() set
dom {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued V6() V7() V8() V10() V11() V12() empty Function-like one-to-one constant functional V24() V25() Function-yielding finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FuncSeq-like integer ext-real V59() V60() V61() V62() V69() V70() V71() V72() V73() V74() V75() Element of K48(NAT)
dom (Sgm (proj1 P)) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
proj2 {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued V6() V7() V8() V10() V11() V12() empty V17() Function-like one-to-one constant functional V24() V25() Function-yielding finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FuncSeq-like integer ext-real V59() V60() V61() V62() V63() V64() V65() V66() V69() V70() V71() V72() V73() V74() V75() set
P is Relation-like NAT -defined Function-like FinSubsequence-like set
Seq P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
proj1 P is V69() V70() V71() V72() V73() V74() set
Sgm (proj1 P) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm (proj1 P)) (#) P is Relation-like NAT -defined Function-like finite set
{} (#) P is Relation-like non-empty empty-yielding NAT -defined RAT -valued V6() V7() V8() V10() V11() V12() empty Function-like one-to-one constant functional V24() V25() Function-yielding finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FuncSeq-like integer ext-real V59() V60() V61() V62() V69() V70() V71() V72() V73() V74() V75() set
P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N is set
[P,N] is V13() set
{P,N} is non empty finite set
{P} is non empty V17() finite V36() 1 -element V69() V70() V71() V72() V73() V74() set
{{P,N},{P}} is non empty finite V36() set
{[P,N]} is Relation-like non empty V17() Function-like constant finite 1 -element set
<*N*> is Relation-like NAT -defined non empty V17() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
R is Relation-like NAT -defined Function-like FinSubsequence-like set
Seq R is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
proj1 R is V69() V70() V71() V72() V73() V74() set
0 + 1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
Seg x is finite x -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
Sgm (proj1 R) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm (proj1 R)) (#) R is Relation-like NAT -defined Function-like finite set
x is Relation-like NAT -defined Function-like FinSubsequence-like set
proj1 x is V69() V70() V71() V72() V73() V74() set
{P} is non empty V17() finite V36() 1 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
Seq x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*P*> is Relation-like NAT -defined NAT -valued non empty V17() Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like V59() V60() V61() V62() V63() V64() V65() V66() Element of NAT *
NAT * is non empty functional FinSequence-membered M12( NAT )
<*P*> (#) {[P,N]} is Relation-like NAT -defined Function-like finite set
{[P,N]} . P is set
<*({[P,N]} . P)*> is Relation-like NAT -defined non empty V17() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
P is Relation-like NAT -defined Function-like FinSubsequence-like set
proj1 P is V69() V70() V71() V72() V73() V74() set
N is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
Seg N is finite N -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
P is set
<*P*> is Relation-like NAT -defined non empty V17() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
N is Relation-like NAT -defined Function-like finite FinSubsequence-like set
Seq N is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
[1,P] is V13() set
{1,P} is non empty finite set
{{1,P},{1}} is non empty finite V36() set
{[1,P]} is Relation-like non empty V17() Function-like constant finite 1 -element set
dom (Seq N) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
{1} is non empty V17() finite V36() 1 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
proj2 (Seq N) is finite set
{P} is non empty V17() finite 1 -element set
proj1 N is finite V69() V70() V71() V72() V73() V74() set
Sgm (proj1 N) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm (proj1 N)) (#) N is Relation-like NAT -defined Function-like finite set
proj2 (Sgm (proj1 N)) is finite V69() V70() V71() V72() V73() V74() set
dom (Sgm (proj1 N)) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
proj2 N is finite set
R is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
Seg R is finite R -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
card (proj1 N) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
Seg (card (proj1 N)) is finite card (proj1 N) -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
card {1} is V6() V7() V8() V12() non empty V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
x is set
{x} is non empty V17() finite 1 -element set
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
[C,P] is V13() set
{C,P} is non empty finite set
{C} is non empty V17() finite V36() 1 -element V69() V70() V71() V72() V73() V74() set
{{C,P},{C}} is non empty finite V36() set
{[C,P]} is Relation-like non empty V17() Function-like constant finite 1 -element set
P is set
N is set
[P,N] is V13() set
{P,N} is non empty finite set
{P} is non empty V17() finite 1 -element set
{{P,N},{P}} is non empty finite V36() set
R is set
x is set
[R,x] is V13() set
{R,x} is non empty finite set
{R} is non empty V17() finite 1 -element set
{{R,x},{R}} is non empty finite V36() set
{[P,N],[R,x]} is Relation-like non empty finite set
C is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom C is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
{P,R} is non empty finite set
C . P is set
C . R is set
len C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
Seg (len C) is finite len C -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
1 + 1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
0 + 1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
{[P,N]} is Relation-like non empty V17() Function-like constant finite 1 -element set
P is set
[1,P] is V13() set
{1,P} is non empty finite set
{{1,P},{1}} is non empty finite V36() set
N is set
<*P,N*> is Relation-like NAT -defined non empty Function-like finite 2 -element FinSequence-like FinSubsequence-like set
[2,N] is V13() set
{2,N} is non empty finite set
{2} is non empty V17() finite V36() 1 -element V69() V70() V71() V72() V73() V74() set
{{2,N},{2}} is non empty finite V36() set
{[1,P],[2,N]} is Relation-like non empty finite set
R is Relation-like Function-like set
proj1 R is set
{1,2} is non empty finite V36() V69() V70() V71() V72() V73() V74() Element of K48(NAT)
dom <*P,N*> is non empty finite 2 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
x is set
<*P,N*> . x is set
[x,P] is V13() set
{x,P} is non empty finite set
{x} is non empty V17() finite 1 -element set
{{x,P},{x}} is non empty finite V36() set
R . x is set
<*P,N*> . x is set
[x,N] is V13() set
{x,N} is non empty finite set
{x} is non empty V17() finite 1 -element set
{{x,N},{x}} is non empty finite V36() set
R . x is set
P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
R is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
R + 1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
R + N is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
R + 0 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
0 + 1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P is Relation-like NAT -defined Function-like finite FinSubsequence-like set
card P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
Seq P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (Seq P) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
proj1 P is finite V69() V70() V71() V72() V73() V74() set
Sgm (proj1 P) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm (proj1 P)) (#) P is Relation-like NAT -defined Function-like finite set
proj2 (Sgm (proj1 P)) is finite V69() V70() V71() V72() V73() V74() set
dom (Seq P) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
dom (Sgm (proj1 P)) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
N is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
Seg N is finite N -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
card (proj1 P) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
card (dom (Sgm (proj1 P))) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P is set
N is set
P /\ N is set
R is set
R is set
P /\ N is set
R is set
P is Relation-like set
proj1 P is set
N is Relation-like set
proj1 N is set
P is set
N is set
R is Relation-like set
R | P is Relation-like set
x is Relation-like set
x | N is Relation-like set
P /\ N is set
proj1 (R | P) is set
proj1 R is set
(proj1 R) /\ P is set
proj1 (x | N) is set
proj1 x is set
(proj1 x) /\ N is set
(proj1 (R | P)) /\ (proj1 (x | N)) is set
P /\ ((proj1 x) /\ N) is set
(proj1 R) /\ (P /\ ((proj1 x) /\ N)) is set
(P /\ N) /\ (proj1 x) is set
(proj1 R) /\ ((P /\ N) /\ (proj1 x)) is set
P is Relation-like NAT -defined Function-like finite FinSubsequence-like set
Seq P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (Seq P) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
proj1 P is finite V69() V70() V71() V72() V73() V74() set
Sgm (proj1 P) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
dom (Sgm (proj1 P)) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
(Sgm (proj1 P)) (#) P is Relation-like NAT -defined Function-like finite set
proj2 (Sgm (proj1 P)) is finite V69() V70() V71() V72() V73() V74() set
P is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj2 P is finite set
Seq P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
proj2 (Seq P) is finite set
proj1 P is finite V69() V70() V71() V72() V73() V74() set
Sgm (proj1 P) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm (proj1 P)) (#) P is Relation-like NAT -defined Function-like finite set
proj2 ((Sgm (proj1 P)) (#) P) is finite set
proj2 (Sgm (proj1 P)) is finite V69() V70() V71() V72() V73() V74() set
P is Relation-like Function-like set
R is Relation-like Function-like set
N is Relation-like Function-like set
proj1 P is set
proj1 N is set
x is set
P . x is set
[x,(P . x)] is V13() set
{x,(P . x)} is non empty finite set
{x} is non empty V17() finite 1 -element set
{{x,(P . x)},{x}} is non empty finite V36() set
N . x is set
[x,(N . x)] is V13() set
{x,(N . x)} is non empty finite set
{{x,(N . x)},{x}} is non empty finite V36() set
P is set
N is Relation-like set
P |` N is Relation-like set
N " P is set
N | (N " P) is Relation-like set
R is set
x is set
[R,x] is V13() set
{R,x} is non empty finite set
{R} is non empty V17() finite 1 -element set
{{R,x},{R}} is non empty finite V36() set
P is set
N is Relation-like Function-like set
P |` N is Relation-like Function-like set
N " P is set
N | (N " P) is Relation-like Function-like set
R is set
x is set
[R,x] is V13() set
{R,x} is non empty finite set
{R} is non empty V17() finite 1 -element set
{{R,x},{R}} is non empty finite V36() set
proj1 N is set
N . R is set
N . R is set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
F₁() is set
K49(F₁(),NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(F₁(),NAT)) is set
P is Relation-like Function-like set
proj1 P is set
proj2 P is set
N is set
R is set
P . R is set
F₂(R) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(F₁(),NAT))
R is set
N . R is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
F₂(R) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is set
N . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
R . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
proj1 N is set
proj1 R is set
P is set
P --> 0 is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
{0} is non empty V17() functional finite V36() 1 -element V69() V70() V71() V72() V73() V74() set
K49(P,{0}) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
C is set
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
P is set
N is set
(N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(N,NAT))
K49(N,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(N,NAT)) is set
N --> 0 is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(N,NAT))
K49(N,{0}) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
(N) . P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
(P) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
P --> 0 is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
K49(P,{0}) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is set
(P) . R is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
N . R is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
C is set
N . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
x . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
R . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
N + R is Relation-like INT -valued RAT -valued Function-like V59() V60() V61() V62() set
N + R is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
proj1 (N + R) is set
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
N + R is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
C is set
x . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
N . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
R . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(N . C) + (R . C) is V24() V25() integer ext-real set
proj1 x is set
proj1 (N + R) is set
proj1 N is set
proj1 R is set
(proj1 N) /\ (proj1 R) is set
P /\ (proj1 R) is set
P /\ P is set
C is set
x . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
N . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
R . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(N . C) + (R . C) is V24() V25() integer ext-real set
(N + R) . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
(P) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
P --> 0 is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
K49(P,{0}) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,N,(P)) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is set
(P) . R is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
N . R is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(N . R) + ((P) . R) is V24() V25() integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
C is set
x . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
N . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
R . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(N . C) - (R . C) is V24() V25() integer ext-real set
(N . C) -' (R . C) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real non negative V58() V69() V70() V71() V72() V73() V74() Element of NAT
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
C is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
q1 is set
x . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
C . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
N . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
R . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(N . q1) - (R . q1) is V24() V25() integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,N,R) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is set
N . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(P,N,R) . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() set
R . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(N . x) + (R . x) is V24() V25() integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
(P) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
P --> 0 is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
K49(P,{0}) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,N,(P)) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is set
(P) . R is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
N . R is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(N . R) - ((P) . R) is V24() V25() integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,x,R) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,x,N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
C is set
(P,x,R) . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(P,x,N) . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
N . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
R . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
x . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(x . C) - (N . C) is V24() V25() integer ext-real set
(x . C) - (R . C) is V24() V25() integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,N,R) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,N,R),R) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is set
(P,(P,N,R),R) . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
N . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(P,N,R) . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() set
R . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
((P,N,R) . x) - (R . x) is V24() V25() integer ext-real set
(N . x) + (R . x) is V24() V25() integer ext-real set
((N . x) + (R . x)) - (R . x) is V24() V25() integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,R,N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,x,N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
C is set
(P,R,N) . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(P,x,N) . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
R . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
x . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
N . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(R . C) - (N . C) is V24() V25() integer ext-real set
(x . C) - (N . C) is V24() V25() integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,R,N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,R,x) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,R,x),N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,R,N),x) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
C is set
(P,(P,R,x),N) . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(P,(P,R,N),x) . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() set
(P,R,N) . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
x . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
((P,R,N) . C) + (x . C) is V24() V25() integer ext-real set
R . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
N . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(R . C) - (N . C) is V24() V25() integer ext-real set
(x . C) + ((R . C) - (N . C)) is V24() V25() integer ext-real set
(x . C) + (R . C) is V24() V25() integer ext-real set
((x . C) + (R . C)) - (N . C) is V24() V25() integer ext-real set
(P,x,R) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,x,R) . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() set
((P,x,R) . C) - (N . C) is V24() V25() integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is set
N . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
R . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,N,R) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,N,R),x) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,R,x) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,N,(P,R,x)) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
C is set
(P,(P,N,R),x) . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() set
(P,N,(P,R,x)) . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() set
(P,N,R) . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() set
x . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
((P,N,R) . C) + (x . C) is V24() V25() integer ext-real set
N . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
R . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(N . C) + (R . C) is V24() V25() integer ext-real set
((N . C) + (R . C)) + (x . C) is V24() V25() integer ext-real set
(P,R,x) . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() set
(N . C) + ((P,R,x) . C) is V24() V25() integer ext-real set
(R . C) + (x . C) is V24() V25() integer ext-real set
(N . C) + ((R . C) + (x . C)) is V24() V25() integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,N,x) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
C is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,R,C) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
q1 is set
(P,N,x) . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() set
(P,R,C) . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() set
N . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
R . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
x . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
C . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(N . q1) + (x . q1) is V24() V25() integer ext-real set
(R . q1) + (C . q1) is V24() V25() integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,R,N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is set
(P,R,N) . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
R . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
N . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(R . x) - (N . x) is V24() V25() integer ext-real set
(R . x) - 0 is V24() V25() integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,R,x) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
C is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,N,C) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
q1 is set
(P,N,C) . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(P,R,x) . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
N . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
R . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
x . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
C . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(R . q1) - (x . q1) is V24() V25() integer ext-real set
(N . q1) - (C . q1) is V24() V25() integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,R,N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,R,N),N) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is set
R . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(P,(P,R,N),N) . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() set
(P,R,N) . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
N . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
((P,R,N) . x) + (N . x) is V24() V25() integer ext-real set
(R . x) - (N . x) is V24() V25() integer ext-real set
((R . x) - (N . x)) + (N . x) is V24() V25() integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,N,R) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,N,R),N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is set
(P,(P,N,R),N) . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
R . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(P,N,R) . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() set
N . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
((P,N,R) . x) - (N . x) is V24() V25() integer ext-real set
(N . x) + (R . x) is V24() V25() integer ext-real set
((N . x) + (R . x)) - (N . x) is V24() V25() integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,N,R) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,x,N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,x,N),R) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,x,(P,N,R)) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,x,(P,N,R)),(P,N,R)) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,(P,x,(P,N,R)),(P,N,R)),N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,(P,(P,x,(P,N,R)),(P,N,R)),N),R) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,x,(P,N,R)),R) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,(P,x,(P,N,R)),R),N) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,(P,(P,x,(P,N,R)),R),N),N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,(P,(P,(P,x,(P,N,R)),R),N),N),R) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,(P,x,(P,N,R)),R),R) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,R,N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,x,(P,R,N)) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,x,R) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,x,R),N) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,N,(P,R,N)) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,N,(P,R,N)),(P,R,N)) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,x,(P,R,N)),N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,(P,x,(P,R,N)),N),N) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
the Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT)) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
[ the Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT)), the Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))] is V13() set
{ the Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT)), the Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))} is non empty functional finite set
{ the Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))} is non empty V17() functional finite 1 -element set
{{ the Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT)), the Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))},{ the Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))}} is non empty finite V36() set
P is set
P is set
N is (P)
N `1 is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
[R,x] is V13() set
{R,x} is non empty functional finite set
{R} is non empty V17() functional finite 1 -element set
{{R,x},{R}} is non empty finite V36() set
N `2 is set
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
[R,x] is V13() set
{R,x} is non empty functional finite set
{R} is non empty V17() functional finite 1 -element set
{{R,x},{R}} is non empty finite V36() set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
R is (P)
(P,R) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,N,(P,R)) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,R) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,N,(P,R)),(P,R)) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is (P)
(P,R) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,N,R) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,N,(P,R)) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,R) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is (P)
(P,x) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,R),(P,x)) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,N,R),x) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,N,(P,R)),(P,x)) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,(P,N,(P,R)),(P,x)),(P,R)) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,x) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,(P,(P,N,(P,R)),(P,x)),(P,R)),(P,x)) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,N,(P,R)),(P,R)) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,x),(P,R)) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,(P,x),(P,R)),(P,R)) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,(P,R),(P,x)),(P,R)) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,N,R),(P,x)) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,(P,N,R),(P,x)),(P,x)) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,(P,N,(P,R)),(P,R)),(P,x)) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,(P,(P,N,(P,R)),(P,R)),(P,x)),(P,x)) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
P is set
Funcs (P,NAT) is non empty functional FUNCTION_DOMAIN of P, NAT
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is (P)
R is set
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,x,N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like Function-like set
proj1 R is set
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R . x is set
(P,x,N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
C is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,C,N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like Function-like set
proj1 R is set
x is Relation-like Function-like set
proj1 x is set
C is set
R . C is set
q1 is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,q1,N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x . C is set
P is set
Funcs (P,NAT) is non empty functional FUNCTION_DOMAIN of P, NAT
N is (P)
(P,N) is Relation-like Function-like set
proj2 (P,N) is set
R is set
proj1 (P,N) is set
x is set
(P,N) . x is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
C is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,C,N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is (P)
(P,R) is Relation-like Function-like set
x is (P)
(P,N,x) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,N,x),R) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,x) is Relation-like Function-like set
(P,x) (#) (P,R) is Relation-like Function-like set
((P,x) (#) (P,R)) . N is set
proj1 (P,x) is set
Funcs (P,NAT) is non empty functional FUNCTION_DOMAIN of P, NAT
(P,R) . (P,N,x) is set
(P,x) . N is set
(P,R) . ((P,x) . N) is set
P is set
the (P) is (P)
{ the (P)} is non empty V17() finite 1 -element set
R is set
P is set
N is non empty (P)
R is Element of N
P is set
P is set
N is non empty (P)
N * is non empty functional FinSequence-membered M12(N)
Funcs (P,NAT) is non empty functional FUNCTION_DOMAIN of P, NAT
R is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
len R is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
dom R is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
dom x is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
Seg (len x) is finite len x -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
Seg (len R) is finite len R -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
C is set
proj1 x is finite V69() V70() V71() V72() V73() V74() set
x . C is set
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
R /. q1 is Element of N
(P,(R /. q1)) is Relation-like Function-like set
C is Relation-like NAT -defined Function-like Function-yielding finite FinSequence-like FinSubsequence-like set
compose (C,(Funcs (P,NAT))) is Relation-like Function-like set
q1 is Relation-like Function-like set
len C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
C . q2 is set
R /. q2 is Element of N
(P,(R /. q2)) is Relation-like Function-like set
x is Relation-like Function-like set
C is Relation-like Function-like set
q1 is Relation-like NAT -defined Function-like Function-yielding finite FinSequence-like FinSubsequence-like set
compose (q1,(Funcs (P,NAT))) is Relation-like Function-like set
len q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q2 is Relation-like NAT -defined Function-like Function-yielding finite FinSequence-like FinSubsequence-like set
compose (q2,(Funcs (P,NAT))) is Relation-like Function-like set
len q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
dom q1 is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
Seg (len q1) is finite len q1 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
dom q2 is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
Seg (len q2) is finite len q2 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
Seg (len R) is finite len R -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
fs2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
q1 . fs2 is set
R /. fs2 is Element of N
(P,(R /. fs2)) is Relation-like Function-like set
q2 . fs2 is set
P is set
Funcs (P,NAT) is non empty functional FUNCTION_DOMAIN of P, NAT
id (Funcs (P,NAT)) is Relation-like Funcs (P,NAT) -defined Funcs (P,NAT) -valued non empty Function-like one-to-one total quasi_total Element of K48(K49((Funcs (P,NAT)),(Funcs (P,NAT))))
K49((Funcs (P,NAT)),(Funcs (P,NAT))) is Relation-like set
K48(K49((Funcs (P,NAT)),(Funcs (P,NAT)))) is set
N is non empty (P)
<*> N is Relation-like non-empty empty-yielding NAT -defined N -valued V6() V7() V8() V10() V11() V12() empty Function-like one-to-one constant functional V24() V25() Function-yielding finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FuncSeq-like integer ext-real V59() V60() V61() V62() V69() V70() V71() V72() V73() V74() V75() Element of N *
N * is non empty functional FinSequence-membered M12(N)
(P,N,(<*> N)) is Relation-like Function-like set
len (<*> N) is Relation-like non-empty empty-yielding NAT -defined RAT -valued V6() V7() V8() V10() V11() V12() empty Function-like one-to-one constant functional V24() V25() Function-yielding finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FuncSeq-like integer ext-real V58() V59() V60() V61() V62() V69() V70() V71() V72() V73() V74() V75() Element of NAT
dom (<*> N) is Relation-like non-empty empty-yielding NAT -defined RAT -valued V6() V7() V8() V10() V11() V12() empty Function-like one-to-one constant functional V24() V25() Function-yielding finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FuncSeq-like integer ext-real V59() V60() V61() V62() V69() V70() V71() V72() V73() V74() V75() Element of K48(NAT)
R is Relation-like NAT -defined Function-like Function-yielding finite FinSequence-like FinSubsequence-like set
compose (R,(Funcs (P,NAT))) is Relation-like Function-like set
len R is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P is set
N is non empty (P)
R is (P,N)
<*R*> is Relation-like NAT -defined N -valued non empty V17() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like Element of N *
N * is non empty functional FinSequence-membered M12(N)
(P,N,<*R*>) is Relation-like Function-like set
(P,R) is Relation-like Function-like set
Funcs (P,NAT) is non empty functional FUNCTION_DOMAIN of P, NAT
len <*R*> is V6() V7() V8() V12() non empty V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
dom <*R*> is non empty V17() finite 1 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
x is Relation-like NAT -defined Function-like Function-yielding finite FinSequence-like FinSubsequence-like set
compose (x,(Funcs (P,NAT))) is Relation-like Function-like set
len x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
<*R*> . 1 is set
{1} is non empty V17() finite V36() 1 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
<*R*> /. 1 is Element of N
x . 1 is set
(P,(<*R*> /. 1)) is Relation-like Function-like set
<*(P,R)*> is Relation-like NAT -defined non empty V17() Function-like constant Function-yielding finite 1 -element FinSequence-like FinSubsequence-like FuncSeq-like set
proj1 (P,R) is set
P is set
Funcs (P,NAT) is non empty functional FUNCTION_DOMAIN of P, NAT
id (Funcs (P,NAT)) is Relation-like Funcs (P,NAT) -defined Funcs (P,NAT) -valued non empty Function-like one-to-one total quasi_total Element of K48(K49((Funcs (P,NAT)),(Funcs (P,NAT))))
K49((Funcs (P,NAT)),(Funcs (P,NAT))) is Relation-like set
K48(K49((Funcs (P,NAT)),(Funcs (P,NAT)))) is set
N is non empty (P)
R is (P,N)
(P,R) is Relation-like Function-like set
(id (Funcs (P,NAT))) (#) (P,R) is Relation-like Funcs (P,NAT) -defined Function-like set
<*(P,R)*> is Relation-like NAT -defined non empty V17() Function-like constant Function-yielding finite 1 -element FinSequence-like FinSubsequence-like FuncSeq-like set
compose (<*(P,R)*>,(Funcs (P,NAT))) is Relation-like Function-like set
proj1 (P,R) is set
P is set
N is non empty (P)
R is (P,N)
(P,R) is Relation-like Function-like set
x is (P,N)
<*R,x*> is Relation-like NAT -defined N -valued non empty Function-like finite 2 -element FinSequence-like FinSubsequence-like Element of N *
N * is non empty functional FinSequence-membered M12(N)
(P,N,<*R,x*>) is Relation-like Function-like set
(P,x) is Relation-like Function-like set
(P,R) (#) (P,x) is Relation-like Function-like set
Funcs (P,NAT) is non empty functional FUNCTION_DOMAIN of P, NAT
len <*R,x*> is V6() V7() V8() V12() non empty V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
dom <*R,x*> is non empty finite 2 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
C is Relation-like NAT -defined Function-like Function-yielding finite FinSequence-like FinSubsequence-like set
compose (C,(Funcs (P,NAT))) is Relation-like Function-like set
len C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
<*R,x*> . 1 is set
<*R,x*> . 2 is set
{1,2} is non empty finite V36() V69() V70() V71() V72() V73() V74() Element of K48(NAT)
<*R,x*> /. 1 is Element of N
<*R,x*> /. 2 is Element of N
C . 1 is set
C . 2 is set
<*(P,R),(P,x)*> is Relation-like NAT -defined non empty Function-like Function-yielding finite 2 -element FinSequence-like FinSubsequence-like set
id (Funcs (P,NAT)) is Relation-like Funcs (P,NAT) -defined Funcs (P,NAT) -valued non empty Function-like one-to-one total quasi_total Element of K48(K49((Funcs (P,NAT)),(Funcs (P,NAT))))
K49((Funcs (P,NAT)),(Funcs (P,NAT))) is Relation-like set
K48(K49((Funcs (P,NAT)),(Funcs (P,NAT)))) is set
(id (Funcs (P,NAT))) (#) (P,R) is Relation-like Funcs (P,NAT) -defined Function-like set
(id (Funcs (P,NAT))) (#) ((P,R) (#) (P,x)) is Relation-like Funcs (P,NAT) -defined Function-like set
P is set
Funcs (P,NAT) is non empty functional FUNCTION_DOMAIN of P, NAT
N is non empty (P)
N * is non empty functional FinSequence-membered M12(N)
R is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
(P,N,R) is Relation-like Function-like set
proj1 (P,N,R) is set
proj2 (P,N,R) is set
x is Relation-like NAT -defined Function-like Function-yielding finite FinSequence-like FinSubsequence-like set
len x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
dom x is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
compose (x,(Funcs (P,NAT))) is Relation-like Function-like set
proj1 (compose (x,(Funcs (P,NAT)))) is set
proj2 (compose (x,(Funcs (P,NAT)))) is set
id (Funcs (P,NAT)) is Relation-like Funcs (P,NAT) -defined Funcs (P,NAT) -valued non empty Function-like one-to-one total quasi_total Element of K48(K49((Funcs (P,NAT)),(Funcs (P,NAT))))
K49((Funcs (P,NAT)),(Funcs (P,NAT))) is Relation-like set
K48(K49((Funcs (P,NAT)),(Funcs (P,NAT)))) is set
x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
x + 1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
C is Relation-like NAT -defined Function-like Function-yielding finite FinSequence-like FinSubsequence-like set
len C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
dom C is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
compose (C,(Funcs (P,NAT))) is Relation-like Function-like set
proj1 (compose (C,(Funcs (P,NAT)))) is set
proj2 (compose (C,(Funcs (P,NAT)))) is set
q1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
q2 is set
<*q2*> is Relation-like NAT -defined non empty V17() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
q1 ^ <*q2*> is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set
len q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
0 + 1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
C . (x + 1) is set
C is (P)
(P,C) is Relation-like Function-like set
fs2 is Relation-like NAT -defined Function-like Function-yielding finite FinSequence-like FinSubsequence-like set
compose (fs2,(Funcs (P,NAT))) is Relation-like Function-like set
(compose (fs2,(Funcs (P,NAT)))) (#) (P,C) is Relation-like Function-like set
proj1 (P,C) is set
proj2 (P,C) is set
dom fs2 is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
C3 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
fs2 . C3 is set
C . C3 is set
proj1 (compose (fs2,(Funcs (P,NAT)))) is set
proj2 (compose (fs2,(Funcs (P,NAT)))) is set
len R is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
dom R is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
x is Relation-like NAT -defined Function-like Function-yielding finite FinSequence-like FinSubsequence-like set
compose (x,(Funcs (P,NAT))) is Relation-like Function-like set
len x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
dom x is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
x . C is set
Seg (len x) is finite len x -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
Seg (len R) is finite len R -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
R /. C is Element of N
q1 is (P,N)
(P,q1) is Relation-like Function-like set
P is set
N is non empty (P)
N * is non empty functional FinSequence-membered M12(N)
R is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
(P,N,R) is Relation-like Function-like set
x is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
R ^ x is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
(P,N,(R ^ x)) is Relation-like Function-like set
(P,N,x) is Relation-like Function-like set
(P,N,R) (#) (P,N,x) is Relation-like Function-like set
Funcs (P,NAT) is non empty functional FUNCTION_DOMAIN of P, NAT
len (R ^ x) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
dom (R ^ x) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
C is Relation-like NAT -defined Function-like Function-yielding finite FinSequence-like FinSubsequence-like set
compose (C,(Funcs (P,NAT))) is Relation-like Function-like set
len C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
len R is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
dom R is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
q1 is Relation-like NAT -defined Function-like Function-yielding finite FinSequence-like FinSubsequence-like set
compose (q1,(Funcs (P,NAT))) is Relation-like Function-like set
len q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
len x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
dom x is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
q2 is Relation-like NAT -defined Function-like Function-yielding finite FinSequence-like FinSubsequence-like set
compose (q2,(Funcs (P,NAT))) is Relation-like Function-like set
len q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
proj2 (P,N,R) is set
(len R) + (len x) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
dom C is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
(len q1) + (len q2) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
Seg ((len q1) + (len q2)) is finite (len q1) + (len q2) -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
dom q1 is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
fs2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
C . fs2 is set
q1 . fs2 is set
Seg (len q1) is finite len q1 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
Seg (len R) is finite len R -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
(R ^ x) /. fs2 is Element of N
(P,((R ^ x) /. fs2)) is Relation-like Function-like set
(R ^ x) . fs2 is set
R . fs2 is set
R /. fs2 is Element of N
dom q2 is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
fs2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(len q1) + fs2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
C . ((len q1) + fs2) is set
q2 . fs2 is set
Seg (len q2) is finite len q2 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
(R ^ x) /. ((len q1) + fs2) is Element of N
(P,((R ^ x) /. ((len q1) + fs2))) is Relation-like Function-like set
(R ^ x) . ((len q1) + fs2) is set
x . fs2 is set
x /. fs2 is Element of N
q1 ^ q2 is Relation-like NAT -defined Function-like Function-yielding finite FinSequence-like FinSubsequence-like set
P is set
N is non empty (P)
N * is non empty functional FinSequence-membered M12(N)
R is (P,N)
<*R*> is Relation-like NAT -defined N -valued non empty V17() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like Element of N *
(P,R) is Relation-like Function-like set
x is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
x ^ <*R*> is Relation-like NAT -defined N -valued non empty Function-like finite FinSequence-like FinSubsequence-like Element of N *
(P,N,(x ^ <*R*>)) is Relation-like Function-like set
(P,N,x) is Relation-like Function-like set
(P,N,x) (#) (P,R) is Relation-like Function-like set
(P,N,<*R*>) is Relation-like Function-like set
(P,N,x) (#) (P,N,<*R*>) is Relation-like Function-like set
P is set
N is non empty (P)
N * is non empty functional FinSequence-membered M12(N)
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
R is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
(P,N,R) is Relation-like Function-like set
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,N,R) . x is set
proj1 (P,N,R) is set
Funcs (P,NAT) is non empty functional FUNCTION_DOMAIN of P, NAT
proj2 (P,N,R) is set
[x,((P,N,R) . x)] is V13() set
{x,((P,N,R) . x)} is non empty finite set
{x} is non empty V17() functional finite 1 -element set
{{x,((P,N,R) . x)},{x}} is non empty finite V36() set
P is set
P is set
N is non empty (P)
N * is non empty functional FinSequence-membered M12(N)
K48((N *)) is set
R is functional FinSequence-membered Element of K48((N *))
x is functional FinSequence-membered Element of K48((N *))
{ (b₁ ^ b₂) where b₁, b₂ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ( b₁ in R & b₂ in x ) } is set
q1 is set
q2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
fs2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q2 ^ fs2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
P is set
N is non empty (P)
N * is non empty functional FinSequence-membered M12(N)
K48((N *)) is set
R is non empty functional FinSequence-membered Element of K48((N *))
x is non empty functional FinSequence-membered Element of K48((N *))
(P,N,R,x) is functional FinSequence-membered Element of K48((N *))
{ (b₁ ^ b₂) where b₁, b₂ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ( b₁ in R & b₂ in x ) } is set
C is set
q1 is set
q2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
fs2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q2 ^ fs2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
P is set
N is non empty (P)
N * is non empty functional FinSequence-membered M12(N)
K48((N *)) is set
R is functional FinSequence-membered Element of K48((N *))
x is functional FinSequence-membered Element of K48((N *))
R \/ x is functional FinSequence-membered Element of K48((N *))
C is functional FinSequence-membered Element of K48((N *))
(P,N,(R \/ x),C) is functional FinSequence-membered Element of K48((N *))
{ (b₁ ^ b₂) where b₁, b₂ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ( b₁ in R \/ x & b₂ in C ) } is set
(P,N,R,C) is functional FinSequence-membered Element of K48((N *))
{ (b₁ ^ b₂) where b₁, b₂ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ( b₁ in R & b₂ in C ) } is set
(P,N,x,C) is functional FinSequence-membered Element of K48((N *))
{ (b₁ ^ b₂) where b₁, b₂ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ( b₁ in x & b₂ in C ) } is set
(P,N,R,C) \/ (P,N,x,C) is functional FinSequence-membered Element of K48((N *))
q1 is set
q2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
fs2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q2 ^ fs2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q1 is set
q2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
fs2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q2 ^ fs2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
fs2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q2 ^ fs2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
P is set
N is non empty (P)
N * is non empty functional FinSequence-membered M12(N)
K48((N *)) is set
R is functional FinSequence-membered Element of K48((N *))
x is functional FinSequence-membered Element of K48((N *))
(P,N,R,x) is functional FinSequence-membered Element of K48((N *))
{ (b₁ ^ b₂) where b₁, b₂ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ( b₁ in R & b₂ in x ) } is set
C is functional FinSequence-membered Element of K48((N *))
x \/ C is functional FinSequence-membered Element of K48((N *))
(P,N,R,(x \/ C)) is functional FinSequence-membered Element of K48((N *))
{ (b₁ ^ b₂) where b₁, b₂ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ( b₁ in R & b₂ in x \/ C ) } is set
(P,N,R,C) is functional FinSequence-membered Element of K48((N *))
{ (b₁ ^ b₂) where b₁, b₂ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ( b₁ in R & b₂ in C ) } is set
(P,N,R,x) \/ (P,N,R,C) is functional FinSequence-membered Element of K48((N *))
q1 is set
q2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
fs2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q2 ^ fs2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q1 is set
q2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
fs2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q2 ^ fs2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
fs2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q2 ^ fs2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
P is set
N is non empty (P)
N * is non empty functional FinSequence-membered M12(N)
R is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
{R} is non empty V17() functional finite V36() 1 -element FinSequence-membered Element of K48((N *))
K48((N *)) is set
x is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
{x} is non empty V17() functional finite V36() 1 -element FinSequence-membered Element of K48((N *))
(P,N,{R},{x}) is non empty functional FinSequence-membered Element of K48((N *))
{ (b₁ ^ b₂) where b₁, b₂ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ( b₁ in {R} & b₂ in {x} ) } is set
R ^ x is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
{(R ^ x)} is non empty V17() functional finite V36() 1 -element FinSequence-membered Element of K48((N *))
C is set
q1 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q1 ^ q2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
C is set
P is set
N is non empty (P)
N * is non empty functional FinSequence-membered M12(N)
R is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
x is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
{R,x} is non empty functional finite V36() FinSequence-membered Element of K48((N *))
K48((N *)) is set
C is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
{C} is non empty V17() functional finite V36() 1 -element FinSequence-membered Element of K48((N *))
(P,N,{R,x},{C}) is non empty functional FinSequence-membered Element of K48((N *))
{ (b₁ ^ b₂) where b₁, b₂ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ( b₁ in {R,x} & b₂ in {C} ) } is set
R ^ C is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
x ^ C is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
{(R ^ C),(x ^ C)} is non empty functional finite V36() FinSequence-membered Element of K48((N *))
{R} is non empty V17() functional finite V36() 1 -element FinSequence-membered Element of K48((N *))
{x} is non empty V17() functional finite V36() 1 -element FinSequence-membered Element of K48((N *))
{R} \/ {x} is non empty functional finite V36() FinSequence-membered Element of K48((N *))
(P,N,({R} \/ {x}),{C}) is non empty functional FinSequence-membered Element of K48((N *))
{ (b₁ ^ b₂) where b₁, b₂ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ( b₁ in {R} \/ {x} & b₂ in {C} ) } is set
(P,N,{R},{C}) is non empty functional FinSequence-membered Element of K48((N *))
{ (b₁ ^ b₂) where b₁, b₂ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ( b₁ in {R} & b₂ in {C} ) } is set
(P,N,{x},{C}) is non empty functional FinSequence-membered Element of K48((N *))
{ (b₁ ^ b₂) where b₁, b₂ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ( b₁ in {x} & b₂ in {C} ) } is set
(P,N,{R},{C}) \/ (P,N,{x},{C}) is non empty functional FinSequence-membered Element of K48((N *))
{(R ^ C)} is non empty V17() functional finite V36() 1 -element FinSequence-membered Element of K48((N *))
{(R ^ C)} \/ (P,N,{x},{C}) is non empty functional FinSequence-membered Element of K48((N *))
{(x ^ C)} is non empty V17() functional finite V36() 1 -element FinSequence-membered Element of K48((N *))
{(R ^ C)} \/ {(x ^ C)} is non empty functional finite V36() FinSequence-membered Element of K48((N *))
P is set
N is non empty (P)
N * is non empty functional FinSequence-membered M12(N)
R is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
{R} is non empty V17() functional finite V36() 1 -element FinSequence-membered Element of K48((N *))
K48((N *)) is set
x is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
R ^ x is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
C is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
{x,C} is non empty functional finite V36() FinSequence-membered Element of K48((N *))
(P,N,{R},{x,C}) is non empty functional FinSequence-membered Element of K48((N *))
{ (b₁ ^ b₂) where b₁, b₂ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ( b₁ in {R} & b₂ in {x,C} ) } is set
R ^ C is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
{(R ^ x),(R ^ C)} is non empty functional finite V36() FinSequence-membered Element of K48((N *))
{x} is non empty V17() functional finite V36() 1 -element FinSequence-membered Element of K48((N *))
{C} is non empty V17() functional finite V36() 1 -element FinSequence-membered Element of K48((N *))
{x} \/ {C} is non empty functional finite V36() FinSequence-membered Element of K48((N *))
(P,N,{R},({x} \/ {C})) is non empty functional FinSequence-membered Element of K48((N *))
{ (b₁ ^ b₂) where b₁, b₂ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ( b₁ in {R} & b₂ in {x} \/ {C} ) } is set
(P,N,{R},{x}) is non empty functional FinSequence-membered Element of K48((N *))
{ (b₁ ^ b₂) where b₁, b₂ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ( b₁ in {R} & b₂ in {x} ) } is set
(P,N,{R},{C}) is non empty functional FinSequence-membered Element of K48((N *))
{ (b₁ ^ b₂) where b₁, b₂ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ( b₁ in {R} & b₂ in {C} ) } is set
(P,N,{R},{x}) \/ (P,N,{R},{C}) is non empty functional FinSequence-membered Element of K48((N *))
{(R ^ x)} is non empty V17() functional finite V36() 1 -element FinSequence-membered Element of K48((N *))
{(R ^ x)} \/ (P,N,{R},{C}) is non empty functional FinSequence-membered Element of K48((N *))
{(R ^ C)} is non empty V17() functional finite V36() 1 -element FinSequence-membered Element of K48((N *))
{(R ^ x)} \/ {(R ^ C)} is non empty functional finite V36() FinSequence-membered Element of K48((N *))
P is set
N is non empty (P)
N * is non empty functional FinSequence-membered M12(N)
K48((N *)) is set
R is functional FinSequence-membered Element of K48((N *))
x is functional FinSequence-membered Element of K48((N *))
{ b₁ where b₁ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ex b₂, b₃ being Relation-like NAT -defined Function-like finite FinSubsequence-like set st
( b₁ = b₂ \/ b₃ & b₂ misses b₃ & Seq b₂ in R & Seq b₃ in x ) } is set
q1 is set
q2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
fs2 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
C is Relation-like NAT -defined Function-like finite FinSubsequence-like set
fs2 \/ C is Relation-like finite set
Seq fs2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq C is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
C is functional FinSequence-membered Element of K48((N *))
q1 is functional FinSequence-membered Element of K48((N *))
q2 is functional FinSequence-membered Element of K48((N *))
{ b₁ where b₁ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ex b₂, b₃ being Relation-like NAT -defined Function-like finite FinSubsequence-like set st
( b₁ = b₂ \/ b₃ & b₂ misses b₃ & Seq b₂ in q1 & Seq b₃ in q2 ) } is set
{ b₁ where b₁ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ex b₂, b₃ being Relation-like NAT -defined Function-like finite FinSubsequence-like set st
( b₁ = b₂ \/ b₃ & b₂ misses b₃ & Seq b₂ in q2 & Seq b₃ in q1 ) } is set
fs2 is set
C is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
C3 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q1 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
C3 \/ q1 is Relation-like finite set
Seq C3 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq q1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
fs2 is set
C is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
C3 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q1 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
C3 \/ q1 is Relation-like finite set
Seq C3 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq q1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
P is set
N is non empty (P)
N * is non empty functional FinSequence-membered M12(N)
K48((N *)) is set
R is functional FinSequence-membered Element of K48((N *))
x is functional FinSequence-membered Element of K48((N *))
R \/ x is functional FinSequence-membered Element of K48((N *))
C is functional FinSequence-membered Element of K48((N *))
(P,N,(R \/ x),C) is functional FinSequence-membered Element of K48((N *))
{ b₁ where b₁ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ex b₂, b₃ being Relation-like NAT -defined Function-like finite FinSubsequence-like set st
( b₁ = b₂ \/ b₃ & b₂ misses b₃ & Seq b₂ in R \/ x & Seq b₃ in C ) } is set
(P,N,R,C) is functional FinSequence-membered Element of K48((N *))
{ b₁ where b₁ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ex b₂, b₃ being Relation-like NAT -defined Function-like finite FinSubsequence-like set st
( b₁ = b₂ \/ b₃ & b₂ misses b₃ & Seq b₂ in R & Seq b₃ in C ) } is set
(P,N,x,C) is functional FinSequence-membered Element of K48((N *))
{ b₁ where b₁ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ex b₂, b₃ being Relation-like NAT -defined Function-like finite FinSubsequence-like set st
( b₁ = b₂ \/ b₃ & b₂ misses b₃ & Seq b₂ in x & Seq b₃ in C ) } is set
(P,N,R,C) \/ (P,N,x,C) is functional FinSequence-membered Element of K48((N *))
q1 is set
q2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
fs2 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
C is Relation-like NAT -defined Function-like finite FinSubsequence-like set
fs2 \/ C is Relation-like finite set
Seq fs2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq C is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
fs2 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
C is Relation-like NAT -defined Function-like finite FinSubsequence-like set
fs2 \/ C is Relation-like finite set
Seq fs2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq C is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
q1 is set
q2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
fs2 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
C is Relation-like NAT -defined Function-like finite FinSubsequence-like set
fs2 \/ C is Relation-like finite set
Seq fs2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq C is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
fs2 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
C is Relation-like NAT -defined Function-like finite FinSubsequence-like set
fs2 \/ C is Relation-like finite set
Seq fs2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq C is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
q2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
fs2 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
C is Relation-like NAT -defined Function-like finite FinSubsequence-like set
fs2 \/ C is Relation-like finite set
Seq fs2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq C is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
fs2 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
C is Relation-like NAT -defined Function-like finite FinSubsequence-like set
fs2 \/ C is Relation-like finite set
Seq fs2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq C is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
P is set
N is non empty (P)
N * is non empty functional FinSequence-membered M12(N)
R is (P,N)
<*R*> is Relation-like NAT -defined N -valued non empty V17() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like Element of N *
{<*R*>} is non empty V17() functional finite V36() 1 -element FinSequence-membered Element of K48((N *))
K48((N *)) is set
x is (P,N)
<*x*> is Relation-like NAT -defined N -valued non empty V17() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like Element of N *
{<*x*>} is non empty V17() functional finite V36() 1 -element FinSequence-membered Element of K48((N *))
(P,N,{<*R*>},{<*x*>}) is functional FinSequence-membered Element of K48((N *))
{ b₁ where b₁ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ex b₂, b₃ being Relation-like NAT -defined Function-like finite FinSubsequence-like set st
( b₁ = b₂ \/ b₃ & b₂ misses b₃ & Seq b₂ in {<*R*>} & Seq b₃ in {<*x*>} ) } is set
<*R,x*> is Relation-like NAT -defined N -valued non empty Function-like finite 2 -element FinSequence-like FinSubsequence-like Element of N *
<*x,R*> is Relation-like NAT -defined N -valued non empty Function-like finite 2 -element FinSequence-like FinSubsequence-like Element of N *
{<*R,x*>,<*x,R*>} is non empty functional finite V36() FinSequence-membered Element of K48((N *))
C is set
C3 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q1 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q2 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q1 \/ q2 is Relation-like finite set
Seq q1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq q2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
q1 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q2 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q1 \/ q2 is Relation-like finite set
Seq q1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq q2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
C4 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
[C4,R] is V13() Element of K49(NAT,N)
K49(NAT,N) is Relation-like V17() non finite set
{C4,R} is non empty finite set
{C4} is non empty V17() finite V36() 1 -element V69() V70() V71() V72() V73() V74() set
{{C4,R},{C4}} is non empty finite V36() set
{[C4,R]} is Relation-like non empty V17() Function-like constant finite 1 -element set
q3 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
[q3,x] is V13() Element of K49(NAT,N)
{q3,x} is non empty finite set
{q3} is non empty V17() finite V36() 1 -element V69() V70() V71() V72() V73() V74() set
{{q3,x},{q3}} is non empty finite V36() set
{[q3,x]} is Relation-like non empty V17() Function-like constant finite 1 -element set
{[C4,R],[q3,x]} is Relation-like non empty finite set
C is set
[1,R] is V13() Element of K49(NAT,N)
K49(NAT,N) is Relation-like V17() non finite set
{1,R} is non empty finite set
{{1,R},{1}} is non empty finite V36() set
[2,x] is V13() Element of K49(NAT,N)
{2,x} is non empty finite set
{2} is non empty V17() finite V36() 1 -element V69() V70() V71() V72() V73() V74() set
{{2,x},{2}} is non empty finite V36() set
{[1,R],[2,x]} is Relation-like non empty finite set
{[1,R]} is Relation-like non empty V17() Function-like constant finite 1 -element set
{[2,x]} is Relation-like non empty V17() Function-like constant finite 1 -element set
{[1,R]} \/ {[2,x]} is Relation-like non empty finite set
q1 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
C3 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
Seq C3 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq q1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
[1,x] is V13() Element of K49(NAT,N)
K49(NAT,N) is Relation-like V17() non finite set
{1,x} is non empty finite set
{{1,x},{1}} is non empty finite V36() set
[2,R] is V13() Element of K49(NAT,N)
{2,R} is non empty finite set
{2} is non empty V17() finite V36() 1 -element V69() V70() V71() V72() V73() V74() set
{{2,R},{2}} is non empty finite V36() set
{[1,x],[2,R]} is Relation-like non empty finite set
{[1,x]} is Relation-like non empty V17() Function-like constant finite 1 -element set
{[2,R]} is Relation-like non empty V17() Function-like constant finite 1 -element set
{[1,x]} \/ {[2,R]} is Relation-like non empty finite set
q1 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
C3 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
Seq C3 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq q1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
P is set
N is non empty (P)
N * is non empty functional FinSequence-membered M12(N)
R is (P,N)
<*R*> is Relation-like NAT -defined N -valued non empty V17() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like Element of N *
x is (P,N)
<*x*> is Relation-like NAT -defined N -valued non empty V17() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like Element of N *
{<*R*>,<*x*>} is non empty functional finite V36() FinSequence-membered Element of K48((N *))
K48((N *)) is set
C is (P,N)
<*C*> is Relation-like NAT -defined N -valued non empty V17() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like Element of N *
{<*C*>} is non empty V17() functional finite V36() 1 -element FinSequence-membered Element of K48((N *))
(P,N,{<*R*>,<*x*>},{<*C*>}) is functional FinSequence-membered Element of K48((N *))
{ b₁ where b₁ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ex b₂, b₃ being Relation-like NAT -defined Function-like finite FinSubsequence-like set st
( b₁ = b₂ \/ b₃ & b₂ misses b₃ & Seq b₂ in {<*R*>,<*x*>} & Seq b₃ in {<*C*>} ) } is set
<*R,C*> is Relation-like NAT -defined N -valued non empty Function-like finite 2 -element FinSequence-like FinSubsequence-like Element of N *
<*x,C*> is Relation-like NAT -defined N -valued non empty Function-like finite 2 -element FinSequence-like FinSubsequence-like Element of N *
<*C,R*> is Relation-like NAT -defined N -valued non empty Function-like finite 2 -element FinSequence-like FinSubsequence-like Element of N *
<*C,x*> is Relation-like NAT -defined N -valued non empty Function-like finite 2 -element FinSequence-like FinSubsequence-like Element of N *
{<*R,C*>,<*x,C*>,<*C,R*>,<*C,x*>} is functional finite FinSequence-membered Element of K48((N *))
{<*R*>} is non empty V17() functional finite V36() 1 -element FinSequence-membered Element of K48((N *))
{<*x*>} is non empty V17() functional finite V36() 1 -element FinSequence-membered Element of K48((N *))
{<*R*>} \/ {<*x*>} is non empty functional finite V36() FinSequence-membered Element of K48((N *))
(P,N,{<*R*>},{<*C*>}) is functional FinSequence-membered Element of K48((N *))
{ b₁ where b₁ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ex b₂, b₃ being Relation-like NAT -defined Function-like finite FinSubsequence-like set st
( b₁ = b₂ \/ b₃ & b₂ misses b₃ & Seq b₂ in {<*R*>} & Seq b₃ in {<*C*>} ) } is set
(P,N,{<*x*>},{<*C*>}) is functional FinSequence-membered Element of K48((N *))
{ b₁ where b₁ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ex b₂, b₃ being Relation-like NAT -defined Function-like finite FinSubsequence-like set st
( b₁ = b₂ \/ b₃ & b₂ misses b₃ & Seq b₂ in {<*x*>} & Seq b₃ in {<*C*>} ) } is set
(P,N,{<*R*>},{<*C*>}) \/ (P,N,{<*x*>},{<*C*>}) is functional FinSequence-membered Element of K48((N *))
{<*R,C*>,<*C,R*>} is non empty functional finite V36() FinSequence-membered Element of K48((N *))
{<*x,C*>,<*C,x*>} is non empty functional finite V36() FinSequence-membered Element of K48((N *))
{<*R,C*>,<*C,R*>,<*x,C*>,<*C,x*>} is functional finite FinSequence-membered Element of K48((N *))
P is set
N is non empty (P)
N * is non empty functional FinSequence-membered M12(N)
K48((N *)) is set
R is functional FinSequence-membered Element of K48((N *))
x is functional FinSequence-membered Element of K48((N *))
(P,N,R,x) is functional FinSequence-membered Element of K48((N *))
{ (b₁ ^ b₂) where b₁, b₂ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ( b₁ in R & b₂ in x ) } is set
C is functional FinSequence-membered Element of K48((N *))
(P,N,(P,N,R,x),C) is functional FinSequence-membered Element of K48((N *))
{ (b₁ ^ b₂) where b₁, b₂ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ( b₁ in (P,N,R,x) & b₂ in C ) } is set
(P,N,x,C) is functional FinSequence-membered Element of K48((N *))
{ (b₁ ^ b₂) where b₁, b₂ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ( b₁ in x & b₂ in C ) } is set
(P,N,R,(P,N,x,C)) is functional FinSequence-membered Element of K48((N *))
{ (b₁ ^ b₂) where b₁, b₂ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ( b₁ in R & b₂ in (P,N,x,C) ) } is set
q1 is set
q2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
fs2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q2 ^ fs2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
C is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
C3 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
C ^ C3 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
C3 ^ fs2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
C ^ (C3 ^ fs2) is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q1 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q1 is set
q2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
fs2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q2 ^ fs2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
C is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
C3 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
C ^ C3 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q2 ^ C is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
(q2 ^ C) ^ C3 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q1 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
N is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 P is finite V69() V70() V71() V72() V73() V74() set
{ (N + b₁) where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : b₁ in proj1 P } is set
x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
Seg x is finite x -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
C is set
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N + q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P . q1 is set
[q1,(P . q1)] is V13() set
{q1,(P . q1)} is non empty finite set
{q1} is non empty V17() finite V36() 1 -element V69() V70() V71() V72() V73() V74() set
{{q1,(P . q1)},{q1}} is non empty finite V36() set
C is Relation-like Function-like set
proj1 C is set
N + x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
Seg (N + x) is finite N + x -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
q1 is set
q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N + q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q1 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 q1 is finite V69() V70() V71() V72() V73() V74() set
q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
N + q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q1 . (N + q2) is set
P . q2 is set
fs2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N + fs2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P . fs2 is set
x is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 x is finite V69() V70() V71() V72() V73() V74() set
C is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 C is finite V69() V70() V71() V72() V73() V74() set
q1 is set
q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N + q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
x . q1 is set
P . q2 is set
C . q1 is set
P is Relation-like NAT -defined Function-like finite FinSubsequence-like set
(P,0) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 P is finite V69() V70() V71() V72() V73() V74() set
{ (0 + b₁) where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : b₁ in proj1 P } is set
proj1 (P,0) is finite V69() V70() V71() V72() V73() V74() set
R is set
x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
0 + x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
R is set
x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
Seg x is finite x -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
0 + C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
R is set
(P,0) . R is set
P . R is set
x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
0 + x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P + N is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
R is Relation-like NAT -defined Function-like finite FinSubsequence-like set
(R,(P + N)) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
(R,N) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
((R,N),P) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 R is finite V69() V70() V71() V72() V73() V74() set
{ (N + b₁) where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : b₁ in proj1 R } is set
proj1 (R,N) is finite V69() V70() V71() V72() V73() V74() set
{ (P + b₁) where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : b₁ in proj1 (R,N) } is set
{ ((P + N) + b₁) where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : b₁ in proj1 R } is set
proj1 ((R,N),P) is finite V69() V70() V71() V72() V73() V74() set
proj1 (R,(P + N)) is finite V69() V70() V71() V72() V73() V74() set
C3 is set
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P + q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N + q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(P + N) + q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
C3 is set
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(P + N) + q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N + q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P + q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
C3 is set
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(P + N) + q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N + q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P + (N + q1) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(R,(P + N)) . C3 is set
R . q1 is set
(R,N) . (N + q1) is set
((R,N),P) . C3 is set
P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P + 1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(N,P) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 (N,P) is finite V69() V70() V71() V72() V73() V74() set
len N is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P + (len N) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
{ b₁ where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : ( P + 1 <= b₁ & b₁ <= P + (len N) ) } is set
dom N is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
Seg (len N) is finite len N -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
{ b₁ where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : ( 1 <= b₁ & b₁ <= len N ) } is set
{ (P + b₁) where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : b₁ in dom N } is set
x is set
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P + C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P + q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
x is set
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P + 0 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
P + q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N is Relation-like NAT -defined Function-like finite FinSubsequence-like set
(N,P) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 (N,P) is finite V69() V70() V71() V72() V73() V74() set
proj1 N is finite V69() V70() V71() V72() V73() V74() set
{ (P + b₁) where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : b₁ in proj1 N } is set
R is set
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P + C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
x is set
[R,x] is V13() set
{R,x} is non empty finite set
{R} is non empty V17() finite 1 -element set
{{R,x},{R}} is non empty finite V36() set
R is set
Sgm (proj1 N) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
proj2 (Sgm (proj1 N)) is finite V69() V70() V71() V72() V73() V74() set
x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P + x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 N is finite V69() V70() V71() V72() V73() V74() set
(N,P) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 (N,P) is finite V69() V70() V71() V72() V73() V74() set
R is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
Seg R is finite R -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
x is set
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P + C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
x is Relation-like Function-like set
proj1 x is set
{ (P + b₁) where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : b₁ in proj1 N } is set
C is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj2 C is finite set
q1 is set
proj1 C is finite V69() V70() V71() V72() V73() V74() set
q2 is set
C . q2 is set
fs2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P + fs2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q1 is set
q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P + q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
C . q2 is set
fs2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P + fs2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
C . q1 is set
P + q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P + q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
proj1 C is finite V69() V70() V71() V72() V73() V74() set
q1 is set
C . q1 is set
q2 is set
C . q2 is set
fs2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P + fs2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P + C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom N is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
(N,P) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 (N,P) is finite V69() V70() V71() V72() V73() V74() set
R is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 R is finite V69() V70() V71() V72() V73() V74() set
proj2 R is finite set
len N is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
Seg (len N) is finite len N -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom x is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N is Relation-like NAT -defined Function-like finite FinSubsequence-like set
card N is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(N,P) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
card (N,P) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
proj1 N is finite V69() V70() V71() V72() V73() V74() set
proj1 (N,P) is finite V69() V70() V71() V72() V73() V74() set
R is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 R is finite V69() V70() V71() V72() V73() V74() set
proj2 R is finite set
card (proj1 N) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
card (proj1 (N,P)) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom N is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
(N,P) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
Seq (N,P) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (Seq (N,P)) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
proj1 (N,P) is finite V69() V70() V71() V72() V73() V74() set
Sgm (proj1 (N,P)) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
proj2 (Sgm (proj1 (N,P))) is finite V69() V70() V71() V72() V73() V74() set
(Sgm (proj1 (N,P))) (#) (N,P) is Relation-like NAT -defined Function-like finite set
len N is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
Seg (len N) is finite len N -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
dom (Sgm (proj1 (N,P))) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
len (Sgm (proj1 (N,P))) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
Seg (len (Sgm (proj1 (N,P)))) is finite len (Sgm (proj1 (N,P))) -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
card (proj1 (N,P)) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
R is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
Seg R is finite R -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
card (N,P) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N + P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
R is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom R is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
(R,N) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 (R,N) is finite V69() V70() V71() V72() V73() V74() set
Sgm (proj1 (R,N)) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm (proj1 (R,N))) . P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom x is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
proj2 x is finite set
proj2 (Sgm (proj1 (R,N))) is finite V69() V70() V71() V72() V73() V74() set
C is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
len C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
fs2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
C . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
C . q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
dom C is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
Seg (len C) is finite len C -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
{ b₁ where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : ( 1 <= b₁ & b₁ <= len C ) } is set
C3 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
C3 + 1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(len C) - 1 is V24() V25() integer ext-real set
(len C) + 0 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(len C) + 1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N + C3 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N + q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
Seg q1 is finite q1 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
R is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom R is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
(R,N) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
Seq (R,N) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(Seq (R,N)) . P is set
R . P is set
dom (Seq (R,N)) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
proj1 (R,N) is finite V69() V70() V71() V72() V73() V74() set
Sgm (proj1 (R,N)) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm (proj1 (R,N))) (#) (R,N) is Relation-like NAT -defined Function-like finite set
((Sgm (proj1 (R,N))) (#) (R,N)) . P is set
(Sgm (proj1 (R,N))) . P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(R,N) . ((Sgm (proj1 (R,N))) . P) is set
N + P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(R,N) . (N + P) is set
P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(N,P) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
Seq (N,P) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (Seq (N,P)) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
dom N is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
R is set
(Seq (N,P)) . R is set
N . R is set
P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(N,(len P)) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
P \/ (N,(len P)) is Relation-like finite set
proj1 (P \/ (N,(len P))) is finite set
len N is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(len P) + (len N) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
Seg ((len P) + (len N)) is finite (len P) + (len N) -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
{ b₁ where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : ( 1 <= b₁ & b₁ <= (len P) + (len N) ) } is set
dom P is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
proj1 (N,(len P)) is finite V69() V70() V71() V72() V73() V74() set
(dom P) \/ (proj1 (N,(len P))) is finite V69() V70() V71() V72() V73() V74() set
Seg (len P) is finite len P -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
{ b₁ where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : ( 1 <= b₁ & b₁ <= len P ) } is set
(len P) + 1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
{ b₁ where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : ( (len P) + 1 <= b₁ & b₁ <= (len P) + (len N) ) } is set
R is set
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
R is set
x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
C is V24() V25() integer ext-real set
C + 1 is V24() V25() integer ext-real set
C + (len N) is V24() V25() integer ext-real set
P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len N is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
dom N is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
R is Relation-like NAT -defined Function-like finite FinSubsequence-like set
(R,P) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 (R,P) is finite V69() V70() V71() V72() V73() V74() set
Seg (len N) is finite len N -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
{ b₁ where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : ( 1 <= b₁ & b₁ <= len N ) } is set
proj1 R is finite V69() V70() V71() V72() V73() V74() set
{ (P + b₁) where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : b₁ in proj1 R } is set
(dom N) /\ (proj1 (R,P)) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
x is set
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P + C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
Seg q1 is finite q1 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
{ b₁ where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : ( 1 <= b₁ & b₁ <= q1 ) } is set
C - 0 is V24() V25() integer ext-real set
1 - 1 is V24() V25() integer ext-real set
q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(len N) + C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q2 - 0 is V24() V25() integer ext-real set
((len N) + C) - C is V24() V25() integer ext-real set
fs2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
P ^ N is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(N,(len P)) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
P \/ (N,(len P)) is Relation-like finite set
proj1 (P \/ (N,(len P))) is finite set
len N is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(len P) + (len N) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
Seg ((len P) + (len N)) is finite (len P) + (len N) -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
dom P is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
proj1 (N,(len P)) is finite V69() V70() V71() V72() V73() V74() set
R is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom R is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
R . x is set
P . x is set
[x,(P . x)] is V13() set
{x,(P . x)} is non empty finite set
{x} is non empty V17() finite V36() 1 -element V69() V70() V71() V72() V73() V74() set
{{x,(P . x)},{x}} is non empty finite V36() set
dom N is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(len P) + x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
R . ((len P) + x) is set
N . x is set
{ ((len P) + b₁) where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : b₁ in dom N } is set
(N,(len P)) . ((len P) + x) is set
[((len P) + x),((N,(len P)) . ((len P) + x))] is V13() set
{((len P) + x),((N,(len P)) . ((len P) + x))} is non empty finite set
{((len P) + x)} is non empty V17() finite V36() 1 -element V69() V70() V71() V72() V73() V74() set
{{((len P) + x),((N,(len P)) . ((len P) + x))},{((len P) + x)}} is non empty finite V36() set
P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len N is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
R is Relation-like NAT -defined Function-like finite FinSubsequence-like set
(R,P) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
dom N is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
proj1 (R,P) is finite V69() V70() V71() V72() V73() V74() set
P is set
N is non empty (P)
N * is non empty functional FinSequence-membered M12(N)
K48((N *)) is set
R is functional FinSequence-membered Element of K48((N *))
x is functional FinSequence-membered Element of K48((N *))
(P,N,R,x) is functional FinSequence-membered Element of K48((N *))
{ b₁ where b₁ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ex b₂, b₃ being Relation-like NAT -defined Function-like finite FinSubsequence-like set st
( b₁ = b₂ \/ b₃ & b₂ misses b₃ & Seq b₂ in R & Seq b₃ in x ) } is set
C is functional FinSequence-membered Element of K48((N *))
(P,N,(P,N,R,x),C) is functional FinSequence-membered Element of K48((N *))
{ b₁ where b₁ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ex b₂, b₃ being Relation-like NAT -defined Function-like finite FinSubsequence-like set st
( b₁ = b₂ \/ b₃ & b₂ misses b₃ & Seq b₂ in (P,N,R,x) & Seq b₃ in C ) } is set
(P,N,x,C) is functional FinSequence-membered Element of K48((N *))
{ b₁ where b₁ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ex b₂, b₃ being Relation-like NAT -defined Function-like finite FinSubsequence-like set st
( b₁ = b₂ \/ b₃ & b₂ misses b₃ & Seq b₂ in x & Seq b₃ in C ) } is set
(P,N,R,(P,N,x,C)) is functional FinSequence-membered Element of K48((N *))
{ b₁ where b₁ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ex b₂, b₃ being Relation-like NAT -defined Function-like finite FinSubsequence-like set st
( b₁ = b₂ \/ b₃ & b₂ misses b₃ & Seq b₂ in R & Seq b₃ in (P,N,x,C) ) } is set
q1 is set
q2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
fs2 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
C is Relation-like NAT -defined Function-like finite FinSubsequence-like set
fs2 \/ C is Relation-like finite set
Seq fs2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq C is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
fs2 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
C is Relation-like NAT -defined Function-like finite FinSubsequence-like set
fs2 \/ C is Relation-like finite set
Seq fs2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq C is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
C3 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q1 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q2 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q1 \/ q2 is Relation-like finite set
Seq q1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq q2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
q1 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q2 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q1 \/ q2 is Relation-like finite set
Seq q1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq q2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
proj1 fs2 is finite V69() V70() V71() V72() V73() V74() set
C4 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
Seg C4 is finite C4 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
Sgm (proj1 fs2) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
proj1 q1 is finite V69() V70() V71() V72() V73() V74() set
(Sgm (proj1 fs2)) .: (proj1 q1) is finite V69() V70() V71() V72() V73() V74() set
proj1 q2 is finite V69() V70() V71() V72() V73() V74() set
(Sgm (proj1 fs2)) .: (proj1 q2) is finite V69() V70() V71() V72() V73() V74() set
(Sgm (proj1 fs2)) | (proj1 q1) is Relation-like NAT -defined proj1 q1 -defined NAT -defined INT -valued RAT -valued Function-like finite FinSubsequence-like V59() V60() V61() V62() Element of K48(K49(NAT,NAT))
K49(NAT,NAT) is Relation-like INT -valued RAT -valued V17() non finite V59() V60() V61() V62() set
K48(K49(NAT,NAT)) is V17() non finite set
proj2 ((Sgm (proj1 fs2)) | (proj1 q1)) is finite V69() V70() V71() V72() V73() V74() set
(Sgm (proj1 fs2)) | (proj1 q2) is Relation-like NAT -defined proj1 q2 -defined NAT -defined INT -valued RAT -valued Function-like finite FinSubsequence-like V59() V60() V61() V62() Element of K48(K49(NAT,NAT))
proj2 ((Sgm (proj1 fs2)) | (proj1 q2)) is finite V69() V70() V71() V72() V73() V74() set
fs2 | (proj2 ((Sgm (proj1 fs2)) | (proj1 q1))) is Relation-like NAT -defined proj2 ((Sgm (proj1 fs2)) | (proj1 q1)) -defined NAT -defined Function-like finite FinSubsequence-like set
fs2 | (proj2 ((Sgm (proj1 fs2)) | (proj1 q2))) is Relation-like NAT -defined proj2 ((Sgm (proj1 fs2)) | (proj1 q2)) -defined NAT -defined Function-like finite FinSubsequence-like set
dom (Sgm (proj1 fs2)) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
proj1 (q1 \/ q2) is finite set
(proj1 q1) \/ (proj1 q2) is finite V69() V70() V71() V72() V73() V74() set
(fs2 | (proj2 ((Sgm (proj1 fs2)) | (proj1 q1)))) \/ (fs2 | (proj2 ((Sgm (proj1 fs2)) | (proj1 q2)))) is Relation-like finite set
(proj2 ((Sgm (proj1 fs2)) | (proj1 q1))) \/ (proj2 ((Sgm (proj1 fs2)) | (proj1 q2))) is finite V69() V70() V71() V72() V73() V74() set
fs2 | ((proj2 ((Sgm (proj1 fs2)) | (proj1 q1))) \/ (proj2 ((Sgm (proj1 fs2)) | (proj1 q2)))) is Relation-like NAT -defined (proj2 ((Sgm (proj1 fs2)) | (proj1 q1))) \/ (proj2 ((Sgm (proj1 fs2)) | (proj1 q2))) -defined NAT -defined Function-like finite FinSubsequence-like set
(Sgm (proj1 fs2)) .: ((proj1 q1) \/ (proj1 q2)) is finite V69() V70() V71() V72() V73() V74() set
fs2 | ((Sgm (proj1 fs2)) .: ((proj1 q1) \/ (proj1 q2))) is Relation-like NAT -defined (Sgm (proj1 fs2)) .: ((proj1 q1) \/ (proj1 q2)) -defined NAT -defined Function-like finite FinSubsequence-like set
(Sgm (proj1 fs2)) | (dom (Sgm (proj1 fs2))) is Relation-like NAT -defined dom (Sgm (proj1 fs2)) -defined NAT -defined INT -valued RAT -valued Function-like finite FinSubsequence-like V59() V60() V61() V62() Element of K48(K49(NAT,NAT))
proj2 ((Sgm (proj1 fs2)) | (dom (Sgm (proj1 fs2)))) is finite V69() V70() V71() V72() V73() V74() set
fs2 | (proj2 ((Sgm (proj1 fs2)) | (dom (Sgm (proj1 fs2))))) is Relation-like NAT -defined proj2 ((Sgm (proj1 fs2)) | (dom (Sgm (proj1 fs2)))) -defined NAT -defined Function-like finite FinSubsequence-like set
proj2 (Sgm (proj1 fs2)) is finite V69() V70() V71() V72() V73() V74() set
fs2 | (proj2 (Sgm (proj1 fs2))) is Relation-like NAT -defined proj2 (Sgm (proj1 fs2)) -defined NAT -defined Function-like finite FinSubsequence-like set
fs2 | (proj1 fs2) is Relation-like NAT -defined proj1 fs2 -defined NAT -defined Function-like finite FinSubsequence-like set
proj2 q2 is finite set
proj2 fs2 is finite set
proj2 C is finite set
(proj2 fs2) \/ (proj2 C) is finite set
proj2 (Seq fs2) is finite set
proj2 q1 is finite set
proj2 q2 is finite set
(proj2 q1) \/ (proj2 q2) is finite set
proj2 (Seq q1) is finite set
proj2 (Seq q2) is finite set
C is Relation-like NAT -defined proj2 q2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of proj2 q2
K48(C) is finite V36() set
q3 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q4 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q5 is Relation-like NAT -defined proj2 q2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of proj2 q2
K48(q5) is finite V36() set
ss2 is Relation-like NAT -defined proj2 q2 -valued Function-like finite FinSubsequence-like Element of K48(q5)
Seq ss2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
q6 is Relation-like NAT -defined proj2 q2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of proj2 q2
ss2 is Relation-like NAT -defined proj2 q2 -valued Function-like finite FinSubsequence-like Element of K48(C)
ss1 is Relation-like NAT -defined proj2 q2 -valued Function-like finite FinSubsequence-like Element of K48(C)
proj1 ss1 is finite V69() V70() V71() V72() V73() V74() set
Sgm (proj1 ss1) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
proj1 ss2 is finite V69() V70() V71() V72() V73() V74() set
(Sgm (proj1 ss1)) | (proj1 ss2) is Relation-like NAT -defined proj1 ss2 -defined NAT -defined INT -valued RAT -valued Function-like finite FinSubsequence-like V59() V60() V61() V62() Element of K48(K49(NAT,NAT))
proj2 ((Sgm (proj1 ss1)) | (proj1 ss2)) is finite V69() V70() V71() V72() V73() V74() set
ss1 | (proj2 ((Sgm (proj1 ss1)) | (proj1 ss2))) is Relation-like NAT -defined proj2 ((Sgm (proj1 ss1)) | (proj1 ss2)) -defined NAT -defined proj2 q2 -valued Function-like finite FinSubsequence-like set
Seq q3 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
fss4 is Relation-like NAT -defined proj2 q2 -valued Function-like finite FinSubsequence-like Element of K48(q5)
Seq fss4 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
ss is Relation-like NAT -defined proj2 q2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of proj2 q2
ss1 is Relation-like NAT -defined proj2 q2 -valued Function-like finite FinSubsequence-like Element of K48(C)
proj1 fss4 is finite V69() V70() V71() V72() V73() V74() set
(Sgm (proj1 ss1)) | (proj1 fss4) is Relation-like NAT -defined proj1 fss4 -defined NAT -defined INT -valued RAT -valued Function-like finite FinSubsequence-like V59() V60() V61() V62() Element of K48(K49(NAT,NAT))
proj2 ((Sgm (proj1 ss1)) | (proj1 fss4)) is finite V69() V70() V71() V72() V73() V74() set
ss1 | (proj2 ((Sgm (proj1 ss1)) | (proj1 fss4))) is Relation-like NAT -defined proj2 ((Sgm (proj1 ss1)) | (proj1 fss4)) -defined NAT -defined proj2 q2 -valued Function-like finite FinSubsequence-like set
fs2 /\ C is Relation-like finite set
q3 /\ C is Relation-like finite set
q4 /\ C is Relation-like finite set
(q3 /\ C) \/ (q4 /\ C) is Relation-like finite set
proj1 q4 is finite V69() V70() V71() V72() V73() V74() set
proj1 C is finite V69() V70() V71() V72() V73() V74() set
q4 \/ C is Relation-like finite set
dom q2 is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
(proj1 fs2) \/ (proj1 C) is finite V69() V70() V71() V72() V73() V74() set
proj1 q3 is finite V69() V70() V71() V72() V73() V74() set
(proj1 q3) \/ (proj1 q4) is finite V69() V70() V71() V72() V73() V74() set
((proj1 q3) \/ (proj1 q4)) \/ (proj1 C) is finite V69() V70() V71() V72() V73() V74() set
(proj1 q4) \/ (proj1 C) is finite V69() V70() V71() V72() V73() V74() set
(proj1 q3) \/ ((proj1 q4) \/ (proj1 C)) is finite V69() V70() V71() V72() V73() V74() set
q7 is Relation-like Function-like set
proj1 q7 is set
(proj1 q3) \/ (proj1 q7) is set
len q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
Seg (len q2) is finite len q2 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
q7 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q3 \/ q7 is Relation-like finite set
q3 /\ q7 is Relation-like finite set
q3 /\ q4 is Relation-like finite set
(q3 /\ q4) \/ (q3 /\ C) is Relation-like finite set
Seq q7 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
proj2 (Seq q7) is finite set
proj2 q7 is finite set
proj2 q3 is finite set
(proj2 q7) \/ (proj2 q3) is finite set
dom (Seq q7) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
len (Seq q7) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
Seg (len (Seq q7)) is finite len (Seq q7) -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
proj1 q7 is finite V69() V70() V71() V72() V73() V74() set
Sgm (proj1 q7) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm (proj1 q7)) (#) q4 is Relation-like NAT -defined Function-like finite set
proj1 ((Sgm (proj1 q7)) (#) q4) is finite V69() V70() V71() V72() V73() V74() set
dom (Sgm (proj1 q7)) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
(Sgm (proj1 q7)) (#) C is Relation-like NAT -defined Function-like finite set
proj1 ((Sgm (proj1 q7)) (#) C) is finite V69() V70() V71() V72() V73() V74() set
C3 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
(Sgm (proj1 q7)) (#) q7 is Relation-like NAT -defined Function-like finite set
q8 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q9 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q8 \/ q9 is Relation-like finite set
proj1 q8 is finite V69() V70() V71() V72() V73() V74() set
(Sgm (proj1 q7)) " (proj1 q4) is finite set
proj1 q9 is finite V69() V70() V71() V72() V73() V74() set
(Sgm (proj1 q7)) " (proj1 C) is finite set
(proj1 C) /\ (proj1 q4) is finite V69() V70() V71() V72() V73() V74() set
(proj1 q4) /\ (proj1 C) is finite V69() V70() V71() V72() V73() V74() set
(Sgm (proj1 q7)) " ((proj1 q4) /\ (proj1 C)) is finite set
((Sgm (proj1 q7)) " (proj1 q4)) /\ ((Sgm (proj1 q7)) " (proj1 C)) is finite set
proj2 (Sgm (proj1 q7)) is finite V69() V70() V71() V72() V73() V74() set
(Sgm (proj1 q7)) | (proj1 q8) is Relation-like NAT -defined proj1 q8 -defined NAT -defined INT -valued RAT -valued Function-like finite FinSubsequence-like V59() V60() V61() V62() Element of K48(K49(NAT,NAT))
proj2 ((Sgm (proj1 q7)) | (proj1 q8)) is finite V69() V70() V71() V72() V73() V74() set
(proj1 q4) |` (Sgm (proj1 q7)) is Relation-like NAT -defined proj1 q4 -valued INT -valued Function-like finite FinSubsequence-like V59() V60() V61() set
proj2 ((proj1 q4) |` (Sgm (proj1 q7))) is finite V69() V70() V71() V72() V73() set
Sgm (proj1 q8) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm (proj1 q7)) * (Sgm (proj1 q8)) is Relation-like NAT -defined INT -valued RAT -valued Function-like finite V59() V60() V61() V62() Element of K48(K49(NAT,NAT))
Sgm (proj2 ((Sgm (proj1 q7)) | (proj1 q8))) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
Seq q8 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(Sgm (proj1 q8)) (#) ((Sgm (proj1 q7)) (#) q4) is Relation-like NAT -defined Function-like finite set
((Sgm (proj1 q7)) * (Sgm (proj1 q8))) (#) q4 is Relation-like NAT -defined Function-like finite set
Seq q4 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(Sgm (proj1 q7)) | (proj1 q9) is Relation-like NAT -defined proj1 q9 -defined NAT -defined INT -valued RAT -valued Function-like finite FinSubsequence-like V59() V60() V61() V62() Element of K48(K49(NAT,NAT))
proj2 ((Sgm (proj1 q7)) | (proj1 q9)) is finite V69() V70() V71() V72() V73() V74() set
(proj1 C) |` (Sgm (proj1 q7)) is Relation-like NAT -defined proj1 C -valued INT -valued Function-like finite FinSubsequence-like V59() V60() V61() set
proj2 ((proj1 C) |` (Sgm (proj1 q7))) is finite V69() V70() V71() V72() V73() set
Sgm (proj1 q9) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm (proj1 q7)) * (Sgm (proj1 q9)) is Relation-like NAT -defined INT -valued RAT -valued Function-like finite V59() V60() V61() V62() Element of K48(K49(NAT,NAT))
Sgm (proj2 ((Sgm (proj1 q7)) | (proj1 q9))) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
Seq q9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(Sgm (proj1 q9)) (#) ((Sgm (proj1 q7)) (#) C) is Relation-like NAT -defined Function-like finite set
((Sgm (proj1 q7)) * (Sgm (proj1 q9))) (#) C is Relation-like NAT -defined Function-like finite set
c₃₀ is Relation-like NAT -defined Function-like finite FinSubsequence-like set
c₃₁ is Relation-like NAT -defined Function-like finite FinSubsequence-like set
c₃₀ \/ c₃₁ is Relation-like finite set
Seq c₃₀ is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq c₃₁ is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
q1 is set
q2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
fs2 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
C is Relation-like NAT -defined Function-like finite FinSubsequence-like set
fs2 \/ C is Relation-like finite set
Seq fs2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq C is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
fs2 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
C is Relation-like NAT -defined Function-like finite FinSubsequence-like set
fs2 \/ C is Relation-like finite set
Seq fs2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq C is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
C3 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q1 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q2 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q1 \/ q2 is Relation-like finite set
Seq q1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq q2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
q1 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q2 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q1 \/ q2 is Relation-like finite set
Seq q1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq q2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
proj1 C is finite V69() V70() V71() V72() V73() V74() set
C4 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
Seg C4 is finite C4 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
Sgm (proj1 C) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
proj1 q1 is finite V69() V70() V71() V72() V73() V74() set
(Sgm (proj1 C)) .: (proj1 q1) is finite V69() V70() V71() V72() V73() V74() set
proj1 q2 is finite V69() V70() V71() V72() V73() V74() set
(Sgm (proj1 C)) .: (proj1 q2) is finite V69() V70() V71() V72() V73() V74() set
(Sgm (proj1 C)) | (proj1 q1) is Relation-like NAT -defined proj1 q1 -defined NAT -defined INT -valued RAT -valued Function-like finite FinSubsequence-like V59() V60() V61() V62() Element of K48(K49(NAT,NAT))
K49(NAT,NAT) is Relation-like INT -valued RAT -valued V17() non finite V59() V60() V61() V62() set
K48(K49(NAT,NAT)) is V17() non finite set
proj2 ((Sgm (proj1 C)) | (proj1 q1)) is finite V69() V70() V71() V72() V73() V74() set
(Sgm (proj1 C)) | (proj1 q2) is Relation-like NAT -defined proj1 q2 -defined NAT -defined INT -valued RAT -valued Function-like finite FinSubsequence-like V59() V60() V61() V62() Element of K48(K49(NAT,NAT))
proj2 ((Sgm (proj1 C)) | (proj1 q2)) is finite V69() V70() V71() V72() V73() V74() set
C | (proj2 ((Sgm (proj1 C)) | (proj1 q1))) is Relation-like NAT -defined proj2 ((Sgm (proj1 C)) | (proj1 q1)) -defined NAT -defined Function-like finite FinSubsequence-like set
C | (proj2 ((Sgm (proj1 C)) | (proj1 q2))) is Relation-like NAT -defined proj2 ((Sgm (proj1 C)) | (proj1 q2)) -defined NAT -defined Function-like finite FinSubsequence-like set
dom (Sgm (proj1 C)) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
dom (Seq C) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
(proj1 q1) \/ (proj1 q2) is finite V69() V70() V71() V72() V73() V74() set
(C | (proj2 ((Sgm (proj1 C)) | (proj1 q1)))) \/ (C | (proj2 ((Sgm (proj1 C)) | (proj1 q2)))) is Relation-like finite set
(proj2 ((Sgm (proj1 C)) | (proj1 q1))) \/ (proj2 ((Sgm (proj1 C)) | (proj1 q2))) is finite V69() V70() V71() V72() V73() V74() set
C | ((proj2 ((Sgm (proj1 C)) | (proj1 q1))) \/ (proj2 ((Sgm (proj1 C)) | (proj1 q2)))) is Relation-like NAT -defined (proj2 ((Sgm (proj1 C)) | (proj1 q1))) \/ (proj2 ((Sgm (proj1 C)) | (proj1 q2))) -defined NAT -defined Function-like finite FinSubsequence-like set
(Sgm (proj1 C)) .: ((proj1 q1) \/ (proj1 q2)) is finite V69() V70() V71() V72() V73() V74() set
C | ((Sgm (proj1 C)) .: ((proj1 q1) \/ (proj1 q2))) is Relation-like NAT -defined (Sgm (proj1 C)) .: ((proj1 q1) \/ (proj1 q2)) -defined NAT -defined Function-like finite FinSubsequence-like set
(Sgm (proj1 C)) | (dom (Sgm (proj1 C))) is Relation-like NAT -defined dom (Sgm (proj1 C)) -defined NAT -defined INT -valued RAT -valued Function-like finite FinSubsequence-like V59() V60() V61() V62() Element of K48(K49(NAT,NAT))
proj2 ((Sgm (proj1 C)) | (dom (Sgm (proj1 C)))) is finite V69() V70() V71() V72() V73() V74() set
C | (proj2 ((Sgm (proj1 C)) | (dom (Sgm (proj1 C))))) is Relation-like NAT -defined proj2 ((Sgm (proj1 C)) | (dom (Sgm (proj1 C)))) -defined NAT -defined Function-like finite FinSubsequence-like set
proj2 (Sgm (proj1 C)) is finite V69() V70() V71() V72() V73() V74() set
C | (proj2 (Sgm (proj1 C))) is Relation-like NAT -defined proj2 (Sgm (proj1 C)) -defined NAT -defined Function-like finite FinSubsequence-like set
C | (proj1 C) is Relation-like NAT -defined proj1 C -defined NAT -defined Function-like finite FinSubsequence-like set
proj2 q2 is finite set
proj2 fs2 is finite set
proj2 C is finite set
(proj2 fs2) \/ (proj2 C) is finite set
proj2 (Seq C) is finite set
proj2 q1 is finite set
proj2 q2 is finite set
(proj2 q1) \/ (proj2 q2) is finite set
proj2 (Seq q1) is finite set
proj2 (Seq q2) is finite set
C is Relation-like NAT -defined proj2 q2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of proj2 q2
K48(C) is finite V36() set
q3 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q4 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q5 is Relation-like NAT -defined proj2 q2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of proj2 q2
K48(q5) is finite V36() set
ss2 is Relation-like NAT -defined proj2 q2 -valued Function-like finite FinSubsequence-like Element of K48(q5)
Seq ss2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
q6 is Relation-like NAT -defined proj2 q2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of proj2 q2
ss2 is Relation-like NAT -defined proj2 q2 -valued Function-like finite FinSubsequence-like Element of K48(C)
ss1 is Relation-like NAT -defined proj2 q2 -valued Function-like finite FinSubsequence-like Element of K48(C)
proj1 ss1 is finite V69() V70() V71() V72() V73() V74() set
Sgm (proj1 ss1) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
proj1 ss2 is finite V69() V70() V71() V72() V73() V74() set
(Sgm (proj1 ss1)) | (proj1 ss2) is Relation-like NAT -defined proj1 ss2 -defined NAT -defined INT -valued RAT -valued Function-like finite FinSubsequence-like V59() V60() V61() V62() Element of K48(K49(NAT,NAT))
proj2 ((Sgm (proj1 ss1)) | (proj1 ss2)) is finite V69() V70() V71() V72() V73() V74() set
ss1 | (proj2 ((Sgm (proj1 ss1)) | (proj1 ss2))) is Relation-like NAT -defined proj2 ((Sgm (proj1 ss1)) | (proj1 ss2)) -defined NAT -defined proj2 q2 -valued Function-like finite FinSubsequence-like set
fss4 is Relation-like NAT -defined proj2 q2 -valued Function-like finite FinSubsequence-like Element of K48(q5)
Seq fss4 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
ss is Relation-like NAT -defined proj2 q2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of proj2 q2
ss1 is Relation-like NAT -defined proj2 q2 -valued Function-like finite FinSubsequence-like Element of K48(C)
proj1 fss4 is finite V69() V70() V71() V72() V73() V74() set
(Sgm (proj1 ss1)) | (proj1 fss4) is Relation-like NAT -defined proj1 fss4 -defined NAT -defined INT -valued RAT -valued Function-like finite FinSubsequence-like V59() V60() V61() V62() Element of K48(K49(NAT,NAT))
proj2 ((Sgm (proj1 ss1)) | (proj1 fss4)) is finite V69() V70() V71() V72() V73() V74() set
ss1 | (proj2 ((Sgm (proj1 ss1)) | (proj1 fss4))) is Relation-like NAT -defined proj2 ((Sgm (proj1 ss1)) | (proj1 fss4)) -defined NAT -defined proj2 q2 -valued Function-like finite FinSubsequence-like set
Seq q4 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
fs2 /\ C is Relation-like finite set
fs2 /\ q3 is Relation-like finite set
fs2 /\ q4 is Relation-like finite set
(fs2 /\ q3) \/ (fs2 /\ q4) is Relation-like finite set
proj1 fs2 is finite V69() V70() V71() V72() V73() V74() set
proj1 q3 is finite V69() V70() V71() V72() V73() V74() set
fs2 \/ q3 is Relation-like finite set
dom q2 is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
(proj1 fs2) \/ (proj1 C) is finite V69() V70() V71() V72() V73() V74() set
proj1 q4 is finite V69() V70() V71() V72() V73() V74() set
(proj1 q3) \/ (proj1 q4) is finite V69() V70() V71() V72() V73() V74() set
(proj1 fs2) \/ ((proj1 q3) \/ (proj1 q4)) is finite V69() V70() V71() V72() V73() V74() set
(proj1 fs2) \/ (proj1 q3) is finite V69() V70() V71() V72() V73() V74() set
((proj1 fs2) \/ (proj1 q3)) \/ (proj1 q4) is finite V69() V70() V71() V72() V73() V74() set
q7 is Relation-like Function-like set
proj1 q7 is set
(proj1 q7) \/ (proj1 q4) is set
len q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
Seg (len q2) is finite len q2 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
q7 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q7 \/ q4 is Relation-like finite set
q7 /\ q4 is Relation-like finite set
q3 /\ q4 is Relation-like finite set
(fs2 /\ q4) \/ (q3 /\ q4) is Relation-like finite set
Seq q7 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
proj2 (Seq q7) is finite set
proj2 q7 is finite set
proj2 q4 is finite set
(proj2 q7) \/ (proj2 q4) is finite set
dom (Seq q7) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
len (Seq q7) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
Seg (len (Seq q7)) is finite len (Seq q7) -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
proj1 q7 is finite V69() V70() V71() V72() V73() V74() set
Sgm (proj1 q7) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm (proj1 q7)) (#) fs2 is Relation-like NAT -defined Function-like finite set
proj1 ((Sgm (proj1 q7)) (#) fs2) is finite V69() V70() V71() V72() V73() V74() set
dom (Sgm (proj1 q7)) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
(Sgm (proj1 q7)) (#) q3 is Relation-like NAT -defined Function-like finite set
proj1 ((Sgm (proj1 q7)) (#) q3) is finite V69() V70() V71() V72() V73() V74() set
C3 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
(Sgm (proj1 q7)) (#) q7 is Relation-like NAT -defined Function-like finite set
q8 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q9 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q8 \/ q9 is Relation-like finite set
proj1 q8 is finite V69() V70() V71() V72() V73() V74() set
(Sgm (proj1 q7)) " (proj1 fs2) is finite set
proj1 q9 is finite V69() V70() V71() V72() V73() V74() set
(Sgm (proj1 q7)) " (proj1 q3) is finite set
(proj1 fs2) /\ (proj1 q3) is finite V69() V70() V71() V72() V73() V74() set
(Sgm (proj1 q7)) " ((proj1 fs2) /\ (proj1 q3)) is finite set
((Sgm (proj1 q7)) " (proj1 fs2)) /\ ((Sgm (proj1 q7)) " (proj1 q3)) is finite set
proj2 (Sgm (proj1 q7)) is finite V69() V70() V71() V72() V73() V74() set
(Sgm (proj1 q7)) | (proj1 q8) is Relation-like NAT -defined proj1 q8 -defined NAT -defined INT -valued RAT -valued Function-like finite FinSubsequence-like V59() V60() V61() V62() Element of K48(K49(NAT,NAT))
proj2 ((Sgm (proj1 q7)) | (proj1 q8)) is finite V69() V70() V71() V72() V73() V74() set
(proj1 fs2) |` (Sgm (proj1 q7)) is Relation-like NAT -defined proj1 fs2 -valued INT -valued Function-like finite FinSubsequence-like V59() V60() V61() set
proj2 ((proj1 fs2) |` (Sgm (proj1 q7))) is finite V69() V70() V71() V72() V73() set
Sgm (proj1 q8) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm (proj1 q7)) * (Sgm (proj1 q8)) is Relation-like NAT -defined INT -valued RAT -valued Function-like finite V59() V60() V61() V62() Element of K48(K49(NAT,NAT))
Sgm (proj2 ((Sgm (proj1 q7)) | (proj1 q8))) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
Seq q8 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(Sgm (proj1 q8)) (#) ((Sgm (proj1 q7)) (#) fs2) is Relation-like NAT -defined Function-like finite set
((Sgm (proj1 q7)) * (Sgm (proj1 q8))) (#) fs2 is Relation-like NAT -defined Function-like finite set
(Sgm (proj1 q7)) | (proj1 q9) is Relation-like NAT -defined proj1 q9 -defined NAT -defined INT -valued RAT -valued Function-like finite FinSubsequence-like V59() V60() V61() V62() Element of K48(K49(NAT,NAT))
proj2 ((Sgm (proj1 q7)) | (proj1 q9)) is finite V69() V70() V71() V72() V73() V74() set
(proj1 q3) |` (Sgm (proj1 q7)) is Relation-like NAT -defined proj1 q3 -valued INT -valued Function-like finite FinSubsequence-like V59() V60() V61() set
proj2 ((proj1 q3) |` (Sgm (proj1 q7))) is finite V69() V70() V71() V72() V73() set
Sgm (proj1 q9) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm (proj1 q7)) * (Sgm (proj1 q9)) is Relation-like NAT -defined INT -valued RAT -valued Function-like finite V59() V60() V61() V62() Element of K48(K49(NAT,NAT))
Sgm (proj2 ((Sgm (proj1 q7)) | (proj1 q9))) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
Seq q9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(Sgm (proj1 q9)) (#) ((Sgm (proj1 q7)) (#) q3) is Relation-like NAT -defined Function-like finite set
((Sgm (proj1 q7)) * (Sgm (proj1 q9))) (#) q3 is Relation-like NAT -defined Function-like finite set
Seq q3 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
c₃₀ is Relation-like NAT -defined Function-like finite FinSubsequence-like set
c₃₁ is Relation-like NAT -defined Function-like finite FinSubsequence-like set
c₃₀ \/ c₃₁ is Relation-like finite set
Seq c₃₀ is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq c₃₁ is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
P is set
N is non empty (P)
N * is non empty functional FinSequence-membered M12(N)
K48((N *)) is set
R is functional FinSequence-membered Element of K48((N *))
x is functional FinSequence-membered Element of K48((N *))
(P,N,R,x) is functional FinSequence-membered Element of K48((N *))
{ (b₁ ^ b₂) where b₁, b₂ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ( b₁ in R & b₂ in x ) } is set
(P,N,R,x) is functional FinSequence-membered Element of K48((N *))
{ b₁ where b₁ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ex b₂, b₃ being Relation-like NAT -defined Function-like finite FinSubsequence-like set st
( b₁ = b₂ \/ b₃ & b₂ misses b₃ & Seq b₂ in R & Seq b₃ in x ) } is set
C is set
q2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
fs2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q2 ^ fs2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
len q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(fs2,(len q2)) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q1 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
q1 \/ (fs2,(len q2)) is Relation-like finite set
Seq q1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq (fs2,(len q2)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
P is set
N is non empty (P)
N * is non empty functional FinSequence-membered M12(N)
K48((N *)) is set
R is functional FinSequence-membered Element of K48((N *))
x is functional FinSequence-membered Element of K48((N *))
C is functional FinSequence-membered Element of K48((N *))
(P,N,R,C) is functional FinSequence-membered Element of K48((N *))
{ (b₁ ^ b₂) where b₁, b₂ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ( b₁ in R & b₂ in C ) } is set
q1 is functional FinSequence-membered Element of K48((N *))
(P,N,x,q1) is functional FinSequence-membered Element of K48((N *))
{ (b₁ ^ b₂) where b₁, b₂ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ( b₁ in x & b₂ in q1 ) } is set
q2 is set
fs2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
C is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
fs2 ^ C is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
P is set
N is non empty (P)
N * is non empty functional FinSequence-membered M12(N)
K48((N *)) is set
R is functional FinSequence-membered Element of K48((N *))
x is functional FinSequence-membered Element of K48((N *))
C is functional FinSequence-membered Element of K48((N *))
(P,N,R,C) is functional FinSequence-membered Element of K48((N *))
{ b₁ where b₁ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ex b₂, b₃ being Relation-like NAT -defined Function-like finite FinSubsequence-like set st
( b₁ = b₂ \/ b₃ & b₂ misses b₃ & Seq b₂ in R & Seq b₃ in C ) } is set
q1 is functional FinSequence-membered Element of K48((N *))
(P,N,x,q1) is functional FinSequence-membered Element of K48((N *))
{ b₁ where b₁ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ex b₂, b₃ being Relation-like NAT -defined Function-like finite FinSubsequence-like set st
( b₁ = b₂ \/ b₃ & b₂ misses b₃ & Seq b₂ in x & Seq b₃ in q1 ) } is set
q2 is set
fs2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
C is Relation-like NAT -defined Function-like finite FinSubsequence-like set
C3 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
C \/ C3 is Relation-like finite set
Seq C is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq C3 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
N is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P ^ N is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (P ^ N) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
R is Relation-like NAT -defined Function-like finite FinSubsequence-like set
x is Relation-like NAT -defined Function-like finite FinSubsequence-like set
(x,(len P)) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
R \/ (x,(len P)) is Relation-like finite set
proj1 (R \/ (x,(len P))) is finite set
proj1 R is finite V69() V70() V71() V72() V73() V74() set
dom P is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
proj1 x is finite V69() V70() V71() V72() V73() V74() set
dom N is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
C is set
proj1 (x,(len P)) is finite V69() V70() V71() V72() V73() V74() set
(proj1 R) \/ (proj1 (x,(len P))) is finite V69() V70() V71() V72() V73() V74() set
len N is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(len P) + (len N) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
Seg ((len P) + (len N)) is finite (len P) + (len N) -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
Seg (len P) is finite len P -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
(N,(len P)) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 (N,(len P)) is finite V69() V70() V71() V72() V73() V74() set
q1 is set
{ ((len P) + b₁) where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : b₁ in dom N } is set
{ ((len P) + b₁) where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : b₁ in proj1 x } is set
q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(len P) + q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P \/ (N,(len P)) is Relation-like finite set
proj1 (P \/ (N,(len P))) is finite set
(dom P) \/ (proj1 (N,(len P))) is finite V69() V70() V71() V72() V73() V74() set
N is Relation-like NAT -defined Function-like finite FinSubsequence-like set
P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
R is Relation-like NAT -defined Function-like finite FinSubsequence-like set
len P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(R,(len P)) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
R is Relation-like NAT -defined Function-like finite FinSubsequence-like set
N is Relation-like NAT -defined Function-like finite FinSubsequence-like set
(R,P) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 (R,P) is finite V69() V70() V71() V72() V73() V74() set
(N,P) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 (N,P) is finite V69() V70() V71() V72() V73() V74() set
proj1 R is finite V69() V70() V71() V72() V73() V74() set
{ (P + b₁) where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : b₁ in proj1 R } is set
proj1 N is finite V69() V70() V71() V72() V73() V74() set
{ (P + b₁) where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : b₁ in proj1 N } is set
x is set
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P + C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
R is Relation-like NAT -defined Function-like finite FinSubsequence-like set
N is Relation-like NAT -defined Function-like finite FinSubsequence-like set
(R,P) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
(N,P) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 (R,P) is finite V69() V70() V71() V72() V73() V74() set
proj1 R is finite V69() V70() V71() V72() V73() V74() set
{ (P + b₁) where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : b₁ in proj1 R } is set
proj1 (N,P) is finite V69() V70() V71() V72() V73() V74() set
proj1 N is finite V69() V70() V71() V72() V73() V74() set
{ (P + b₁) where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : b₁ in proj1 N } is set
x is set
C is set
[x,C] is V13() set
{x,C} is non empty finite set
{x} is non empty V17() finite 1 -element set
{{x,C},{x}} is non empty finite V36() set
(R,P) . x is set
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P + q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
R . q1 is set
N . q1 is set
(N,P) . x is set
N is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(N,(len P)) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
P ^ N is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
proj1 (N,(len P)) is finite V69() V70() V71() V72() V73() V74() set
dom N is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
{ ((len P) + b₁) where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : b₁ in dom N } is set
(len P) + 1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
len N is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(len P) + (len N) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
{ b₁ where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : ( (len P) + 1 <= b₁ & b₁ <= (len P) + (len N) ) } is set
dom (P ^ N) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
Seg ((len P) + (len N)) is finite (len P) + (len N) -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
{ b₁ where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : ( 1 <= b₁ & b₁ <= (len P) + (len N) ) } is set
R is set
x is set
[R,x] is V13() set
{R,x} is non empty finite set
{R} is non empty V17() finite 1 -element set
{{R,x},{R}} is non empty finite V36() set
(N,(len P)) . R is set
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(len P) + q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N . q1 is set
(P ^ N) . R is set
P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 N is finite V69() V70() V71() V72() V73() V74() set
(N,P) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 (N,P) is finite V69() V70() V71() V72() V73() V74() set
R is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 R is finite V69() V70() V71() V72() V73() V74() set
(R,P) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 (R,P) is finite V69() V70() V71() V72() V73() V74() set
{ (P + b₁) where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : b₁ in proj1 N } is set
{ (P + b₁) where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : b₁ in proj1 R } is set
(proj1 (N,P)) /\ (proj1 (R,P)) is finite V69() V70() V71() V72() V73() V74() set
x is set
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P + C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(proj1 N) /\ (proj1 R) is finite V69() V70() V71() V72() V73() V74() set
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P + q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N is Relation-like NAT -defined Function-like finite FinSubsequence-like set
R is Relation-like NAT -defined Function-like finite FinSubsequence-like set
x is Relation-like NAT -defined Function-like finite FinSubsequence-like set
R \/ x is Relation-like finite set
(R,P) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
(x,P) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
(R,P) \/ (x,P) is Relation-like finite set
(N,P) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 (N,P) is finite V69() V70() V71() V72() V73() V74() set
proj1 N is finite V69() V70() V71() V72() V73() V74() set
{ (P + b₁) where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : b₁ in proj1 N } is set
proj1 (R,P) is finite V69() V70() V71() V72() V73() V74() set
proj1 R is finite V69() V70() V71() V72() V73() V74() set
{ (P + b₁) where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : b₁ in proj1 R } is set
proj1 (x,P) is finite V69() V70() V71() V72() V73() V74() set
proj1 x is finite V69() V70() V71() V72() V73() V74() set
{ (P + b₁) where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : b₁ in proj1 x } is set
q1 is set
q2 is set
[q1,q2] is V13() set
{q1,q2} is non empty finite set
{q1} is non empty V17() finite 1 -element set
{{q1,q2},{q1}} is non empty finite V36() set
C is Relation-like Function-like set
proj1 C is set
(proj1 (R,P)) \/ (proj1 (x,P)) is finite V69() V70() V71() V72() V73() V74() set
(R,P) . q1 is set
(N,P) . q1 is set
[q1,((N,P) . q1)] is V13() set
{q1,((N,P) . q1)} is non empty finite set
{{q1,((N,P) . q1)},{q1}} is non empty finite V36() set
(x,P) . q1 is set
(N,P) . q1 is set
fs2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P + fs2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(proj1 R) \/ (proj1 x) is finite V69() V70() V71() V72() V73() V74() set
(proj1 (R,P)) \/ (proj1 (x,P)) is finite V69() V70() V71() V72() V73() V74() set
C is Relation-like Function-like set
proj1 C is set
N . fs2 is set
R . fs2 is set
(R,P) . q1 is set
C . q1 is set
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P + C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P + C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
x . fs2 is set
(x,P) . q1 is set
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P + C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P + C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N is Relation-like NAT -defined Function-like finite FinSubsequence-like set
Seq N is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (Seq N) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
(N,P) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
Seq (N,P) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (Seq (N,P)) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
card N is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
card (N,P) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
len (Seq N) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
len (Seq (N,P)) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
Seg (len (Seq N)) is finite len (Seq N) -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
R is Relation-like NAT -defined Function-like finite FinSubsequence-like set
Seq R is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (Seq R) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
proj1 R is finite V69() V70() V71() V72() V73() V74() set
Sgm (proj1 R) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm (proj1 R)) . P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(R,N) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 (R,N) is finite V69() V70() V71() V72() V73() V74() set
Sgm (proj1 (R,N)) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm (proj1 (R,N))) . P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
x is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 x is finite V69() V70() V71() V72() V73() V74() set
proj2 x is finite set
Seq x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
proj2 (Seq x) is finite set
proj2 (Sgm (proj1 R)) is finite V69() V70() V71() V72() V73() V74() set
(Sgm (proj1 R)) (#) R is Relation-like NAT -defined Function-like finite set
proj1 ((Sgm (proj1 R)) (#) R) is finite V69() V70() V71() V72() V73() V74() set
dom (Sgm (proj1 R)) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(Sgm (proj1 R)) . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(Seq x) . C is set
Sgm (proj1 x) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm (proj1 x)) (#) x is Relation-like NAT -defined Function-like finite set
((Sgm (proj1 x)) (#) x) . C is set
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
x . q1 is set
N + q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
proj2 (Sgm (proj1 (R,N))) is finite V69() V70() V71() V72() V73() V74() set
dom (Seq x) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
Sgm (proj1 x) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm (proj1 x)) (#) x is Relation-like NAT -defined Function-like finite set
proj1 ((Sgm (proj1 x)) (#) x) is finite V69() V70() V71() V72() V73() V74() set
C is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
len C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
fs2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
C . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
C . q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
dom C is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
Seg (len C) is finite len C -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
{ b₁ where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : ( 1 <= b₁ & b₁ <= len C ) } is set
C3 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
C3 + 1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(len C) - 1 is V24() V25() integer ext-real set
(len C) + 0 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(len C) + 1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(Sgm (proj1 R)) . C3 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
C . C3 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N + q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(Sgm (proj1 R)) . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
C . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
C4 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N + C4 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
len (Sgm (proj1 R)) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q3 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
Seg q3 is finite q3 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
Seg q1 is finite q1 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
R is Relation-like NAT -defined Function-like finite FinSubsequence-like set
Seq R is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (Seq R) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
(R,N) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
Seq (R,N) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(Seq (R,N)) . P is set
(Seq R) . P is set
proj1 R is finite V69() V70() V71() V72() V73() V74() set
Sgm (proj1 R) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm (proj1 R)) . P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
proj1 (R,N) is finite V69() V70() V71() V72() V73() V74() set
Sgm (proj1 (R,N)) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm (proj1 (R,N))) . P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N + x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
proj2 (Sgm (proj1 R)) is finite V69() V70() V71() V72() V73() V74() set
dom (Seq (R,N)) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
(Sgm (proj1 (R,N))) (#) (R,N) is Relation-like NAT -defined Function-like finite set
proj1 ((Sgm (proj1 (R,N))) (#) (R,N)) is finite V69() V70() V71() V72() V73() V74() set
(Sgm (proj1 R)) (#) R is Relation-like NAT -defined Function-like finite set
proj1 ((Sgm (proj1 R)) (#) R) is finite V69() V70() V71() V72() V73() V74() set
dom (Sgm (proj1 R)) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
((Sgm (proj1 (R,N))) (#) (R,N)) . P is set
(R,N) . ((Sgm (proj1 (R,N))) . P) is set
R . x is set
((Sgm (proj1 R)) (#) R) . P is set
P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N is Relation-like NAT -defined Function-like finite FinSubsequence-like set
Seq N is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(N,P) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
Seq (N,P) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (Seq N) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
dom (Seq (N,P)) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
R is set
(Seq (N,P)) . R is set
(Seq N) . R is set
P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
Seg P is finite P -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
N is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N + P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
Seg (N + P) is finite N + P -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
R is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 R is finite V69() V70() V71() V72() V73() V74() set
(R,N) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 (R,N) is finite V69() V70() V71() V72() V73() V74() set
{ (N + b₁) where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : b₁ in proj1 R } is set
{ b₁ where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : ( 1 <= b₁ & b₁ <= P ) } is set
{ b₁ where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : ( 1 <= b₁ & b₁ <= N + P ) } is set
x is set
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N + C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
0 + 1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N is Relation-like NAT -defined Function-like finite FinSubsequence-like set
R is Relation-like NAT -defined Function-like finite FinSubsequence-like set
(R,(len P)) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
N \/ (R,(len P)) is Relation-like finite set
proj1 N is finite V69() V70() V71() V72() V73() V74() set
dom P is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
proj1 (R,(len P)) is finite V69() V70() V71() V72() V73() V74() set
Seg (len P) is finite len P -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
proj1 R is finite V69() V70() V71() V72() V73() V74() set
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
Seg C is finite C -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
(len P) + C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
Seg ((len P) + C) is finite (len P) + C -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
(len P) + 0 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(proj1 N) \/ (proj1 (R,(len P))) is finite V69() V70() V71() V72() V73() V74() set
proj1 (N \/ (R,(len P))) is finite set
x is Relation-like Function-like set
q1 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
N is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
R is Relation-like NAT -defined Function-like finite FinSubsequence-like set
x is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 R is finite V69() V70() V71() V72() V73() V74() set
(x,(len P)) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 (x,(len P)) is finite V69() V70() V71() V72() V73() V74() set
(proj1 R) \/ (proj1 (x,(len P))) is finite V69() V70() V71() V72() V73() V74() set
Sgm ((proj1 R) \/ (proj1 (x,(len P)))) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
Sgm (proj1 R) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
Sgm (proj1 (x,(len P))) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm (proj1 R)) ^ (Sgm (proj1 (x,(len P)))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
dom P is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
Seg (len P) is finite len P -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
{ b₁ where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : ( 1 <= b₁ & b₁ <= len P ) } is set
(N,(len P)) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 (N,(len P)) is finite V69() V70() V71() V72() V73() V74() set
(len P) + 1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
len N is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(len P) + (len N) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
{ b₁ where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : ( (len P) + 1 <= b₁ & b₁ <= (len P) + (len N) ) } is set
q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
fs2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
Seg C is finite C -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
Seg q1 is finite q1 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
N is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
R is Relation-like NAT -defined Function-like finite FinSubsequence-like set
x is Relation-like NAT -defined Function-like finite FinSubsequence-like set
(x,(len P)) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
R \/ (x,(len P)) is Relation-like finite set
Seq R is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (Seq R) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
Seq x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (Seq x) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(len (Seq R)) + (len (Seq x)) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
Seg ((len (Seq R)) + (len (Seq x))) is finite (len (Seq R)) + (len (Seq x)) -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
C is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 R is finite V69() V70() V71() V72() V73() V74() set
proj1 (x,(len P)) is finite V69() V70() V71() V72() V73() V74() set
proj1 C is finite V69() V70() V71() V72() V73() V74() set
Sgm (proj1 C) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
proj2 (Sgm (proj1 C)) is finite V69() V70() V71() V72() V73() V74() set
Seq C is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (Seq C) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
(Sgm (proj1 C)) (#) C is Relation-like NAT -defined Function-like finite set
proj1 ((Sgm (proj1 C)) (#) C) is finite V69() V70() V71() V72() V73() V74() set
dom (Sgm (proj1 C)) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
(proj1 R) \/ (proj1 (x,(len P))) is finite V69() V70() V71() V72() V73() V74() set
Sgm ((proj1 R) \/ (proj1 (x,(len P)))) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
dom (Sgm ((proj1 R) \/ (proj1 (x,(len P))))) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
Sgm (proj1 R) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
Sgm (proj1 (x,(len P))) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm (proj1 R)) ^ (Sgm (proj1 (x,(len P)))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
dom ((Sgm (proj1 R)) ^ (Sgm (proj1 (x,(len P))))) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
len (Sgm (proj1 R)) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
len (Sgm (proj1 (x,(len P)))) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(len (Sgm (proj1 R))) + (len (Sgm (proj1 (x,(len P))))) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
Seg ((len (Sgm (proj1 R))) + (len (Sgm (proj1 (x,(len P)))))) is finite (len (Sgm (proj1 R))) + (len (Sgm (proj1 (x,(len P))))) -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
card (proj1 (x,(len P))) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
Seg q1 is finite q1 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
card (proj1 R) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
Seg q1 is finite q1 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
card (x,(len P)) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
card x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
card R is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
N is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
R is Relation-like NAT -defined Function-like finite FinSubsequence-like set
x is Relation-like NAT -defined Function-like finite FinSubsequence-like set
(x,(len P)) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
R \/ (x,(len P)) is Relation-like finite set
Seq R is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (Seq R) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
Seq x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (Seq x) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(len (Seq R)) + (len (Seq x)) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
Seg ((len (Seq R)) + (len (Seq x))) is finite (len (Seq R)) + (len (Seq x)) -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
((Seq x),(len (Seq R))) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
(Seq R) \/ ((Seq x),(len (Seq R))) is Relation-like finite set
C is Relation-like NAT -defined Function-like finite FinSubsequence-like set
Seq C is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (Seq C) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
{ b₁ where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : ( 1 <= b₁ & b₁ <= (len (Seq R)) + (len (Seq x)) ) } is set
dom (Seq R) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
Seg (len (Seq R)) is finite len (Seq R) -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
{ b₁ where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : ( 1 <= b₁ & b₁ <= len (Seq R) ) } is set
proj1 ((Seq x),(len (Seq R))) is finite V69() V70() V71() V72() V73() V74() set
(len (Seq R)) + 1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
{ b₁ where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : ( (len (Seq R)) + 1 <= b₁ & b₁ <= (len (Seq R)) + (len (Seq x)) ) } is set
(dom (Seq R)) \/ (proj1 ((Seq x),(len (Seq R)))) is finite V69() V70() V71() V72() V73() V74() set
q1 is set
q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q1 is set
q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(len (Seq R)) + 0 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
0 + 1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
proj1 ((Seq R) \/ ((Seq x),(len (Seq R)))) is finite set
q1 is Relation-like Function-like set
q2 is set
(Seq C) . q2 is set
q1 . q2 is set
proj1 C is finite V69() V70() V71() V72() V73() V74() set
Sgm (proj1 C) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm (proj1 C)) (#) C is Relation-like NAT -defined Function-like finite set
proj1 ((Sgm (proj1 C)) (#) C) is finite V69() V70() V71() V72() V73() V74() set
((Sgm (proj1 C)) (#) C) . q2 is set
(Sgm (proj1 C)) . q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
C . ((Sgm (proj1 C)) . q2) is set
proj1 R is finite V69() V70() V71() V72() V73() V74() set
proj1 (x,(len P)) is finite V69() V70() V71() V72() V73() V74() set
(proj1 R) \/ (proj1 (x,(len P))) is finite V69() V70() V71() V72() V73() V74() set
Sgm ((proj1 R) \/ (proj1 (x,(len P)))) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm ((proj1 R) \/ (proj1 (x,(len P))))) . q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
C . ((Sgm ((proj1 R) \/ (proj1 (x,(len P))))) . q2) is set
Sgm (proj1 R) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
Sgm (proj1 (x,(len P))) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm (proj1 R)) ^ (Sgm (proj1 (x,(len P)))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
((Sgm (proj1 R)) ^ (Sgm (proj1 (x,(len P))))) . q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
C . (((Sgm (proj1 R)) ^ (Sgm (proj1 (x,(len P))))) . q2) is set
dom (Sgm (proj1 R)) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
(Sgm (proj1 R)) . q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
proj2 (Sgm (proj1 R)) is finite V69() V70() V71() V72() V73() V74() set
C . ((Sgm (proj1 R)) . q2) is set
R . ((Sgm (proj1 R)) . q2) is set
(Sgm (proj1 R)) (#) R is Relation-like NAT -defined Function-like finite set
((Sgm (proj1 R)) (#) R) . q2 is set
(Seq R) . q2 is set
dom (Seq x) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
{ ((len (Seq R)) + b₁) where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : b₁ in dom (Seq x) } is set
fs2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(len (Seq R)) + fs2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
((Seq x),(len (Seq R))) . q2 is set
(Seq x) . fs2 is set
card (proj1 R) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
len (Sgm (proj1 R)) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
Seg C is finite C -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
card R is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
Seg (len (Seq x)) is finite len (Seq x) -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
card x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
card (x,(len P)) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
card (proj1 (x,(len P))) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
len (Sgm (proj1 (x,(len P)))) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
Seg C is finite C -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
Seg C is finite C -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
dom (Sgm (proj1 (x,(len P)))) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
(Sgm (proj1 (x,(len P)))) . fs2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
proj2 (Sgm (proj1 (x,(len P)))) is finite V69() V70() V71() V72() V73() V74() set
C . ((Sgm (proj1 (x,(len P)))) . fs2) is set
(x,(len P)) . ((Sgm (proj1 (x,(len P)))) . fs2) is set
(Sgm (proj1 (x,(len P)))) (#) (x,(len P)) is Relation-like NAT -defined Function-like finite set
((Sgm (proj1 (x,(len P)))) (#) (x,(len P))) . fs2 is set
Seq (x,(len P)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(Seq (x,(len P))) . fs2 is set
P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
N is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
R is Relation-like NAT -defined Function-like finite FinSubsequence-like set
x is Relation-like NAT -defined Function-like finite FinSubsequence-like set
(x,(len P)) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
R \/ (x,(len P)) is Relation-like finite set
Seq R is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(Seq R) ^ (Seq x) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (Seq R) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
len (Seq x) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(len (Seq R)) + (len (Seq x)) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
Seg ((len (Seq R)) + (len (Seq x))) is finite (len (Seq R)) + (len (Seq x)) -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
((Seq x),(len (Seq R))) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
(Seq R) \/ ((Seq x),(len (Seq R))) is Relation-like finite set
C is Relation-like NAT -defined Function-like finite FinSubsequence-like set
Seq C is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (Seq C) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
dom (Seq R) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(Seq C) . q1 is set
(Seq R) . q1 is set
dom (Seq x) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(len (Seq R)) + q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(Seq C) . ((len (Seq R)) + q1) is set
(Seq x) . q1 is set
proj1 ((Seq x),(len (Seq R))) is finite V69() V70() V71() V72() V73() V74() set
{ ((len (Seq R)) + b₁) where b₁ is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT : b₁ in dom (Seq x) } is set
((Seq x),(len (Seq R))) . ((len (Seq R)) + q1) is set
P is set
N is non empty (P)
N * is non empty functional FinSequence-membered M12(N)
K48((N *)) is set
R is functional FinSequence-membered Element of K48((N *))
x is functional FinSequence-membered Element of K48((N *))
(P,N,R,x) is functional FinSequence-membered Element of K48((N *))
{ b₁ where b₁ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ex b₂, b₃ being Relation-like NAT -defined Function-like finite FinSubsequence-like set st
( b₁ = b₂ \/ b₃ & b₂ misses b₃ & Seq b₂ in R & Seq b₃ in x ) } is set
C is functional FinSequence-membered Element of K48((N *))
(P,N,R,C) is functional FinSequence-membered Element of K48((N *))
{ (b₁ ^ b₂) where b₁, b₂ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ( b₁ in R & b₂ in C ) } is set
q1 is functional FinSequence-membered Element of K48((N *))
(P,N,C,q1) is functional FinSequence-membered Element of K48((N *))
{ b₁ where b₁ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ex b₂, b₃ being Relation-like NAT -defined Function-like finite FinSubsequence-like set st
( b₁ = b₂ \/ b₃ & b₂ misses b₃ & Seq b₂ in C & Seq b₃ in q1 ) } is set
(P,N,(P,N,R,x),(P,N,C,q1)) is functional FinSequence-membered Element of K48((N *))
{ (b₁ ^ b₂) where b₁, b₂ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ( b₁ in (P,N,R,x) & b₂ in (P,N,C,q1) ) } is set
(P,N,x,q1) is functional FinSequence-membered Element of K48((N *))
{ (b₁ ^ b₂) where b₁, b₂ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ( b₁ in x & b₂ in q1 ) } is set
(P,N,(P,N,R,C),(P,N,x,q1)) is functional FinSequence-membered Element of K48((N *))
{ b₁ where b₁ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ex b₂, b₃ being Relation-like NAT -defined Function-like finite FinSubsequence-like set st
( b₁ = b₂ \/ b₃ & b₂ misses b₃ & Seq b₂ in (P,N,R,C) & Seq b₃ in (P,N,x,q1) ) } is set
q2 is set
fs2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
C is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
fs2 ^ C is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
C3 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q1 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q2 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q1 \/ q2 is Relation-like finite set
Seq q1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq q2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
q1 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q2 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q1 \/ q2 is Relation-like finite set
Seq q1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq q2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
C4 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q3 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q4 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q3 \/ q4 is Relation-like finite set
Seq q3 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq q4 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
q3 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q4 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q3 \/ q4 is Relation-like finite set
Seq q3 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq q4 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len fs2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(q3,(len fs2)) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
(q4,(len fs2)) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q5 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
ss is Relation-like NAT -defined Function-like finite FinSubsequence-like set
(ss,(len fs2)) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q6 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
(C,(len fs2)) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj1 q1 is finite V69() V70() V71() V72() V73() V74() set
proj1 q5 is finite V69() V70() V71() V72() V73() V74() set
proj1 q2 is finite V69() V70() V71() V72() V73() V74() set
proj1 q6 is finite V69() V70() V71() V72() V73() V74() set
q1 \/ q5 is Relation-like finite set
q2 \/ q6 is Relation-like finite set
C is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
dom C is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
len C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
Seg (len C) is finite len C -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
ss1 is Relation-like Function-like set
proj1 ss1 is set
ss2 is Relation-like Function-like set
proj1 ss2 is set
ss1 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
ss2 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
ss1 \/ ss2 is Relation-like finite set
q1 \/ (q3,(len fs2)) is Relation-like finite set
(q1 \/ (q3,(len fs2))) \/ q2 is Relation-like finite set
((q1 \/ (q3,(len fs2))) \/ q2) \/ (q4,(len fs2)) is Relation-like finite set
(q1 \/ q2) \/ (q3,(len fs2)) is Relation-like finite set
((q1 \/ q2) \/ (q3,(len fs2))) \/ (q4,(len fs2)) is Relation-like finite set
(q3,(len fs2)) \/ (q4,(len fs2)) is Relation-like finite set
fs2 \/ ((q3,(len fs2)) \/ (q4,(len fs2))) is Relation-like finite set
fs2 \/ (C,(len fs2)) is Relation-like finite set
ss1 /\ q2 is Relation-like finite set
q1 /\ q2 is Relation-like finite set
(q3,(len fs2)) /\ q2 is Relation-like finite set
(q1 /\ q2) \/ ((q3,(len fs2)) /\ q2) is Relation-like finite set
ss1 /\ (q4,(len fs2)) is Relation-like finite set
q1 /\ (q4,(len fs2)) is Relation-like finite set
(q3,(len fs2)) /\ (q4,(len fs2)) is Relation-like finite set
(q1 /\ (q4,(len fs2))) \/ ((q3,(len fs2)) /\ (q4,(len fs2))) is Relation-like finite set
ss1 /\ ss2 is Relation-like finite set
((q1 /\ q2) \/ ((q3,(len fs2)) /\ q2)) \/ ((q1 /\ (q4,(len fs2))) \/ ((q3,(len fs2)) /\ (q4,(len fs2)))) is Relation-like finite set
proj1 q3 is finite V69() V70() V71() V72() V73() V74() set
proj1 q4 is finite V69() V70() V71() V72() V73() V74() set
proj1 (q3,(len fs2)) is finite V69() V70() V71() V72() V73() V74() set
proj1 (q4,(len fs2)) is finite V69() V70() V71() V72() V73() V74() set
(Seq q1) ^ (Seq q3) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(Seq q2) ^ (Seq q4) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq ss1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
fss4 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
Seq fss4 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq ss2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
fss4 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
Seq fss4 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
P is set
N is non empty (P)
N * is non empty functional FinSequence-membered M12(N)
K48((N *)) is set
R is non empty functional FinSequence-membered Element of K48((N *))
x is non empty functional FinSequence-membered Element of K48((N *))
(P,N,R,x) is functional FinSequence-membered Element of K48((N *))
{ b₁ where b₁ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ex b₂, b₃ being Relation-like NAT -defined Function-like finite FinSubsequence-like set st
( b₁ = b₂ \/ b₃ & b₂ misses b₃ & Seq b₂ in R & Seq b₃ in x ) } is set
C is set
q1 is set
q2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
fs2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q2 ^ fs2 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
C is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
len q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
(fs2,(len q2)) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q2 \/ (fs2,(len q2)) is Relation-like finite set
Seq q2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq (fs2,(len q2)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
P is set
N is non empty (P)
N * is non empty functional FinSequence-membered M12(N)
<*> N is Relation-like non-empty empty-yielding NAT -defined N -valued V6() V7() V8() V10() V11() V12() empty Function-like one-to-one constant functional V24() V25() Function-yielding finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FuncSeq-like integer ext-real V59() V60() V61() V62() V69() V70() V71() V72() V73() V74() V75() Element of N *
{(<*> N)} is non empty V17() functional finite V36() 1 -element FinSequence-membered V69() V70() V71() V72() V73() V74() Element of K48((N *))
K48((N *)) is set
P is set
N is non empty (P)
N * is non empty functional FinSequence-membered M12(N)
R is (P,N)
<*R*> is Relation-like NAT -defined N -valued non empty V17() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like Element of N *
{<*R*>} is non empty V17() functional finite V36() 1 -element FinSequence-membered Element of K48((N *))
K48((N *)) is set
P is set
N is non empty (P)
N * is non empty functional FinSequence-membered M12(N)
K48((N *)) is set
(P,N) is non empty functional FinSequence-membered Element of K48((N *))
<*> N is Relation-like non-empty empty-yielding NAT -defined N -valued V6() V7() V8() V10() V11() V12() empty Function-like one-to-one constant functional V24() V25() Function-yielding finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FuncSeq-like integer ext-real V59() V60() V61() V62() V69() V70() V71() V72() V73() V74() V75() Element of N *
{(<*> N)} is non empty V17() functional finite V36() 1 -element FinSequence-membered V69() V70() V71() V72() V73() V74() Element of K48((N *))
R is functional FinSequence-membered Element of K48((N *))
(P,N,(P,N),R) is functional FinSequence-membered Element of K48((N *))
{ (b₁ ^ b₂) where b₁, b₂ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ( b₁ in (P,N) & b₂ in R ) } is set
x is set
C is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q1 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
C ^ q1 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
x is set
C is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
(<*> N) ^ C is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
P is set
N is non empty (P)
N * is non empty functional FinSequence-membered M12(N)
K48((N *)) is set
(P,N) is non empty functional FinSequence-membered Element of K48((N *))
<*> N is Relation-like non-empty empty-yielding NAT -defined N -valued V6() V7() V8() V10() V11() V12() empty Function-like one-to-one constant functional V24() V25() Function-yielding finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FuncSeq-like integer ext-real V59() V60() V61() V62() V69() V70() V71() V72() V73() V74() V75() Element of N *
{(<*> N)} is non empty V17() functional finite V36() 1 -element FinSequence-membered V69() V70() V71() V72() V73() V74() Element of K48((N *))
R is functional FinSequence-membered Element of K48((N *))
(P,N,R,(P,N)) is functional FinSequence-membered Element of K48((N *))
{ (b₁ ^ b₂) where b₁, b₂ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ( b₁ in R & b₂ in (P,N) ) } is set
x is set
C is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q1 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
C ^ q1 is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
x is set
C is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
C ^ (<*> N) is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
P is set
N is non empty (P)
N * is non empty functional FinSequence-membered M12(N)
K48((N *)) is set
(P,N) is non empty functional FinSequence-membered Element of K48((N *))
<*> N is Relation-like non-empty empty-yielding NAT -defined N -valued V6() V7() V8() V10() V11() V12() empty Function-like one-to-one constant functional V24() V25() Function-yielding finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FuncSeq-like integer ext-real V59() V60() V61() V62() V69() V70() V71() V72() V73() V74() V75() Element of N *
{(<*> N)} is non empty V17() functional finite V36() 1 -element FinSequence-membered V69() V70() V71() V72() V73() V74() Element of K48((N *))
R is functional FinSequence-membered Element of K48((N *))
(P,N,(P,N),R) is functional FinSequence-membered Element of K48((N *))
{ b₁ where b₁ is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N * : ex b₂, b₃ being Relation-like NAT -defined Function-like finite FinSubsequence-like set st
( b₁ = b₂ \/ b₃ & b₂ misses b₃ & Seq b₂ in (P,N) & Seq b₃ in R ) } is set
x is set
C is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q1 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q2 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q1 \/ q2 is Relation-like finite set
Seq q1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq q2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
q1 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q2 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q1 \/ q2 is Relation-like finite set
Seq q1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seq q2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
x is set
C is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
q1 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q2 is Relation-like NAT -defined Function-like finite FinSubsequence-like set
q1 /\ q2 is Relation-like finite set
Seq q2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
{} \/ q2 is Relation-like finite set
Seq q1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set