:: PARTFUN4 semantic presentation

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