:: DIFF_1 semantic presentation

REAL is non empty V32() V57() V58() V59() V63() set

NAT is non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() Element of bool REAL

bool REAL is set

[:NAT,REAL:] is V13() complex-valued ext-real-valued real-valued set

bool [:NAT,REAL:] is set

COMPLEX is non empty V32() V57() V63() set

omega is non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() set

bool omega is set

bool NAT is set

RAT is non empty V32() V57() V58() V59() V60() V63() set

INT is non empty V32() V57() V58() V59() V60() V61() V63() set

ExtREAL is non empty V58() set

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V13() non-empty empty-yielding V17( RAT ) ext-real complex-valued ext-real-valued real-valued natural-valued V57() V58() V59() V60() V61() V62() V63() set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() Element of NAT

{{},1} is non empty V57() V58() V59() V60() V61() V62() set

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V13() non-empty empty-yielding V17( RAT ) V30() ext-real complex-valued ext-real-valued real-valued natural-valued V56() V57() V58() V59() V60() V61() V62() V63() Element of NAT

- 1 is V11() real ext-real Element of REAL

PFuncs (REAL,REAL) is non empty functional set

[:NAT,(PFuncs (REAL,REAL)):] is V13() set

bool [:NAT,(PFuncs (REAL,REAL)):] is set

[:REAL,REAL:] is V13() complex-valued ext-real-valued real-valued set

bool [:REAL,REAL:] is set

x is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

dom x is V57() V58() V59() Element of bool REAL

h is V11() real ext-real set

- h is V11() real ext-real set

(- h) ++ (dom x) is V57() V58() V59() Element of bool REAL

f2 is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

dom f2 is V57() V58() V59() Element of bool REAL

S is set

S is set

S is V11() real ext-real Element of REAL

f2 . S is V11() real ext-real Element of REAL

S + h is V11() real ext-real Element of REAL

x . (S + h) is V11() real ext-real Element of REAL

S is V11() real ext-real Element of REAL

f2 . S is V11() real ext-real Element of REAL

S + h is V11() real ext-real Element of REAL

x . (S + h) is V11() real ext-real Element of REAL

f is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

dom f is V57() V58() V59() Element of bool REAL

f2 is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

dom f2 is V57() V58() V59() Element of bool REAL

k is V11() real ext-real Element of REAL

f . k is V11() real ext-real Element of REAL

f2 . k is V11() real ext-real Element of REAL

k + h is V11() real ext-real Element of REAL

x . (k + h) is V11() real ext-real Element of REAL

x is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

h is V11() real ext-real set

