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

K49(F

K48(K49(F

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

N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(F

R is set

N . R is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set

F

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(