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
c5 is Relation-like Function-like set
dom c5 is set
e is set
c5 . 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
c5 is Relation-like Function-like set
dom c5 is set
e is Relation-like Function-like set
dom e is set
n is set
c5 . n is set
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
c5 is set
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
c5 is Relation-like X -defined the carrier of x -valued Function-like Element of K19(K20(X, the carrier of x))
(x,c5) is Relation-like REAL -valued Function-like set
K20(X,REAL) is set
K19(K20(X,REAL)) is set
dom (x,c5) is set
dom c5 is set
rng (x,c5) is set
e is set
n is set
(x,c5) . n is set
c5 /. n is Element of the carrier of x
(x,(c5 /. 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 . (c5 /. n) is complex Element of REAL
dom c5 is set
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
c5 /. n is Element of the carrier of x
(x,(c5 /. 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 . (c5 /. n) is complex Element of REAL
n is set
e . n is set
c5 /. n is Element of the carrier of x
(x,(c5 /. 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 . (c5 /. n) is complex Element of REAL
c is Element of X
c5 /. c is Element of the carrier of x
(x,(c5 /. c)) is complex Element of REAL
the of x . (c5 /. c) is complex Element of REAL
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
c5 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) Element of K19(K20(NAT,REAL))
dom c5 is set
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
c5 . e is complex Element of REAL
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
c5 . 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
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