:: NORMSP_0 semantic presentation

REAL is non empty V28() set

K19(REAL) is set

NAT is non empty V21() V22() V23() Element of K19(REAL)

NAT is non empty V21() V22() V23() set

K19(NAT) is set

1 is non empty set

K20(1,1) is set

K19(K20(1,1)) is set

K20(K20(1,1),1) is set

K19(K20(K20(1,1),1)) is set

{} is Function-like functional empty V21() V22() V23() V25() V26() V27() complex set

{{}} is non empty set

op1 is Relation-like 1 -defined 1 -valued Function-like non empty total V18(1,1) Element of K19(K20(1,1))

{} .--> {} is Relation-like {{}} -defined Function-like one-to-one set

{{}} --> {} is Relation-like {{}} -defined {{}} -valued Function-like constant non empty total V18({{}},{{}}) Element of K19(K20({{}},{{}}))

K20({{}},{{}}) is set

K19(K20({{}},{{}})) is set

0 is Function-like functional empty V21() V22() V23() V25() V26() V27() complex Element of NAT

1 --> 0 is Relation-like 1 -defined NAT -valued Function-like constant non empty total V18(1, NAT ) Element of K19(K20(1,NAT))

K20(1,NAT) is set

K19(K20(1,NAT)) is set

{0} is non empty set

K20(1,{0}) is set

K20(1,REAL) is set

K19(K20(1,REAL)) is set

f is Relation-like 1 -defined REAL -valued Function-like non empty total V18(1, REAL ) Element of K19(K20(1,REAL))

(1,f) is () ()

X is non empty ()

the carrier of X is non empty set

the of X is Relation-like the carrier of X -defined REAL -valued Function-like non empty total V18( the carrier of X, REAL ) Element of K19(K20( the carrier of X,REAL))

K20( the carrier of X,REAL) is set

K19(K20( the carrier of X,REAL)) is set

x is Element of the carrier of X

the of X . x is complex Element of REAL

X is non empty ()

the carrier of X is non empty set

x is Relation-like the carrier of X -valued Function-like set

dom x is set

c

dom c

e is set

c

x /. e is Element of the carrier of X

(X,(x /. e)) is complex Element of REAL

the of X is Relation-like the carrier of X -defined REAL -valued Function-like non empty total V18( the carrier of X, REAL ) Element of K19(K20( the carrier of X,REAL))

K20( the carrier of X,REAL) is set

K19(K20( the carrier of X,REAL)) is set

the of X . (x /. e) is complex Element of REAL

c

dom c

e is Relation-like Function-like set

dom e is set

n is set

c

e . n is set

x /. n is Element of the carrier of X

(X,(x /. n)) is complex Element of REAL

the of X is Relation-like the carrier of X -defined REAL -valued Function-like non empty total V18( the carrier of X, REAL ) Element of K19(K20( the carrier of X,REAL))

K20( the carrier of X,REAL) is set

K19(K20( the carrier of X,REAL)) is set

the of X . (x /. n) is complex Element of REAL

X is non empty ()

the carrier of X is non empty set

x is Relation-like the carrier of X -valued Function-like set

(X,x) is Relation-like Function-like set

c

rng (X,x) is set

dom (X,x) is set

e is set

(X,x) . e is set

x /. e is Element of the carrier of X

(X,(x /. e)) is complex Element of REAL

the of X is Relation-like the carrier of X -defined REAL -valued Function-like non empty total V18( the carrier of X, REAL ) Element of K19(K20( the carrier of X,REAL))

K20( the carrier of X,REAL) is set

K19(K20( the carrier of X,REAL)) is set

the of X . (x /. e) is complex Element of REAL

X is non empty set

x is non empty ()

the carrier of x is non empty set

K20(X, the carrier of x) is set

K19(K20(X, the carrier of x)) is set

c