(x,h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

dom (x,h) is V57() V58() V59() Element of bool REAL

dom x is non empty V57() V58() V59() Element of bool REAL

- h is V11() real ext-real set

(- h) ++ (dom x) is V57() V58() V59() Element of bool REAL

f is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

dom (x,h) is V57() V58() V59() Element of bool REAL

f2 is V11() real ext-real Element of REAL

dom x is non empty V57() V58() V59() Element of bool REAL

- h is V11() real ext-real set

(- h) ++ (dom x) is V57() V58() V59() Element of bool REAL

f . f2 is V11() real ext-real Element of REAL

f2 + h is V11() real ext-real Element of REAL

x . (f2 + h) is V11() real ext-real Element of REAL

dom f is non empty V57() V58() V59() Element of bool REAL

f2 is V11() real ext-real Element of REAL

f . f2 is V11() real ext-real Element of REAL

(x,h) . f2 is V11() real ext-real Element of REAL

f2 + h is V11() real ext-real Element of REAL

x . (f2 + h) is V11() real ext-real Element of REAL

f is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

f2 is V11() real ext-real Element of REAL

f . f2 is V11() real ext-real Element of REAL

f2 + h is V11() real ext-real Element of REAL

x . (f2 + h) is V11() real ext-real Element of REAL

S is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

x is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

h is V11() real ext-real set

(x,h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(x,h) - x is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- x is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

- 1 is V11() real ext-real set

(- 1) (#) x is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(x,h) + (- x) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

x is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

h is V11() real ext-real set

(x,h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(x,h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(x,h) - x is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- x is V13() V16( REAL ) Function-like total complex-valued ext-real-valued real-valued set

(- 1) (#) x is V13() V16( REAL ) Function-like total complex-valued ext-real-valued real-valued set

(x,h) + (- x) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

dom (x,h) is V57() V58() V59() Element of bool REAL

(x,h) is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

dom (x,h) is non empty V57() V58() V59() Element of bool REAL

dom x is non empty V57() V58() V59() Element of bool REAL

(dom (x,h)) /\ (dom x) is V57() V58() V59() Element of bool REAL

REAL /\ (dom x) is V57() V58() V59() Element of bool REAL

REAL /\ REAL is V57() V58() V59() set

x is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

h is V11() real ext-real set

- h is V11() real ext-real set

(x,(- h)) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

x - (x,(- h)) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- (x,(- h)) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(- 1) (#) (x,(- h)) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

x + (- (x,(- h))) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

x is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

h is V11() real ext-real set

(x,h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- h is V11() real ext-real set

(x,(- h)) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

x - (x,(- h)) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- (x,(- h)) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(- 1) (#) (x,(- h)) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

x + (- (x,(- h))) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

dom (x,h) is V57() V58() V59() Element of bool REAL

(x,(- h)) is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

dom (x,(- h)) is non empty V57() V58() V59() Element of bool REAL

dom x is non empty V57() V58() V59() Element of bool REAL

(dom (x,(- h))) /\ (dom x) is V57() V58() V59() Element of bool REAL

REAL /\ (dom x) is V57() V58() V59() Element of bool REAL

REAL /\ REAL is V57() V58() V59() set

x is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

h is V11() real ext-real set

2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() Element of NAT

h / 2 is V11() real ext-real Element of REAL

(x,(h / 2)) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- (h / 2) is V11() real ext-real Element of REAL

(x,(- (h / 2))) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(x,(h / 2)) - (x,(- (h / 2))) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- (x,(- (h / 2))) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(- 1) (#) (x,(- (h / 2))) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(x,(h / 2)) + (- (x,(- (h / 2)))) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

x is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

h is V11() real ext-real set

(x,h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

h / 2 is V11() real ext-real Element of REAL

(x,(h / 2)) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- (h / 2) is V11() real ext-real Element of REAL

(x,(- (h / 2))) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(x,(h / 2)) - (x,(- (h / 2))) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- (x,(- (h / 2))) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(- 1) (#) (x,(- (h / 2))) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(x,(h / 2)) + (- (x,(- (h / 2)))) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

dom (x,h) is V57() V58() V59() Element of bool REAL

(x,(h / 2)) is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

dom (x,(h / 2)) is non empty V57() V58() V59() Element of bool REAL

(x,(- (h / 2))) is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

dom (x,(- (h / 2))) is non empty V57() V58() V59() Element of bool REAL

(dom (x,(h / 2))) /\ (dom (x,(- (h / 2)))) is V57() V58() V59() Element of bool REAL

REAL /\ (dom (x,(- (h / 2)))) is V57() V58() V59() Element of bool REAL

REAL /\ REAL is V57() V58() V59() set

x is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

h is V11() real ext-real set

f2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() Element of NAT

S is Element of PFuncs (REAL,REAL)

k is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(k,h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(k,h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(k,h) - k is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- k is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(- 1) (#) k is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(k,h) + (- k) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

x is Element of PFuncs (REAL,REAL)

r2 is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(r2,h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(r2,h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(r2,h) - r2 is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- r2 is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(- 1) (#) r2 is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(r2,h) + (- r2) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

f is Element of PFuncs (REAL,REAL)

f2 is non empty V13() V16( NAT ) V17( PFuncs (REAL,REAL)) Function-like total quasi_total Element of bool [:NAT,(PFuncs (REAL,REAL)):]

f2 . 0 is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

S is non empty V13() V16( NAT ) V17( PFuncs (REAL,REAL)) Function-like total quasi_total Element of bool [:NAT,(PFuncs (REAL,REAL)):]

S . 0 is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set

k + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() Element of NAT

S . (k + 1) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

S . k is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

((S . k),h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

((S . k),h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

((S . k),h) - (S . k) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- (S . k) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(- 1) (#) (S . k) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

((S . k),h) + (- (S . k)) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

x is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(x,h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(x,h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(x,h) - x is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- x is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(- 1) (#) x is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(x,h) + (- x) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

f is non empty V13() V16( NAT ) V17( PFuncs (REAL,REAL)) Function-like total quasi_total Element of bool [:NAT,(PFuncs (REAL,REAL)):]

f . 0 is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

f2 is non empty V13() V16( NAT ) V17( PFuncs (REAL,REAL)) Function-like total quasi_total Element of bool [:NAT,(PFuncs (REAL,REAL)):]

f2 . 0 is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

S is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() Element of NAT

f . S is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

f2 . S is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

S + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() Element of NAT

f . (S + 1) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

f2 . (S + 1) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

((f . S),h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

((f . S),h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

((f . S),h) - (f . S) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- (f . S) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(- 1) (#) (f . S) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

((f . S),h) + (- (f . S)) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

x is V11() real ext-real Element of REAL

h is V11() real ext-real Element of REAL

x + h is V11() real ext-real Element of REAL

f is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

dom f is V57() V58() V59() Element of bool REAL

(f,h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(f,h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(f,h) - f is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- f is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(- 1) (#) f is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(f,h) + (- f) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(f,h) . x is V11() real ext-real Element of REAL

f . (x + h) is V11() real ext-real Element of REAL

f . x is V11() real ext-real Element of REAL

(f . (x + h)) - (f . x) is V11() real ext-real Element of REAL

dom (f,h) is V57() V58() V59() Element of bool REAL

- h is V11() real ext-real Element of REAL

(- h) ++ (dom f) is V57() V58() V59() Element of bool REAL

(- h) + (x + h) is V11() real ext-real Element of REAL

(f,h) . x is V11() real ext-real Element of REAL

(dom (f,h)) /\ (dom f) is V57() V58() V59() Element of bool REAL

dom (f,h) is V57() V58() V59() Element of bool REAL

x is V11() real ext-real Element of REAL

h is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(h,x) is non empty V13() V16( NAT ) V17( PFuncs (REAL,REAL)) Function-like total quasi_total Element of bool [:NAT,(PFuncs (REAL,REAL)):]

f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set

(h,x) . f is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

f + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() Element of NAT

(h,x) . (f + 1) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(((h,x) . f),x) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(((h,x) . f),x) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(((h,x) . f),x) - ((h,x) . f) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- ((h,x) . f) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(- 1) (#) ((h,x) . f) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(((h,x) . f),x) + (- ((h,x) . f)) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(h,x) . 0 is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set

(h,x) . f is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

x is V11() real ext-real Element of REAL

h is V11() real ext-real Element of REAL

h + x is V11() real ext-real Element of REAL

f is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(f,x) is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(f,x) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(f,x) - f is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- f is V13() V16( REAL ) Function-like total complex-valued ext-real-valued real-valued set

(- 1) (#) f is V13() V16( REAL ) Function-like total complex-valued ext-real-valued real-valued set

(f,x) + (- f) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(f,x) . h is V11() real ext-real Element of REAL

f . (h + x) is V11() real ext-real Element of REAL

f . h is V11() real ext-real Element of REAL

(f . (h + x)) - (f . h) is V11() real ext-real Element of REAL

(f,x) is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(f,x) - f is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(f,x) + (- f) is V13() V16( REAL ) Function-like total complex-valued ext-real-valued real-valued set

dom ((f,x) - f) is non empty V57() V58() V59() Element of bool REAL

(f,x) . h is V11() real ext-real Element of REAL

((f,x) . h) - (f . h) is V11() real ext-real Element of REAL

x is V11() real ext-real Element of REAL

h is V11() real ext-real Element of REAL

h - x is V11() real ext-real Element of REAL

f is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(f,x) is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- x is V11() real ext-real set

(f,(- x)) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

f - (f,(- x)) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- (f,(- x)) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(- 1) (#) (f,(- x)) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

f + (- (f,(- x))) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(f,x) . h is V11() real ext-real Element of REAL

f . h is V11() real ext-real Element of REAL

f . (h - x) is V11() real ext-real Element of REAL

(f . h) - (f . (h - x)) is V11() real ext-real Element of REAL

- x is V11() real ext-real Element of REAL

(f,(- x)) is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(f,(- x)) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(f,(- x)) - f is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- f is V13() V16( REAL ) Function-like total complex-valued ext-real-valued real-valued set

(- 1) (#) f is V13() V16( REAL ) Function-like total complex-valued ext-real-valued real-valued set

(f,(- x)) + (- f) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

- (f,(- x)) is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(- 1) (#) (f,(- x)) is V13() V16( REAL ) Function-like total complex-valued ext-real-valued real-valued set

(- (f,(- x))) . h is V11() real ext-real Element of REAL

(f,(- x)) . h is V11() real ext-real Element of REAL

- ((f,(- x)) . h) is V11() real ext-real Element of REAL

h + (- x) is V11() real ext-real Element of REAL

f . (h + (- x)) is V11() real ext-real Element of REAL

(f . (h + (- x))) - (f . h) is V11() real ext-real Element of REAL

- ((f . (h + (- x))) - (f . h)) is V11() real ext-real Element of REAL

x is V11() real ext-real Element of REAL

x / 2 is V11() real ext-real Element of REAL

h is V11() real ext-real Element of REAL

h + (x / 2) is V11() real ext-real Element of REAL

h - (x / 2) is V11() real ext-real Element of REAL

f is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(f,x) is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

x / 2 is V11() real ext-real Element of REAL

(f,(x / 2)) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- (x / 2) is V11() real ext-real Element of REAL

(f,(- (x / 2))) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(f,(x / 2)) - (f,(- (x / 2))) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- (f,(- (x / 2))) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(- 1) (#) (f,(- (x / 2))) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(f,(x / 2)) + (- (f,(- (x / 2)))) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(f,x) . h is V11() real ext-real Element of REAL

f . (h + (x / 2)) is V11() real ext-real Element of REAL

f . (h - (x / 2)) is V11() real ext-real Element of REAL

(f . (h + (x / 2))) - (f . (h - (x / 2))) is V11() real ext-real Element of REAL

(f,(x / 2)) is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- (x / 2) is V11() real ext-real Element of REAL

(f,(- (x / 2))) is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(f,(x / 2)) - (f,(- (x / 2))) is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- (f,(- (x / 2))) is V13() V16( REAL ) Function-like total complex-valued ext-real-valued real-valued set

(- 1) (#) (f,(- (x / 2))) is V13() V16( REAL ) Function-like total complex-valued ext-real-valued real-valued set

(f,(x / 2)) + (- (f,(- (x / 2)))) is V13() V16( REAL ) Function-like total complex-valued ext-real-valued real-valued set

dom ((f,(x / 2)) - (f,(- (x / 2)))) is non empty V57() V58() V59() Element of bool REAL

(f,(x / 2)) . h is V11() real ext-real Element of REAL

(f,(- (x / 2))) . h is V11() real ext-real Element of REAL

((f,(x / 2)) . h) - ((f,(- (x / 2))) . h) is V11() real ext-real Element of REAL

(f . (h + (x / 2))) - ((f,(- (x / 2))) . h) is V11() real ext-real Element of REAL

h + (- (x / 2)) is V11() real ext-real Element of REAL

f . (h + (- (x / 2))) is V11() real ext-real Element of REAL

(f . (h + (x / 2))) - (f . (h + (- (x / 2)))) is V11() real ext-real Element of REAL

x is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() Element of NAT

x + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() Element of NAT

h is V11() real ext-real Element of REAL

f is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(f,h) is non empty V13() V16( NAT ) V17( PFuncs (REAL,REAL)) Function-like total quasi_total Element of bool [:NAT,(PFuncs (REAL,REAL)):]

(f,h) . (x + 1) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

f2 is V11() real ext-real Element of REAL

f2 + h is V11() real ext-real Element of REAL

f . (f2 + h) is V11() real ext-real Element of REAL

f . f2 is V11() real ext-real Element of REAL

(f . (f2 + h)) - (f . f2) is V11() real ext-real Element of REAL

dom f is non empty V57() V58() V59() Element of bool REAL

f2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() Element of NAT

f2 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() Element of NAT

(f,h) . (f2 + 1) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(f2 + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() Element of NAT

(f,h) . ((f2 + 1) + 1) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

S is V11() real ext-real Element of REAL

((f,h) . ((f2 + 1) + 1)) . S is V11() real ext-real Element of REAL

S + h is V11() real ext-real Element of REAL

((f,h) . (f2 + 1)) . (S + h) is V11() real ext-real Element of REAL

f2 + 2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() Element of NAT

(f,h) . (f2 + 2) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

((f,h) . (f2 + 2)) . S is V11() real ext-real Element of REAL

(((f,h) . (f2 + 1)),h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(((f,h) . (f2 + 1)),h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(((f,h) . (f2 + 1)),h) - ((f,h) . (f2 + 1)) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- ((f,h) . (f2 + 1)) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(- 1) (#) ((f,h) . (f2 + 1)) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(((f,h) . (f2 + 1)),h) + (- ((f,h) . (f2 + 1))) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(((f,h) . (f2 + 1)),h) . S is V11() real ext-real Element of REAL

((f,h) . (f2 + 1)) . S is V11() real ext-real Element of REAL

(((f,h) . (f2 + 1)) . (S + h)) - (((f,h) . (f2 + 1)) . S) is V11() real ext-real Element of REAL

0 - 0 is V11() real ext-real Element of REAL

0 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() Element of NAT

(f,h) . (0 + 1) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

f2 is V11() real ext-real Element of REAL

((f,h) . (0 + 1)) . f2 is V11() real ext-real Element of REAL

(f,h) . 0 is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(((f,h) . 0),h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(((f,h) . 0),h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(((f,h) . 0),h) - ((f,h) . 0) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- ((f,h) . 0) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(- 1) (#) ((f,h) . 0) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(((f,h) . 0),h) + (- ((f,h) . 0)) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(((f,h) . 0),h) . f2 is V11() real ext-real Element of REAL

(f,h) is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(f,h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(f,h) - f is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- f is V13() V16( REAL ) Function-like total complex-valued ext-real-valued real-valued set

(- 1) (#) f is V13() V16( REAL ) Function-like total complex-valued ext-real-valued real-valued set

(f,h) + (- f) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(f,h) . f2 is V11() real ext-real Element of REAL

f2 + h is V11() real ext-real Element of REAL

f . (f2 + h) is V11() real ext-real Element of REAL

f . f2 is V11() real ext-real Element of REAL

(f . (f2 + h)) - (f . f2) is V11() real ext-real Element of REAL

f2 is V11() real ext-real Element of REAL

((f,h) . (x + 1)) . f2 is V11() real ext-real Element of REAL

f2 is V11() real ext-real Element of REAL

((f,h) . (x + 1)) . f2 is V11() real ext-real Element of REAL

x is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() Element of NAT

x + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() Element of NAT

h is V11() real ext-real Element of REAL

f is V11() real ext-real Element of REAL

f2 is V11() real ext-real Element of REAL

S is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

h (#) S is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

((h (#) S),f) is non empty V13() V16( NAT ) V17( PFuncs (REAL,REAL)) Function-like total quasi_total Element of bool [:NAT,(PFuncs (REAL,REAL)):]

((h (#) S),f) . (x + 1) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(((h (#) S),f) . (x + 1)) . f2 is V11() real ext-real Element of REAL

(S,f) is non empty V13() V16( NAT ) V17( PFuncs (REAL,REAL)) Function-like total quasi_total Element of bool [:NAT,(PFuncs (REAL,REAL)):]

(S,f) . (x + 1) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

((S,f) . (x + 1)) . f2 is V11() real ext-real Element of REAL

h * (((S,f) . (x + 1)) . f2) is V11() real ext-real Element of REAL

k is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() Element of NAT

k + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() Element of NAT

((h (#) S),f) . (k + 1) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(S,f) . (k + 1) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(k + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() Element of NAT

((h (#) S),f) . ((k + 1) + 1) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(S,f) . ((k + 1) + 1) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

x is V11() real ext-real Element of REAL

(((h (#) S),f) . ((k + 1) + 1)) . x is V11() real ext-real Element of REAL

((S,f) . ((k + 1) + 1)) . x is V11() real ext-real Element of REAL

h * (((S,f) . ((k + 1) + 1)) . x) is V11() real ext-real Element of REAL

(((h (#) S),f) . (k + 1)) . x is V11() real ext-real Element of REAL

((S,f) . (k + 1)) . x is V11() real ext-real Element of REAL

h * (((S,f) . (k + 1)) . x) is V11() real ext-real Element of REAL

x + f is V11() real ext-real Element of REAL

(((h (#) S),f) . (k + 1)) . (x + f) is V11() real ext-real Element of REAL

((S,f) . (k + 1)) . (x + f) is V11() real ext-real Element of REAL

h * (((S,f) . (k + 1)) . (x + f)) is V11() real ext-real Element of REAL

((((h (#) S),f) . (k + 1)),f) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

((((h (#) S),f) . (k + 1)),f) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

((((h (#) S),f) . (k + 1)),f) - (((h (#) S),f) . (k + 1)) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- (((h (#) S),f) . (k + 1)) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(- 1) (#) (((h (#) S),f) . (k + 1)) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

((((h (#) S),f) . (k + 1)),f) + (- (((h (#) S),f) . (k + 1))) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

((((h (#) S),f) . (k + 1)),f) . x is V11() real ext-real Element of REAL

(h * (((S,f) . (k + 1)) . (x + f))) - (h * (((S,f) . (k + 1)) . x)) is V11() real ext-real Element of REAL

(((S,f) . (k + 1)) . (x + f)) - (((S,f) . (k + 1)) . x) is V11() real ext-real Element of REAL

h * ((((S,f) . (k + 1)) . (x + f)) - (((S,f) . (k + 1)) . x)) is V11() real ext-real Element of REAL

(((S,f) . (k + 1)),f) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(((S,f) . (k + 1)),f) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(((S,f) . (k + 1)),f) - ((S,f) . (k + 1)) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- ((S,f) . (k + 1)) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(- 1) (#) ((S,f) . (k + 1)) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(((S,f) . (k + 1)),f) + (- ((S,f) . (k + 1))) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(((S,f) . (k + 1)),f) . x is V11() real ext-real Element of REAL

h * ((((S,f) . (k + 1)),f) . x) is V11() real ext-real Element of REAL

0 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() Element of NAT

((h (#) S),f) . (0 + 1) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(S,f) . (0 + 1) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

k is V11() real ext-real Element of REAL

(((h (#) S),f) . (0 + 1)) . k is V11() real ext-real Element of REAL

((S,f) . (0 + 1)) . k is V11() real ext-real Element of REAL

h * (((S,f) . (0 + 1)) . k) is V11() real ext-real Element of REAL

dom (h (#) S) is non empty V57() V58() V59() Element of bool REAL

k + f is V11() real ext-real Element of REAL

((h (#) S),f) . 0 is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

((((h (#) S),f) . 0),f) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

((((h (#) S),f) . 0),f) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

((((h (#) S),f) . 0),f) - (((h (#) S),f) . 0) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- (((h (#) S),f) . 0) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(- 1) (#) (((h (#) S),f) . 0) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

((((h (#) S),f) . 0),f) + (- (((h (#) S),f) . 0)) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

((((h (#) S),f) . 0),f) . k is V11() real ext-real Element of REAL

((h (#) S),f) is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

((h (#) S),f) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

((h (#) S),f) - (h (#) S) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- (h (#) S) is V13() V16( REAL ) Function-like total complex-valued ext-real-valued real-valued set

(- 1) (#) (h (#) S) is V13() V16( REAL ) Function-like total complex-valued ext-real-valued real-valued set

((h (#) S),f) + (- (h (#) S)) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

((h (#) S),f) . k is V11() real ext-real Element of REAL

(h (#) S) . (k + f) is V11() real ext-real Element of REAL

(h (#) S) . k is V11() real ext-real Element of REAL

((h (#) S) . (k + f)) - ((h (#) S) . k) is V11() real ext-real Element of REAL

S . (k + f) is V11() real ext-real Element of REAL

h * (S . (k + f)) is V11() real ext-real Element of REAL

(h * (S . (k + f))) - ((h (#) S) . k) is V11() real ext-real Element of REAL

S . k is V11() real ext-real Element of REAL

h * (S . k) is V11() real ext-real Element of REAL

(h * (S . (k + f))) - (h * (S . k)) is V11() real ext-real Element of REAL

(S . (k + f)) - (S . k) is V11() real ext-real Element of REAL

h * ((S . (k + f)) - (S . k)) is V11() real ext-real Element of REAL

(S,f) is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(S,f) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(S,f) - S is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- S is V13() V16( REAL ) Function-like total complex-valued ext-real-valued real-valued set

(- 1) (#) S is V13() V16( REAL ) Function-like total complex-valued ext-real-valued real-valued set

(S,f) + (- S) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(S,f) . k is V11() real ext-real Element of REAL

h * ((S,f) . k) is V11() real ext-real Element of REAL

(S,f) . 0 is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(((S,f) . 0),f) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(((S,f) . 0),f) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(((S,f) . 0),f) - ((S,f) . 0) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- ((S,f) . 0) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(- 1) (#) ((S,f) . 0) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(((S,f) . 0),f) + (- ((S,f) . 0)) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(((S,f) . 0),f) . k is V11() real ext-real Element of REAL

h * ((((S,f) . 0),f) . k) is V11() real ext-real Element of REAL

x is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() Element of NAT

x + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() Element of NAT

h is V11() real ext-real Element of REAL

f is V11() real ext-real Element of REAL

f2 is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(f2,h) is non empty V13() V16( NAT ) V17( PFuncs (REAL,REAL)) Function-like total quasi_total Element of bool [:NAT,(PFuncs (REAL,REAL)):]

(f2,h) . (x + 1) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

((f2,h) . (x + 1)) . f is V11() real ext-real Element of REAL

S is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

f2 + S is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

((f2 + S),h) is non empty V13() V16( NAT ) V17( PFuncs (REAL,REAL)) Function-like total quasi_total Element of bool [:NAT,(PFuncs (REAL,REAL)):]

((f2 + S),h) . (x + 1) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(((f2 + S),h) . (x + 1)) . f is V11() real ext-real Element of REAL

(S,h) is non empty V13() V16( NAT ) V17( PFuncs (REAL,REAL)) Function-like total quasi_total Element of bool [:NAT,(PFuncs (REAL,REAL)):]

(S,h) . (x + 1) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

((S,h) . (x + 1)) . f is V11() real ext-real Element of REAL

(((f2,h) . (x + 1)) . f) + (((S,h) . (x + 1)) . f) is V11() real ext-real Element of REAL

k is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() Element of NAT

k + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() Element of NAT

((f2 + S),h) . (k + 1) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(f2,h) . (k + 1) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(S,h) . (k + 1) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(k + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() Element of NAT

((f2 + S),h) . ((k + 1) + 1) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(f2,h) . ((k + 1) + 1) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(S,h) . ((k + 1) + 1) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

x is V11() real ext-real Element of REAL

(((f2 + S),h) . ((k + 1) + 1)) . x is V11() real ext-real Element of REAL

((f2,h) . ((k + 1) + 1)) . x is V11() real ext-real Element of REAL

((S,h) . ((k + 1) + 1)) . x is V11() real ext-real Element of REAL

(((f2,h) . ((k + 1) + 1)) . x) + (((S,h) . ((k + 1) + 1)) . x) is V11() real ext-real Element of REAL

(((f2 + S),h) . (k + 1)) . x is V11() real ext-real Element of REAL

((f2,h) . (k + 1)) . x is V11() real ext-real Element of REAL

((S,h) . (k + 1)) . x is V11() real ext-real Element of REAL

(((f2,h) . (k + 1)) . x) + (((S,h) . (k + 1)) . x) is V11() real ext-real Element of REAL

x + h is V11() real ext-real Element of REAL

(((f2 + S),h) . (k + 1)) . (x + h) is V11() real ext-real Element of REAL

((f2,h) . (k + 1)) . (x + h) is V11() real ext-real Element of REAL

((S,h) . (k + 1)) . (x + h) is V11() real ext-real Element of REAL

(((f2,h) . (k + 1)) . (x + h)) + (((S,h) . (k + 1)) . (x + h)) is V11() real ext-real Element of REAL

((((f2 + S),h) . (k + 1)),h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

((((f2 + S),h) . (k + 1)),h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

((((f2 + S),h) . (k + 1)),h) - (((f2 + S),h) . (k + 1)) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- (((f2 + S),h) . (k + 1)) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(- 1) (#) (((f2 + S),h) . (k + 1)) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

((((f2 + S),h) . (k + 1)),h) + (- (((f2 + S),h) . (k + 1))) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

((((f2 + S),h) . (k + 1)),h) . x is V11() real ext-real Element of REAL

((((f2 + S),h) . (k + 1)) . (x + h)) - ((((f2 + S),h) . (k + 1)) . x) is V11() real ext-real Element of REAL

(((f2,h) . (k + 1)) . (x + h)) - (((f2,h) . (k + 1)) . x) is V11() real ext-real Element of REAL

(((S,h) . (k + 1)) . (x + h)) - (((S,h) . (k + 1)) . x) is V11() real ext-real Element of REAL

((((f2,h) . (k + 1)) . (x + h)) - (((f2,h) . (k + 1)) . x)) + ((((S,h) . (k + 1)) . (x + h)) - (((S,h) . (k + 1)) . x)) is V11() real ext-real Element of REAL

(((f2,h) . (k + 1)),h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(((f2,h) . (k + 1)),h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(((f2,h) . (k + 1)),h) - ((f2,h) . (k + 1)) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- ((f2,h) . (k + 1)) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(- 1) (#) ((f2,h) . (k + 1)) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(((f2,h) . (k + 1)),h) + (- ((f2,h) . (k + 1))) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(((f2,h) . (k + 1)),h) . x is V11() real ext-real Element of REAL

((((f2,h) . (k + 1)),h) . x) + ((((S,h) . (k + 1)) . (x + h)) - (((S,h) . (k + 1)) . x)) is V11() real ext-real Element of REAL

(((S,h) . (k + 1)),h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(((S,h) . (k + 1)),h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(((S,h) . (k + 1)),h) - ((S,h) . (k + 1)) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- ((S,h) . (k + 1)) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(- 1) (#) ((S,h) . (k + 1)) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(((S,h) . (k + 1)),h) + (- ((S,h) . (k + 1))) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(((S,h) . (k + 1)),h) . x is V11() real ext-real Element of REAL

((((f2,h) . (k + 1)),h) . x) + ((((S,h) . (k + 1)),h) . x) is V11() real ext-real Element of REAL

(((f2,h) . ((k + 1) + 1)) . x) + ((((S,h) . (k + 1)),h) . x) is V11() real ext-real Element of REAL

0 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() Element of NAT

((f2 + S),h) . (0 + 1) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(f2,h) . (0 + 1) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(S,h) . (0 + 1) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

k is V11() real ext-real Element of REAL

(((f2 + S),h) . (0 + 1)) . k is V11() real ext-real Element of REAL

((f2,h) . (0 + 1)) . k is V11() real ext-real Element of REAL

((S,h) . (0 + 1)) . k is V11() real ext-real Element of REAL

(((f2,h) . (0 + 1)) . k) + (((S,h) . (0 + 1)) . k) is V11() real ext-real Element of REAL

((f2 + S),h) . 0 is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

((((f2 + S),h) . 0),h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

((((f2 + S),h) . 0),h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

((((f2 + S),h) . 0),h) - (((f2 + S),h) . 0) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- (((f2 + S),h) . 0) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(- 1) (#) (((f2 + S),h) . 0) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

((((f2 + S),h) . 0),h) + (- (((f2 + S),h) . 0)) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

((((f2 + S),h) . 0),h) . k is V11() real ext-real Element of REAL

((f2 + S),h) is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

((f2 + S),h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

((f2 + S),h) - (f2 + S) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- (f2 + S) is V13() V16( REAL ) Function-like total complex-valued ext-real-valued real-valued set

(- 1) (#) (f2 + S) is V13() V16( REAL ) Function-like total complex-valued ext-real-valued real-valued set

((f2 + S),h) + (- (f2 + S)) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

((f2 + S),h) . k is V11() real ext-real Element of REAL

k + h is V11() real ext-real Element of REAL

(f2 + S) . (k + h) is V11() real ext-real Element of REAL

(f2 + S) . k is V11() real ext-real Element of REAL

((f2 + S) . (k + h)) - ((f2 + S) . k) is V11() real ext-real Element of REAL

f2 . (k + h) is V11() real ext-real Element of REAL

S . (k + h) is V11() real ext-real Element of REAL

(f2 . (k + h)) + (S . (k + h)) is V11() real ext-real Element of REAL

((f2 . (k + h)) + (S . (k + h))) - ((f2 + S) . k) is V11() real ext-real Element of REAL

f2 . k is V11() real ext-real Element of REAL

S . k is V11() real ext-real Element of REAL

(f2 . k) + (S . k) is V11() real ext-real Element of REAL

((f2 . (k + h)) + (S . (k + h))) - ((f2 . k) + (S . k)) is V11() real ext-real Element of REAL

(f2 . (k + h)) - (f2 . k) is V11() real ext-real Element of REAL

(S . (k + h)) - (S . k) is V11() real ext-real Element of REAL

((f2 . (k + h)) - (f2 . k)) + ((S . (k + h)) - (S . k)) is V11() real ext-real Element of REAL

(f2,h) is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(f2,h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(f2,h) - f2 is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- f2 is V13() V16( REAL ) Function-like total complex-valued ext-real-valued real-valued set

(- 1) (#) f2 is V13() V16( REAL ) Function-like total complex-valued ext-real-valued real-valued set

(f2,h) + (- f2) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(f2,h) . k is V11() real ext-real Element of REAL

((f2,h) . k) + ((S . (k + h)) - (S . k)) is V11() real ext-real Element of REAL

(S,h) is non empty V13() V16( REAL ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(S,h) is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(S,h) - S is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- S is V13() V16( REAL ) Function-like total complex-valued ext-real-valued real-valued set

(- 1) (#) S is V13() V16( REAL ) Function-like total complex-valued ext-real-valued real-valued set

(S,h) + (- S) is V13() V16( REAL ) Function-like complex-valued ext-real-valued real-valued set

(S,h) . k is V11() real ext-real Element of REAL

((f2,h) . k) + ((S,h) . k) is V11() real ext-real Element of REAL

(f2,h) . 0 is V13() V16( REAL ) V17( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

(((f2,h) . 0