:: AFINSQ_2 semantic presentation

K19(REAL) is V12() non finite set
COMPLEX is non empty V12() non finite complex-membered V56() set

K19(K20(NAT,REAL)) is V12() non finite set

K19(NAT) is V12() non finite set
K19(NAT) is V12() non finite set
K249(NAT) is V70() set

K19(K20(COMPLEX,COMPLEX)) is V12() non finite set

K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is V12() non finite set

K19(K20(REAL,REAL)) is V12() non finite set

K19(K20(K20(REAL,REAL),REAL)) is V12() non finite set

K19(K20(RAT,RAT)) is V12() non finite set

K19(K20(K20(RAT,RAT),RAT)) is V12() non finite set

K19(K20(INT,INT)) is V12() non finite set

K19(K20(K20(INT,INT),INT)) is V12() non finite set

K19(K20(K20(NAT,NAT),NAT)) is V12() non finite set

x is finite set
p is finite set

p \ x is finite Element of K19(p)
K19(p) is finite V48() set

x is finite set
p is finite set
K20(x,p) is Relation-like finite set
K19(K20(x,p)) is finite V48() set

dom q is finite Element of K19(x)
K19(x) is finite V48() set
y is set
r is set
q . y is set
q . r is set
{y} is non empty V12() finite 1 -element set
x \ {y} is finite Element of K19(x)
c6 is finite set
q .: c6 is finite Element of K19(p)
K19(p) is finite V48() set
c is set
rng q is finite Element of K19(p)
b is set
q . b is set

dom q is finite Element of K19(x)
K19(x) is finite V48() set
q .: (dom q) is finite Element of K19(p)
K19(p) is finite V48() set

rng q is finite Element of K19(p)
y is set

{y} is non empty V12() finite 1 -element set
p \ {y} is finite Element of K19(p)

p is set

p is set

rng p is set
dom p is set

(c6 + 1) - 1 is ext-real complex real integer rational Element of INT

(c6 + 1) - 1 is ext-real complex real integer rational Element of INT

(c6 + 1) - 1 is ext-real complex real integer rational Element of INT

c is set
b is set

x is set

rng p is finite set

q is set
p . q is set
x is set

rng p is finite set
q is set

p . y is set
F2() is non empty set

x . p is set

x . q is set
F3(q) is Element of F2()

p . q is set
F3(q) is Element of F2()

dom (- x) is set

dom (x ") is set

dom (x ^2) is set

dom |.x.| is set

dom (x + p) is set

dom (x (#) p) is set

dom x is finite set
dom (- x) is set

dom x is finite set
dom (x ") is set

dom x is finite set
dom (x ^2) is set

dom x is finite set
dom |.x.| is set

dom (x + p) is set
dom x is finite set
dom p is set
(dom x) /\ (dom p) is finite set

dom (x (#) p) is set
dom x is finite set
dom p is set
(dom x) /\ (dom p) is finite set

p is complex set

dom (p + x) is set

- p is complex set

dom (p (#) x) is set

p is complex set

dom x is finite set
dom (p + x) is set

- p is complex set

dom x is finite set
dom (p (#) x) is set

p . y is set

(len x) - (y + 1) is ext-real complex real integer rational Element of INT
x . ((len x) - (y + 1)) is set
q . y is set

rng x is finite set
rng (x) is finite set

p is set
q is set
x . q is set

(len x) - (y + 1) is ext-real complex real integer rational Element of INT

(x) . r is set

(len x) - (r + 1) is ext-real complex real integer rational Element of INT
x . ((len x) - (r + 1)) is set
p is set
q is set
(x) . q is set

(len x) - (y + 1) is ext-real complex real integer rational Element of INT

(x) . y is set
x . ((len x) - (y + 1)) is set
x is set

rng p is finite Element of K19(x)
K19(x) is set
rng (p) is finite set

y . r is set

x . (r + p) is set

q . r is set

x . (r + p) is set
y . r is set

(len p) - x is ext-real complex real Element of REAL

(q,p) . x is set
q . (x + p) is set
(len q) - p is ext-real complex real Element of REAL

q is set

y is set
(x,p) . q is set
(x,p) . y is set

(len x) - p is ext-real complex real Element of REAL

(x,p) . c6 is set
x . (c6 + p) is set
(x,p) . r is set
x . (r + p) is set

rng (p,x) is finite set
rng p is finite set
q is set

y is set
(p,x) . y is set

(len p) - x is ext-real complex real Element of REAL

(p,x) . r is set
p . (r + x) is set

(x,0) . p is set

x . (p + 0) is set
x . p is set

((p ^ q),((len p) + x)) is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

(len (p ^ q)) - ((len p) + x) is ext-real complex real integer rational Element of INT

((len q) + (len p)) - ((len p) + x) is ext-real complex real integer rational Element of INT
(len q) - x is ext-real complex real Element of REAL

((p ^ q),((len p) + x)) . y is set

(p ^ q) . (((len p) + x) + y) is set

(p ^ q) . ((len p) + (x + y)) is set
q . (x + y) is set
(q,x) . y is set

((x ^ p),(len x)) is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

((x ^ p),((len x) + 0)) is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

rng p is finite set

(len p) - x is ext-real complex real Element of REAL

((p | x) ^ (p,x)) . r is set
(p | x) . r is set
p . r is set

max (0,(r - x)) is ext-real complex real set

((p | x) ^ (p,x)) . r is set
(p,x) . c6 is set

p . (c6 + x) is set
p . r is set
((p | x) ^ (p,x)) . r is set
p . r is set
((p | x) ^ (p,x)) . r is set
p . r is set

x + ((len p) - x) is ext-real complex real Element of REAL

x is set

(len p) - q is ext-real complex real Element of REAL

rng (p,q) is finite set
rng p is finite Element of K19(x)
K19(x) is set
c6 is set

(p,q) . c is set

p . (c + q) is set

rng c6 is finite set

rng x is finite set

((x | q),(p -' 1)) is Relation-like NAT -defined rng x -valued Function-like T-Sequence-like finite V86() set

rng x is finite set

((x | q),(p -' 1)) is Relation-like NAT -defined rng x -valued Function-like T-Sequence-like finite V86() set

(q + 1) - 1 is ext-real complex real integer rational Element of INT

rng x is finite set
((x | q),(p -' 1)) is Relation-like NAT -defined rng x -valued Function-like T-Sequence-like finite V86() set

(x,(p -' 1)) | ((q + 1) -' p) is Relation-like (q + 1) -' p -defined NAT -defined rng (x,(p -' 1)) -valued Function-like T-Sequence-like finite V86() set
rng (x,(p -' 1)) is finite set

(p + 1) - 1 is ext-real complex real integer rational Element of INT

(q + 1) - p is ext-real complex real Element of REAL
q - (p - 1) is ext-real complex real Element of REAL

(len x) - (p -' 1) is ext-real complex real integer rational Element of INT

(x,p,q) . c6 is set
((x,(p -' 1)) | ((q + 1) -' p)) . c6 is set

(q - (p - 1)) + (p -' 1) is ext-real complex real Element of REAL
c6 + (p - 1) is ext-real complex real Element of REAL
((x | q),(p -' 1)) . c6 is set
(x | q) . (c6 + (p -' 1)) is set
(x,(p -' 1)) . c6 is set
x . (c6 + (p -' 1)) is set

rng p is finite set

((p | x),(1 -' 1)) is Relation-like NAT -defined rng p -valued Function-like T-Sequence-like finite V86() set

rng p is finite set

((p | x),(1 -' 1)) is Relation-like NAT -defined rng p -valued Function-like T-Sequence-like finite V86() set

rng p is finite set