REAL is non empty V40() V151() V152() V153() V157() set
NAT is V151() V152() V153() V154() V155() V156() V157() Element of K6(REAL)
K6(REAL) is set
COMPLEX is non empty V40() V151() V157() set
omega is V151() V152() V153() V154() V155() V156() V157() set
K6(omega) is set
K6(NAT) is set
1 is non empty natural V11() real ext-real positive non negative V38() V39() V151() V152() V153() V154() V155() V156() Element of NAT
RAT is non empty V40() V151() V152() V153() V154() V157() set
K7(1,1) is V19() V23( RAT ) V23( INT ) V141() V142() V143() V144() set
INT is non empty V40() V151() V152() V153() V154() V155() V157() set
K6(K7(1,1)) is set
K7(K7(1,1),1) is V19() V23( RAT ) V23( INT ) V141() V142() V143() V144() set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is V19() V141() V142() V143() set
K6(K7(K7(1,1),REAL)) is set
K7(REAL,REAL) is V19() V141() V142() V143() set
K7(K7(REAL,REAL),REAL) is V19() V141() V142() V143() set
K6(K7(K7(REAL,REAL),REAL)) is set
2 is non empty natural V11() real ext-real positive non negative V38() V39() V151() V152() V153() V154() V155() V156() Element of NAT
K7(2,2) is V19() V23( RAT ) V23( INT ) V141() V142() V143() V144() set
K7(K7(2,2),REAL) is V19() V141() V142() V143() set
K6(K7(K7(2,2),REAL)) is set
K6(K7(REAL,REAL)) is set
K384(2) is V175() L15()
the carrier of K384(2) is set
K442() is V187() TopStruct
the carrier of K442() is V151() V152() V153() set
K276() is V93() V187() L7()
K447() is non empty strict TopSpace-like V187() TopStruct
K449() is TopSpace-like V187() SubSpace of K447()
K427(K449(),K449()) is strict TopSpace-like TopStruct
the carrier of K427(K449(),K449()) is set
K7( the carrier of K384(2),REAL) is V19() V141() V142() V143() set
K6(K7( the carrier of K384(2),REAL)) is set
K6( the carrier of K384(2)) is set
{} is empty V19() non-empty empty-yielding V23( RAT ) Function-like one-to-one constant functional V141() V142() V143() V144() V151() V152() V153() V154() V155() V156() V157() set
{{},1} is non empty set
the carrier of K447() is non empty V151() V152() V153() set
0 is empty natural V11() real ext-real non positive non negative V19() non-empty empty-yielding V23( RAT ) Function-like one-to-one constant functional V38() V39() V141() V142() V143() V144() V151() V152() V153() V154() V155() V156() V157() Element of NAT
{0} is non empty functional V151() V152() V153() V154() V155() V156() set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K7( the carrier of T,REAL) is V19() V141() V142() V143() set
K6(K7( the carrier of T,REAL)) is set
R^1 is non empty strict TopSpace-like V187() V189() SubSpace of K447()
the carrier of R^1 is non empty V151() V152() V153() set
K7( the carrier of T, the carrier of R^1) is V19() V141() V142() V143() set
K6(K7( the carrier of T, the carrier of R^1)) is set
f is non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() continuous Element of K6(K7( the carrier of T,REAL))
g is non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() continuous Element of K6(K7( the carrier of T,REAL))
f + g is V19() V22( the carrier of T) V23( REAL ) Function-like V141() V142() V143() Element of K6(K7( the carrier of T,REAL))
G is non empty V19() V22( the carrier of T) V23( the carrier of R^1) Function-like V29( the carrier of T) V33( the carrier of T, the carrier of R^1) continuous V141() V142() V143() Element of K6(K7( the carrier of T, the carrier of R^1))
c is non empty V19() V22( the carrier of T) V23( the carrier of R^1) Function-like V29( the carrier of T) V33( the carrier of T, the carrier of R^1) continuous V141() V142() V143() Element of K6(K7( the carrier of T, the carrier of R^1))
H is non empty V19() V22( the carrier of T) V23( the carrier of R^1) Function-like V29( the carrier of T) V33( the carrier of T, the carrier of R^1) V141() V142() V143() Element of K6(K7( the carrier of T, the carrier of R^1))
h is non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() Element of K6(K7( the carrier of T,REAL))
dom h is non empty Element of K6( the carrier of T)
K6( the carrier of T) is set
the carrier of T /\ the carrier of T is set
dom g is non empty Element of K6( the carrier of T)
the carrier of T /\ (dom g) is Element of K6( the carrier of T)
dom f is non empty Element of K6( the carrier of T)
(dom f) /\ (dom g) is Element of K6( the carrier of T)
c is set
h . c is V11() real ext-real set
f . c is V11() real ext-real set
g . c is V11() real ext-real set
(f . c) + (g . c) is V11() real ext-real set
c is non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() Element of K6(K7( the carrier of T,REAL))
f - g is V19() V22( the carrier of T) V23( REAL ) Function-like V141() V142() V143() Element of K6(K7( the carrier of T,REAL))
G is non empty V19() V22( the carrier of T) V23( the carrier of R^1) Function-like V29( the carrier of T) V33( the carrier of T, the carrier of R^1) continuous V141() V142() V143() Element of K6(K7( the carrier of T, the carrier of R^1))
c is non empty V19() V22( the carrier of T) V23( the carrier of R^1) Function-like V29( the carrier of T) V33( the carrier of T, the carrier of R^1) continuous V141() V142() V143() Element of K6(K7( the carrier of T, the carrier of R^1))
H is non empty V19() V22( the carrier of T) V23( the carrier of R^1) Function-like V29( the carrier of T) V33( the carrier of T, the carrier of R^1) V141() V142() V143() Element of K6(K7( the carrier of T, the carrier of R^1))
h is non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() Element of K6(K7( the carrier of T,REAL))
dom h is non empty Element of K6( the carrier of T)
K6( the carrier of T) is set
the carrier of T /\ the carrier of T is set
dom g is non empty Element of K6( the carrier of T)
the carrier of T /\ (dom g) is Element of K6( the carrier of T)
dom f is non empty Element of K6( the carrier of T)
(dom f) /\ (dom g) is Element of K6( the carrier of T)
dom (f - g) is Element of K6( the carrier of T)
c is set
h . c is V11() real ext-real set
f . c is V11() real ext-real set
g . c is V11() real ext-real set
(f . c) - (g . c) is V11() real ext-real set
c is non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() Element of K6(K7( the carrier of T,REAL))
f (#) g is V19() V22( the carrier of T) V23( REAL ) Function-like V141() V142() V143() Element of K6(K7( the carrier of T,REAL))
G is non empty V19() V22( the carrier of T) V23( the carrier of R^1) Function-like V29( the carrier of T) V33( the carrier of T, the carrier of R^1) continuous V141() V142() V143() Element of K6(K7( the carrier of T, the carrier of R^1))
c is non empty V19() V22( the carrier of T) V23( the carrier of R^1) Function-like V29( the carrier of T) V33( the carrier of T, the carrier of R^1) continuous V141() V142() V143() Element of K6(K7( the carrier of T, the carrier of R^1))
H is non empty V19() V22( the carrier of T) V23( the carrier of R^1) Function-like V29( the carrier of T) V33( the carrier of T, the carrier of R^1) V141() V142() V143() Element of K6(K7( the carrier of T, the carrier of R^1))
h is non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() Element of K6(K7( the carrier of T,REAL))
dom h is non empty Element of K6( the carrier of T)
K6( the carrier of T) is set
the carrier of T /\ the carrier of T is set
dom g is non empty Element of K6( the carrier of T)
the carrier of T /\ (dom g) is Element of K6( the carrier of T)
dom f is non empty Element of K6( the carrier of T)
(dom f) /\ (dom g) is Element of K6( the carrier of T)
c is set
h . c is V11() real ext-real set
f . c is V11() real ext-real set
g . c is V11() real ext-real set
(f . c) * (g . c) is V11() real ext-real set
c is non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() Element of K6(K7( the carrier of T,REAL))
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K7( the carrier of T,REAL) is V19() V141() V142() V143() set
K6(K7( the carrier of T,REAL)) is set
f is non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() continuous Element of K6(K7( the carrier of T,REAL))
- f is V19() V22( the carrier of T) V23( REAL ) Function-like V141() V142() V143() Element of K6(K7( the carrier of T,REAL))
K7( the carrier of T, the carrier of R^1) is V19() V141() V142() V143() set
K6(K7( the carrier of T, the carrier of R^1)) is set
g is non empty V19() V22( the carrier of T) V23( the carrier of R^1) Function-like V29( the carrier of T) V33( the carrier of T, the carrier of R^1) continuous V141() V142() V143() Element of K6(K7( the carrier of T, the carrier of R^1))
G is non empty V19() V22( the carrier of T) V23( the carrier of R^1) Function-like V29( the carrier of T) V33( the carrier of T, the carrier of R^1) V141() V142() V143() Element of K6(K7( the carrier of T, the carrier of R^1))
c is non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() Element of K6(K7( the carrier of T,REAL))
dom c is non empty Element of K6( the carrier of T)
K6( the carrier of T) is set
dom f is non empty Element of K6( the carrier of T)
H is set
c . H is V11() real ext-real set
f . H is V11() real ext-real set
- (f . H) is V11() real ext-real set
H is non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() Element of K6(K7( the carrier of T,REAL))
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K7( the carrier of T,REAL) is V19() V141() V142() V143() set
K6(K7( the carrier of T,REAL)) is set
f is non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() continuous Element of K6(K7( the carrier of T,REAL))
abs f is V19() V22( the carrier of T) V23( REAL ) Function-like V141() V142() V143() nonnegative-yielding Element of K6(K7( the carrier of T,REAL))
K7( the carrier of T, the carrier of R^1) is V19() V141() V142() V143() set
K6(K7( the carrier of T, the carrier of R^1)) is set
g is non empty V19() V22( the carrier of T) V23( the carrier of R^1) Function-like V29( the carrier of T) V33( the carrier of T, the carrier of R^1) continuous V141() V142() V143() Element of K6(K7( the carrier of T, the carrier of R^1))
G is non empty V19() V22( the carrier of T) V23( the carrier of R^1) Function-like V29( the carrier of T) V33( the carrier of T, the carrier of R^1) V141() V142() V143() Element of K6(K7( the carrier of T, the carrier of R^1))
c is non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() Element of K6(K7( the carrier of T,REAL))
dom c is non empty Element of K6( the carrier of T)
K6( the carrier of T) is set
dom f is non empty Element of K6( the carrier of T)
H is set
c . H is V11() real ext-real set
f . H is V11() real ext-real set
abs (f . H) is V11() real ext-real Element of REAL
H is non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() Element of K6(K7( the carrier of T,REAL))
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
f is V11() real ext-real Element of REAL
the carrier of T --> f is non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() Element of K6(K7( the carrier of T,REAL))
K7( the carrier of T,REAL) is V19() V141() V142() V143() set
K6(K7( the carrier of T,REAL)) is set
G is V151() V152() V153() Element of K6(REAL)
( the carrier of T --> f) " G is Element of K6( the carrier of T)
K6( the carrier of T) is set
dom ( the carrier of T --> f) is non empty Element of K6( the carrier of T)
rng ( the carrier of T --> f) is non empty V151() V152() V153() Element of K6(REAL)
{f} is non empty V151() V152() V153() set
(rng ( the carrier of T --> f)) /\ G is V151() V152() V153() Element of K6(REAL)
( the carrier of T --> f) " ((rng ( the carrier of T --> f)) /\ G) is Element of K6( the carrier of T)
( the carrier of T --> f) " (rng ( the carrier of T --> f)) is Element of K6( the carrier of T)
[#] T is non empty non proper closed Element of K6( the carrier of T)
(rng ( the carrier of T --> f)) /\ G is V151() V152() V153() Element of K6(REAL)
( the carrier of T --> f) " ((rng ( the carrier of T --> f)) /\ G) is Element of K6( the carrier of T)
( the carrier of T --> f) " {} is empty V19() non-empty empty-yielding V23( RAT ) Function-like one-to-one constant functional closed V141() V142() V143() V144() V151() V152() V153() V154() V155() V156() V157() Element of K6( the carrier of T)
{} T is empty V19() non-empty empty-yielding V23( RAT ) Function-like one-to-one constant functional closed V141() V142() V143() V144() V151() V152() V153() V154() V155() V156() V157() Element of K6( the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K7( the carrier of T,REAL) is V19() V141() V142() V143() set
K6(K7( the carrier of T,REAL)) is set
the carrier of T --> 1 is non empty V19() non-empty V22( the carrier of T) V23( REAL ) V23( RAT ) V23( INT ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() V144() positive-yielding nonnegative-yielding Element of K6(K7( the carrier of T,REAL))
f is non empty V19() non-empty V22( the carrier of T) V23( REAL ) V23( RAT ) V23( INT ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() V144() positive-yielding nonnegative-yielding Element of K6(K7( the carrier of T,REAL))
- 1 is non empty V11() real ext-real non positive negative Element of REAL
the carrier of T --> (- 1) is non empty V19() non-empty V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() negative-yielding nonpositive-yielding Element of K6(K7( the carrier of T,REAL))
f is non empty V19() non-empty V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() negative-yielding nonpositive-yielding Element of K6(K7( the carrier of T,REAL))
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K7( the carrier of T,REAL) is V19() V141() V142() V143() set
K6(K7( the carrier of T,REAL)) is set
f is non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() continuous nonnegative-yielding Element of K6(K7( the carrier of T,REAL))
sqrt f is non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() nonnegative-yielding Element of K6(K7( the carrier of T,REAL))
K7( the carrier of T, the carrier of R^1) is V19() V141() V142() V143() set
K6(K7( the carrier of T, the carrier of R^1)) is set
G is Element of the carrier of T
f . G is V11() real ext-real set
dom f is non empty Element of K6( the carrier of T)
K6( the carrier of T) is set
rng f is non empty V151() V152() V153() Element of K6(REAL)
g is non empty V19() V22( the carrier of T) V23( the carrier of R^1) Function-like V29( the carrier of T) V33( the carrier of T, the carrier of R^1) continuous V141() V142() V143() Element of K6(K7( the carrier of T, the carrier of R^1))
G is non empty V19() V22( the carrier of T) V23( the carrier of R^1) Function-like V29( the carrier of T) V33( the carrier of T, the carrier of R^1) V141() V142() V143() Element of K6(K7( the carrier of T, the carrier of R^1))
c is non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() Element of K6(K7( the carrier of T,REAL))
dom c is non empty Element of K6( the carrier of T)
K6( the carrier of T) is set
dom f is non empty Element of K6( the carrier of T)
H is set
c . H is V11() real ext-real set
f . H is V11() real ext-real set
sqrt (f . H) is V11() real ext-real set
H is non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() Element of K6(K7( the carrier of T,REAL))
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K7( the carrier of T,REAL) is V19() V141() V142() V143() set
K6(K7( the carrier of T,REAL)) is set
f is non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() continuous Element of K6(K7( the carrier of T,REAL))
g is V11() real ext-real set
g (#) f is V19() V22( the carrier of T) V23( REAL ) Function-like V141() V142() V143() Element of K6(K7( the carrier of T,REAL))
K7( the carrier of T, the carrier of R^1) is V19() V141() V142() V143() set
K6(K7( the carrier of T, the carrier of R^1)) is set
F is non empty V19() V22( the carrier of T) V23( the carrier of R^1) Function-like V29( the carrier of T) V33( the carrier of T, the carrier of R^1) continuous V141() V142() V143() Element of K6(K7( the carrier of T, the carrier of R^1))
c is non empty V19() V22( the carrier of T) V23( the carrier of R^1) Function-like V29( the carrier of T) V33( the carrier of T, the carrier of R^1) V141() V142() V143() Element of K6(K7( the carrier of T, the carrier of R^1))
H is non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() Element of K6(K7( the carrier of T,REAL))
dom H is non empty Element of K6( the carrier of T)
K6( the carrier of T) is set
dom f is non empty Element of K6( the carrier of T)
h is set
H . h is V11() real ext-real set
f . h is V11() real ext-real set
g * (f . h) is V11() real ext-real set
h is non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() Element of K6(K7( the carrier of T,REAL))
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K7( the carrier of T,REAL) is V19() V141() V142() V143() set
K6(K7( the carrier of T,REAL)) is set
f is non empty V19() non-empty V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() continuous Element of K6(K7( the carrier of T,REAL))
f ^ is non empty V19() non-empty V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() Element of K6(K7( the carrier of T,REAL))
K7( the carrier of T, the carrier of R^1) is V19() V141() V142() V143() set
K6(K7( the carrier of T, the carrier of R^1)) is set
G is Element of the carrier of T
f . G is V11() real ext-real set
dom f is non empty Element of K6( the carrier of T)
K6( the carrier of T) is set
g is non empty V19() V22( the carrier of T) V23( the carrier of R^1) Function-like V29( the carrier of T) V33( the carrier of T, the carrier of R^1) continuous V141() V142() V143() Element of K6(K7( the carrier of T, the carrier of R^1))
G is non empty V19() V22( the carrier of T) V23( the carrier of R^1) Function-like V29( the carrier of T) V33( the carrier of T, the carrier of R^1) V141() V142() V143() Element of K6(K7( the carrier of T, the carrier of R^1))
H is set
c is non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() Element of K6(K7( the carrier of T,REAL))
dom c is non empty Element of K6( the carrier of T)
K6( the carrier of T) is set
c . H is V11() real ext-real set
f . H is V11() real ext-real set
1 / (f . H) is V11() real ext-real Element of REAL
(f . H) " is V11() real ext-real set
1 * ((f . H) ") is V11() real ext-real Element of REAL
dom f is non empty Element of K6( the carrier of T)
f " {0} is empty V19() non-empty empty-yielding V23( RAT ) Function-like one-to-one constant functional closed V141() V142() V143() V144() V151() V152() V153() V154() V155() V156() V157() Element of K6( the carrier of T)
(dom f) \ (f " {0}) is Element of K6( the carrier of T)
H is non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() Element of K6(K7( the carrier of T,REAL))
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K7( the carrier of T,REAL) is V19() V141() V142() V143() set
K6(K7( the carrier of T,REAL)) is set
f is non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() continuous Element of K6(K7( the carrier of T,REAL))
g is non empty V19() non-empty V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() continuous Element of K6(K7( the carrier of T,REAL))
f / g is non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() Element of K6(K7( the carrier of T,REAL))
K7( the carrier of T, the carrier of R^1) is V19() V141() V142() V143() set
K6(K7( the carrier of T, the carrier of R^1)) is set
H is Element of the carrier of T
g . H is V11() real ext-real set
dom g is non empty Element of K6( the carrier of T)
K6( the carrier of T) is set
F is non empty V19() V22( the carrier of T) V23( the carrier of R^1) Function-like V29( the carrier of T) V33( the carrier of T, the carrier of R^1) continuous V141() V142() V143() Element of K6(K7( the carrier of T, the carrier of R^1))
G is non empty V19() V22( the carrier of T) V23( the carrier of R^1) Function-like V29( the carrier of T) V33( the carrier of T, the carrier of R^1) continuous V141() V142() V143() Element of K6(K7( the carrier of T, the carrier of R^1))
H is non empty V19() V22( the carrier of T) V23( the carrier of R^1) Function-like V29( the carrier of T) V33( the carrier of T, the carrier of R^1) V141() V142() V143() Element of K6(K7( the carrier of T, the carrier of R^1))
c is set
h is non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() Element of K6(K7( the carrier of T,REAL))
dom h is non empty Element of K6( the carrier of T)
K6( the carrier of T) is set
h . c is V11() real ext-real set
f . c is V11() real ext-real set
g . c is V11() real ext-real set
(f . c) / (g . c) is V11() real ext-real set
(g . c) " is V11() real ext-real set
(f . c) * ((g . c) ") is V11() real ext-real set
the carrier of T /\ the carrier of T is set
dom g is non empty Element of K6( the carrier of T)
the carrier of T /\ (dom g) is Element of K6( the carrier of T)
dom f is non empty Element of K6( the carrier of T)
g " {0} is empty V19() non-empty empty-yielding V23( RAT ) Function-like one-to-one constant functional closed V141() V142() V143() V144() V151() V152() V153() V154() V155() V156() V157() Element of K6( the carrier of T)
(dom g) \ (g " {0}) is Element of K6( the carrier of T)
(dom f) /\ ((dom g) \ (g " {0})) is Element of K6( the carrier of T)
c is non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() Element of K6(K7( the carrier of T,REAL))