(x,c

K20(X,REAL) is set

K19(K20(X,REAL)) is set

dom (x,c

dom c

rng (x,c

e is set

n is set

(x,c

c

(x,(c

the of x is Relation-like the carrier of x -defined REAL -valued Function-like non empty total V18( the carrier of x, REAL ) Element of K19(K20( the carrier of x,REAL))

K20( the carrier of x,REAL) is set

K19(K20( the carrier of x,REAL)) is set

the of x . (c

dom c

e is Relation-like X -defined REAL -valued Function-like Element of K19(K20(X,REAL))

dom e is set

n is Element of X

e . n is set

c

(x,(c

the of x is Relation-like the carrier of x -defined REAL -valued Function-like non empty total V18( the carrier of x, REAL ) Element of K19(K20( the carrier of x,REAL))

K20( the carrier of x,REAL) is set

K19(K20( the carrier of x,REAL)) is set

the of x . (c

n is set

e . n is set

c

(x,(c

the of x is Relation-like the carrier of x -defined REAL -valued Function-like non empty total V18( the carrier of x, REAL ) Element of K19(K20( the carrier of x,REAL))

K20( the carrier of x,REAL) is set

K19(K20( the carrier of x,REAL)) is set

the of x . (c

c is Element of X

c

(x,(c

the of x . (c

X is non empty ()

the carrier of X is non empty set

K20(NAT, the carrier of X) is set

K19(K20(NAT, the carrier of X)) is set

x is Relation-like NAT -defined the carrier of X -valued Function-like non empty total V18( NAT , the carrier of X) Element of K19(K20(NAT, the carrier of X))

(X,x) is Relation-like REAL -valued Function-like set

K20(NAT,REAL) is set

K19(K20(NAT,REAL)) is set

(NAT,X,x) is Relation-like NAT -defined REAL -valued Function-like Element of K19(K20(NAT,REAL))

dom (NAT,X,x) is set

dom x is set

rng (NAT,X,x) is set

c

dom c

dom x is set

(NAT,X,x) is Relation-like NAT -defined REAL -valued Function-like Element of K19(K20(NAT,REAL))

e is V21() V22() V23() V27() complex Element of NAT

c

x . e is Element of the carrier of X

(X,(x . e)) is complex Element of REAL

the of X is Relation-like the carrier of X -defined REAL -valued Function-like non empty total V18( the carrier of X, REAL ) Element of K19(K20( the carrier of X,REAL))

K20( the carrier of X,REAL) is set

K19(K20( the carrier of X,REAL)) is set

the of X . (x . e) is complex Element of REAL

(NAT,X,x) . e is set

x /. e is Element of the carrier of X

(X,(x /. e)) is complex Element of REAL

the of X . (x /. e) is complex Element of REAL

e is set

c

x /. e is Element of the carrier of X

(X,(x /. e)) is complex Element of REAL

the of X is Relation-like the carrier of X -defined REAL -valued Function-like non empty total V18( the carrier of X, REAL ) Element of K19(K20( the carrier of X,REAL))

K20( the carrier of X,REAL) is set

K19(K20( the carrier of X,REAL)) is set

the of X . (x /. e) is complex Element of REAL

n is V21() V22() V23() V27() complex Element of NAT

x . n is Element of the carrier of X

(X,(x . n)) is complex Element of REAL

the of X . (x . n) is complex Element of REAL

z is Element of 1

f is Relation-like 1 -defined REAL -valued Function-like non empty total V18(1, REAL ) Element of K19(K20(1,REAL))

(1,z,f) is () ()

z is Element of 1

f is Relation-like 1 -defined REAL -valued Function-like non empty total V18(1, REAL ) Element of K19(K20(1,REAL))

(1,z,f) is () ()

X is non empty () ()

0. X is zero Element of the carrier of X

the carrier of X is non empty set

the ZeroF of X is Element of the carrier of X

(X,(0. X)) is complex Element of REAL

the of X is Relation-like the carrier of X -defined REAL -valued Function-like non empty total V18( the carrier of X, REAL ) Element of K19(K20( the carrier of X,REAL))

K20( the carrier of X,REAL) is set

K19(K20( the carrier of X,REAL)) is set

the of X . (0. X) is complex Element of REAL

x is Element of the carrier of X

(X,x) is complex Element of REAL

the of X . x is complex Element of REAL

X is non empty () ()

0. X is zero Element of the carrier of X

the carrier of X is non empty set

the ZeroF of X is Element of the carrier of X

(X,(0. X)) is complex Element of REAL

the of X is Relation-like the carrier of X -defined REAL -valued Function-like non empty total V18( the carrier of X, REAL ) Element of K19(K20( the carrier of X,REAL))

K20( the carrier of X,REAL) is set

K19(K20( the carrier of X,REAL)) is set

the of X . (0. X) is complex Element of REAL