:: VFUNCT_2 semantic presentation

NAT is V129() V130() V131() V132() V133() V134() V135() Element of K6(REAL)

REAL is non empty V30() V129() V130() V131() V135() set

K6(REAL) is set

COMPLEX is non empty V30() V129() V135() set

omega is V129() V130() V131() V132() V133() V134() V135() set

K6(omega) is set

K6(NAT) is set

K7(NAT,REAL) is V119() V120() V121() set

K6(K7(NAT,REAL)) is set

RAT is non empty V30() V129() V130() V131() V132() V135() set

INT is non empty V30() V129() V130() V131() V132() V133() V135() set

{} is set

the empty V129() V130() V131() V132() V133() V134() V135() set is empty V129() V130() V131() V132() V133() V134() V135() set

1 is non empty set

0 is natural V11() real V114() V115() ext-real V129() V130() V131() V132() V133() V134() Element of NAT

1r is V11() Element of COMPLEX

- 1r is V11() Element of COMPLEX

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

M is non empty set

K7(M,COMPLEX) is V119() set

K6(K7(M,COMPLEX)) is set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

f2 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f1 is V13() V16(M) V17( COMPLEX ) Function-like V119() Element of K6(K7(M,COMPLEX))

dom f1 is Element of K6(M)

K6(M) is set

dom f2 is Element of K6(M)

(dom f1) /\ (dom f2) is Element of K6(M)

Y is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

dom Y is Element of K6(M)

c is Element of M

Y /. c is Element of the U1 of V

f2 /. c is Element of the U1 of V

f1 /. c is V11() Element of COMPLEX

(f1 /. c) * (f2 /. c) is Element of the U1 of V

M is non empty set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f2 is V11() set

dom f1 is Element of K6(M)

K6(M) is set

Y is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

dom Y is Element of K6(M)

c is Element of M

Y /. c is Element of the U1 of V

f1 /. c is Element of the U1 of V

f2 * (f1 /. c) is Element of the U1 of V

{0} is V129() V130() V131() V132() V133() V134() set

M is non empty set

K7(M,COMPLEX) is V119() set

K6(K7(M,COMPLEX)) is set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

0. V is V49(V) Element of the U1 of V

{(0. V)} is set

f1 is V13() V16(M) V17( COMPLEX ) Function-like V119() Element of K6(K7(M,COMPLEX))

dom f1 is Element of K6(M)

K6(M) is set

f1 " {0} is Element of K6(M)

(dom f1) \ (f1 " {0}) is Element of K6(M)

f2 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,f1,f2) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

dom (M,V,f1,f2) is Element of K6(M)

(M,V,f1,f2) " {(0. V)} is Element of K6(M)

(dom (M,V,f1,f2)) \ ((M,V,f1,f2) " {(0. V)}) is Element of K6(M)

dom f2 is Element of K6(M)

f2 " {(0. V)} is Element of K6(M)

(dom f2) \ (f2 " {(0. V)}) is Element of K6(M)

((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)})) is Element of K6(M)

X is set

Y is Element of M

(dom f1) /\ (dom f2) is Element of K6(M)

(M,V,f1,f2) /. Y is Element of the U1 of V

f2 /. Y is Element of the U1 of V

f1 /. Y is V11() Element of COMPLEX

(f1 /. Y) * (f2 /. Y) is Element of the U1 of V

0c is V11() Element of COMPLEX

f1 . Y is V11() set

X is set

Y is Element of M

f1 . Y is V11() set

f1 /. Y is V11() Element of COMPLEX

(dom f1) /\ (dom f2) is Element of K6(M)

f2 /. Y is Element of the U1 of V

(f1 /. Y) * (f2 /. Y) is Element of the U1 of V

(M,V,f1,f2) /. Y is Element of the U1 of V

M is non empty set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

0. V is V49(V) Element of the U1 of V

{(0. V)} is set

f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

||.f1.|| is V13() V16(M) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(M,REAL))

K7(M,REAL) is V119() V120() V121() set

K6(K7(M,REAL)) is set

||.f1.|| " {0} is Element of K6(M)

K6(M) is set

f1 " {(0. V)} is Element of K6(M)

- f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(- f1) " {(0. V)} is Element of K6(M)

f2 is Element of M

dom ||.f1.|| is Element of K6(M)

||.f1.|| . f2 is V11() real ext-real set

f1 /. f2 is Element of the U1 of V

||.(f1 /. f2).|| is V11() real ext-real Element of REAL

dom f1 is Element of K6(M)

dom f1 is Element of K6(M)

dom ||.f1.|| is Element of K6(M)

f1 /. f2 is Element of the U1 of V

||.(f1 /. f2).|| is V11() real ext-real Element of REAL

||.f1.|| . f2 is V11() real ext-real set

f2 is Element of M

dom (- f1) is Element of K6(M)

(- f1) /. f2 is Element of the U1 of V

f1 /. f2 is Element of the U1 of V

- (f1 /. f2) is Element of the U1 of V

- (- (f1 /. f2)) is Element of the U1 of V

- (0. V) is Element of the U1 of V

dom (- f1) is Element of K6(M)

f1 /. f2 is Element of the U1 of V

(- f1) /. f2 is Element of the U1 of V

- (0. V) is Element of the U1 of V

0c is V11() Element of COMPLEX

M is non empty set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

0. V is V49(V) Element of the U1 of V

{(0. V)} is set

f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f1 " {(0. V)} is Element of K6(M)

K6(M) is set

f2 is V11() Element of COMPLEX

(M,V,f1,f2) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,f1,f2) " {(0. V)} is Element of K6(M)

X is Element of M

dom (M,V,f1,f2) is Element of K6(M)

(M,V,f1,f2) /. X is Element of the U1 of V

f1 /. X is Element of the U1 of V

f2 * (f1 /. X) is Element of the U1 of V

f2 * (0. V) is Element of the U1 of V

dom f1 is Element of K6(M)

dom f1 is Element of K6(M)

dom (M,V,f1,f2) is Element of K6(M)

f1 /. X is Element of the U1 of V

f2 * (f1 /. X) is Element of the U1 of V

f2 * (0. V) is Element of the U1 of V

(M,V,f1,f2) /. X is Element of the U1 of V

M is non empty set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f2 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f1 + f2 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f2 + f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

dom (f1 + f2) is Element of K6(M)

K6(M) is set

dom f2 is Element of K6(M)

dom f1 is Element of K6(M)

(dom f2) /\ (dom f1) is Element of K6(M)

dom (f2 + f1) is Element of K6(M)

X is Element of M

(f1 + f2) /. X is Element of the U1 of V

f2 /. X is Element of the U1 of V

f1 /. X is Element of the U1 of V

(f2 /. X) + (f1 /. X) is Element of the U1 of V

(f2 + f1) /. X is Element of the U1 of V

M is non empty set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

X is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

Y is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

X + Y is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

Y + X is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

M is non empty set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f2 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,f1,f2) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

X is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,(M,V,f1,f2),X) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,f2,X) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,f1,(M,V,f2,X)) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

dom (M,V,(M,V,f1,f2),X) is Element of K6(M)

K6(M) is set

dom (M,V,f1,f2) is Element of K6(M)

dom X is Element of K6(M)

(dom (M,V,f1,f2)) /\ (dom X) is Element of K6(M)

dom f1 is Element of K6(M)

dom f2 is Element of K6(M)

(dom f1) /\ (dom f2) is Element of K6(M)

((dom f1) /\ (dom f2)) /\ (dom X) is Element of K6(M)

(dom f2) /\ (dom X) is Element of K6(M)

(dom f1) /\ ((dom f2) /\ (dom X)) is Element of K6(M)

dom (M,V,f2,X) is Element of K6(M)

(dom f1) /\ (dom (M,V,f2,X)) is Element of K6(M)

dom (M,V,f1,(M,V,f2,X)) is Element of K6(M)

Y is Element of M

(M,V,(M,V,f1,f2),X) /. Y is Element of the U1 of V

(M,V,f1,f2) /. Y is Element of the U1 of V

X /. Y is Element of the U1 of V

((M,V,f1,f2) /. Y) + (X /. Y) is Element of the U1 of V

f1 /. Y is Element of the U1 of V

f2 /. Y is Element of the U1 of V

(f1 /. Y) + (f2 /. Y) is Element of the U1 of V

((f1 /. Y) + (f2 /. Y)) + (X /. Y) is Element of the U1 of V

(f2 /. Y) + (X /. Y) is Element of the U1 of V

(f1 /. Y) + ((f2 /. Y) + (X /. Y)) is Element of the U1 of V

(M,V,f2,X) /. Y is Element of the U1 of V

(f1 /. Y) + ((M,V,f2,X) /. Y) is Element of the U1 of V

(M,V,f1,(M,V,f2,X)) /. Y is Element of the U1 of V

M is non empty set

K7(M,COMPLEX) is V119() set

K6(K7(M,COMPLEX)) is set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

f1 is V13() V16(M) V17( COMPLEX ) Function-like V119() Element of K6(K7(M,COMPLEX))

f2 is V13() V16(M) V17( COMPLEX ) Function-like V119() Element of K6(K7(M,COMPLEX))

f1 (#) f2 is V13() V16(M) V17( COMPLEX ) Function-like V119() Element of K6(K7(M,COMPLEX))

X is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,(f1 (#) f2),X) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,f2,X) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,f1,(M,V,f2,X)) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

dom (M,V,(f1 (#) f2),X) is Element of K6(M)

K6(M) is set

dom (f1 (#) f2) is Element of K6(M)

dom X is Element of K6(M)

(dom (f1 (#) f2)) /\ (dom X) is Element of K6(M)

dom f1 is Element of K6(M)

dom f2 is Element of K6(M)

(dom f1) /\ (dom f2) is Element of K6(M)

((dom f1) /\ (dom f2)) /\ (dom X) is Element of K6(M)

(dom f2) /\ (dom X) is Element of K6(M)

(dom f1) /\ ((dom f2) /\ (dom X)) is Element of K6(M)

dom (M,V,f2,X) is Element of K6(M)

(dom f1) /\ (dom (M,V,f2,X)) is Element of K6(M)

dom (M,V,f1,(M,V,f2,X)) is Element of K6(M)

Y is Element of M

f1 . Y is V11() set

f1 /. Y is V11() Element of COMPLEX

f2 . Y is V11() set

f2 /. Y is V11() Element of COMPLEX

(f1 (#) f2) /. Y is V11() Element of COMPLEX

(f1 (#) f2) . Y is V11() set

(f1 /. Y) * (f2 /. Y) is V11() Element of COMPLEX

(M,V,(f1 (#) f2),X) /. Y is Element of the U1 of V

X /. Y is Element of the U1 of V

((f1 (#) f2) /. Y) * (X /. Y) is Element of the U1 of V

(f2 /. Y) * (X /. Y) is Element of the U1 of V

(f1 /. Y) * ((f2 /. Y) * (X /. Y)) is Element of the U1 of V

(M,V,f2,X) /. Y is Element of the U1 of V

(f1 /. Y) * ((M,V,f2,X) /. Y) is Element of the U1 of V

(M,V,f1,(M,V,f2,X)) /. Y is Element of the U1 of V

M is non empty set

K7(M,COMPLEX) is V119() set

K6(K7(M,COMPLEX)) is set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f2 is V13() V16(M) V17( COMPLEX ) Function-like V119() Element of K6(K7(M,COMPLEX))

X is V13() V16(M) V17( COMPLEX ) Function-like V119() Element of K6(K7(M,COMPLEX))

f2 + X is V13() V16(M) V17( COMPLEX ) Function-like V119() Element of K6(K7(M,COMPLEX))

(M,V,(f2 + X),f1) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,f2,f1) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,X,f1) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,(M,V,f2,f1),(M,V,X,f1)) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

dom (M,V,(f2 + X),f1) is Element of K6(M)

K6(M) is set

dom (f2 + X) is Element of K6(M)

dom f1 is Element of K6(M)

(dom (f2 + X)) /\ (dom f1) is Element of K6(M)

dom f2 is Element of K6(M)

dom X is Element of K6(M)

(dom f2) /\ (dom X) is Element of K6(M)

(dom f1) /\ (dom f1) is Element of K6(M)

((dom f2) /\ (dom X)) /\ ((dom f1) /\ (dom f1)) is Element of K6(M)

((dom f2) /\ (dom X)) /\ (dom f1) is Element of K6(M)

(((dom f2) /\ (dom X)) /\ (dom f1)) /\ (dom f1) is Element of K6(M)

(dom f2) /\ (dom f1) is Element of K6(M)

((dom f2) /\ (dom f1)) /\ (dom X) is Element of K6(M)

(((dom f2) /\ (dom f1)) /\ (dom X)) /\ (dom f1) is Element of K6(M)

(dom X) /\ (dom f1) is Element of K6(M)

((dom f2) /\ (dom f1)) /\ ((dom X) /\ (dom f1)) is Element of K6(M)

dom (M,V,f2,f1) is Element of K6(M)

(dom (M,V,f2,f1)) /\ ((dom X) /\ (dom f1)) is Element of K6(M)

dom (M,V,X,f1) is Element of K6(M)

(dom (M,V,f2,f1)) /\ (dom (M,V,X,f1)) is Element of K6(M)

dom (M,V,(M,V,f2,f1),(M,V,X,f1)) is Element of K6(M)

Y is Element of M

f2 /. Y is V11() Element of COMPLEX

f2 . Y is V11() set

X /. Y is V11() Element of COMPLEX

X . Y is V11() set

(f2 + X) /. Y is V11() Element of COMPLEX

(f2 + X) . Y is V11() set

(f2 /. Y) + (X /. Y) is V11() Element of COMPLEX

(M,V,(f2 + X),f1) /. Y is Element of the U1 of V

f1 /. Y is Element of the U1 of V

((f2 + X) /. Y) * (f1 /. Y) is Element of the U1 of V

(f2 /. Y) * (f1 /. Y) is Element of the U1 of V

(X /. Y) * (f1 /. Y) is Element of the U1 of V

((f2 /. Y) * (f1 /. Y)) + ((X /. Y) * (f1 /. Y)) is Element of the U1 of V

(M,V,f2,f1) /. Y is Element of the U1 of V

((M,V,f2,f1) /. Y) + ((X /. Y) * (f1 /. Y)) is Element of the U1 of V

(M,V,X,f1) /. Y is Element of the U1 of V

((M,V,f2,f1) /. Y) + ((M,V,X,f1) /. Y) is Element of the U1 of V

(M,V,(M,V,f2,f1),(M,V,X,f1)) /. Y is Element of the U1 of V

M is non empty set

K7(M,COMPLEX) is V119() set

K6(K7(M,COMPLEX)) is set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f2 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,f1,f2) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

X is V13() V16(M) V17( COMPLEX ) Function-like V119() Element of K6(K7(M,COMPLEX))

(M,V,X,(M,V,f1,f2)) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,X,f1) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,X,f2) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,(M,V,X,f1),(M,V,X,f2)) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

dom (M,V,X,(M,V,f1,f2)) is Element of K6(M)

K6(M) is set

dom X is Element of K6(M)

dom (M,V,f1,f2) is Element of K6(M)

(dom X) /\ (dom (M,V,f1,f2)) is Element of K6(M)

dom f1 is Element of K6(M)

dom f2 is Element of K6(M)

(dom f1) /\ (dom f2) is Element of K6(M)

(dom X) /\ ((dom f1) /\ (dom f2)) is Element of K6(M)

(dom X) /\ (dom X) is Element of K6(M)

((dom X) /\ (dom X)) /\ (dom f1) is Element of K6(M)

(((dom X) /\ (dom X)) /\ (dom f1)) /\ (dom f2) is Element of K6(M)

(dom X) /\ (dom f1) is Element of K6(M)

((dom X) /\ (dom f1)) /\ (dom X) is Element of K6(M)

(((dom X) /\ (dom f1)) /\ (dom X)) /\ (dom f2) is Element of K6(M)

(dom X) /\ (dom f2) is Element of K6(M)

((dom X) /\ (dom f1)) /\ ((dom X) /\ (dom f2)) is Element of K6(M)

dom (M,V,X,f1) is Element of K6(M)

(dom (M,V,X,f1)) /\ ((dom X) /\ (dom f2)) is Element of K6(M)

dom (M,V,X,f2) is Element of K6(M)

(dom (M,V,X,f1)) /\ (dom (M,V,X,f2)) is Element of K6(M)

dom (M,V,(M,V,X,f1),(M,V,X,f2)) is Element of K6(M)

Y is Element of M

(M,V,X,(M,V,f1,f2)) /. Y is Element of the U1 of V

(M,V,f1,f2) /. Y is Element of the U1 of V

X /. Y is V11() Element of COMPLEX

(X /. Y) * ((M,V,f1,f2) /. Y) is Element of the U1 of V

f1 /. Y is Element of the U1 of V

f2 /. Y is Element of the U1 of V

(f1 /. Y) + (f2 /. Y) is Element of the U1 of V

(X /. Y) * ((f1 /. Y) + (f2 /. Y)) is Element of the U1 of V

(X /. Y) * (f1 /. Y) is Element of the U1 of V

(X /. Y) * (f2 /. Y) is Element of the U1 of V

((X /. Y) * (f1 /. Y)) + ((X /. Y) * (f2 /. Y)) is Element of the U1 of V

(M,V,X,f1) /. Y is Element of the U1 of V

((M,V,X,f1) /. Y) + ((X /. Y) * (f2 /. Y)) is Element of the U1 of V

(M,V,X,f2) /. Y is Element of the U1 of V

((M,V,X,f1) /. Y) + ((M,V,X,f2) /. Y) is Element of the U1 of V

(M,V,(M,V,X,f1),(M,V,X,f2)) /. Y is Element of the U1 of V

M is non empty set

K7(M,COMPLEX) is V119() set

K6(K7(M,COMPLEX)) is set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f2 is V11() Element of COMPLEX

X is V13() V16(M) V17( COMPLEX ) Function-like V119() Element of K6(K7(M,COMPLEX))

(M,V,X,f1) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,(M,V,X,f1),f2) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f2 (#) X is V13() V16(M) V17( COMPLEX ) Function-like V119() Element of K6(K7(M,COMPLEX))

(M,V,(f2 (#) X),f1) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

dom (M,V,X,f1) is Element of K6(M)

K6(M) is set

dom X is Element of K6(M)

dom f1 is Element of K6(M)

(dom X) /\ (dom f1) is Element of K6(M)

dom (M,V,(M,V,X,f1),f2) is Element of K6(M)

dom (f2 (#) X) is Element of K6(M)

(dom (f2 (#) X)) /\ (dom f1) is Element of K6(M)

dom (M,V,(f2 (#) X),f1) is Element of K6(M)

Y is Element of M

(f2 (#) X) /. Y is V11() Element of COMPLEX

(f2 (#) X) . Y is V11() set

X /. Y is V11() Element of COMPLEX

X . Y is V11() set

(M,V,(M,V,X,f1),f2) /. Y is Element of the U1 of V

(M,V,X,f1) /. Y is Element of the U1 of V

f2 * ((M,V,X,f1) /. Y) is Element of the U1 of V

f1 /. Y is Element of the U1 of V

(X /. Y) * (f1 /. Y) is Element of the U1 of V

f2 * ((X /. Y) * (f1 /. Y)) is Element of the U1 of V

f2 * (X /. Y) is V11() Element of COMPLEX

(f2 * (X /. Y)) * (f1 /. Y) is Element of the U1 of V

((f2 (#) X) /. Y) * (f1 /. Y) is Element of the U1 of V

(M,V,(f2 (#) X),f1) /. Y is Element of the U1 of V

M is non empty set

K7(M,COMPLEX) is V119() set

K6(K7(M,COMPLEX)) is set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f2 is V11() Element of COMPLEX

(M,V,f1,f2) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

X is V13() V16(M) V17( COMPLEX ) Function-like V119() Element of K6(K7(M,COMPLEX))

(M,V,X,f1) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,(M,V,X,f1),f2) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,X,(M,V,f1,f2)) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

dom (M,V,(M,V,X,f1),f2) is Element of K6(M)

K6(M) is set

dom (M,V,X,f1) is Element of K6(M)

dom X is Element of K6(M)

dom f1 is Element of K6(M)

(dom X) /\ (dom f1) is Element of K6(M)

dom (M,V,f1,f2) is Element of K6(M)

(dom X) /\ (dom (M,V,f1,f2)) is Element of K6(M)

dom (M,V,X,(M,V,f1,f2)) is Element of K6(M)

Y is Element of M

(M,V,(M,V,X,f1),f2) /. Y is Element of the U1 of V

(M,V,X,f1) /. Y is Element of the U1 of V

f2 * ((M,V,X,f1) /. Y) is Element of the U1 of V

f1 /. Y is Element of the U1 of V

X /. Y is V11() Element of COMPLEX

(X /. Y) * (f1 /. Y) is Element of the U1 of V

f2 * ((X /. Y) * (f1 /. Y)) is Element of the U1 of V

(X /. Y) * f2 is V11() Element of COMPLEX

((X /. Y) * f2) * (f1 /. Y) is Element of the U1 of V

f2 * (f1 /. Y) is Element of the U1 of V

(X /. Y) * (f2 * (f1 /. Y)) is Element of the U1 of V

(M,V,f1,f2) /. Y is Element of the U1 of V

(X /. Y) * ((M,V,f1,f2) /. Y) is Element of the U1 of V

(M,V,X,(M,V,f1,f2)) /. Y is Element of the U1 of V

M is non empty set

K7(M,COMPLEX) is V119() set

K6(K7(M,COMPLEX)) is set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f2 is V13() V16(M) V17( COMPLEX ) Function-like V119() Element of K6(K7(M,COMPLEX))

X is V13() V16(M) V17( COMPLEX ) Function-like V119() Element of K6(K7(M,COMPLEX))

f2 - X is V13() V16(M) V17( COMPLEX ) Function-like V119() Element of K6(K7(M,COMPLEX))

- X is V13() Function-like V119() set

- 1 is V11() set

(- 1) (#) X is V13() Function-like set

f2 + (- X) is V13() Function-like set

(M,V,(f2 - X),f1) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,f2,f1) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,X,f1) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,f2,f1) - (M,V,X,f1) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

dom (M,V,(f2 - X),f1) is Element of K6(M)

K6(M) is set

- X is V13() V16(M) V17( COMPLEX ) Function-like V119() Element of K6(K7(M,COMPLEX))

f2 + (- X) is V13() V16(M) V17( COMPLEX ) Function-like V119() Element of K6(K7(M,COMPLEX))

dom (f2 + (- X)) is Element of K6(M)

dom f1 is Element of K6(M)

(dom (f2 + (- X))) /\ (dom f1) is Element of K6(M)

dom f2 is Element of K6(M)

dom (- X) is Element of K6(M)

(dom f2) /\ (dom (- X)) is Element of K6(M)

(dom f1) /\ (dom f1) is Element of K6(M)

((dom f2) /\ (dom (- X))) /\ ((dom f1) /\ (dom f1)) is Element of K6(M)

dom X is Element of K6(M)

(dom f2) /\ (dom X) is Element of K6(M)

((dom f2) /\ (dom X)) /\ ((dom f1) /\ (dom f1)) is Element of K6(M)

((dom f2) /\ (dom X)) /\ (dom f1) is Element of K6(M)

(((dom f2) /\ (dom X)) /\ (dom f1)) /\ (dom f1) is Element of K6(M)

(dom f2) /\ (dom f1) is Element of K6(M)

((dom f2) /\ (dom f1)) /\ (dom X) is Element of K6(M)

(((dom f2) /\ (dom f1)) /\ (dom X)) /\ (dom f1) is Element of K6(M)

(dom X) /\ (dom f1) is Element of K6(M)

((dom f2) /\ (dom f1)) /\ ((dom X) /\ (dom f1)) is Element of K6(M)

dom (M,V,f2,f1) is Element of K6(M)

(dom (M,V,f2,f1)) /\ ((dom X) /\ (dom f1)) is Element of K6(M)

dom (M,V,X,f1) is Element of K6(M)

(dom (M,V,f2,f1)) /\ (dom (M,V,X,f1)) is Element of K6(M)

dom ((M,V,f2,f1) - (M,V,X,f1)) is Element of K6(M)

Y is Element of M

dom (f2 - X) is Element of K6(M)

(dom (f2 - X)) /\ (dom f1) is Element of K6(M)

f2 /. Y is V11() Element of COMPLEX

f2 . Y is V11() set

(f2 + (- X)) /. Y is V11() Element of COMPLEX

(f2 + (- X)) . Y is V11() set

(- X) . Y is V11() set

(f2 . Y) + ((- X) . Y) is set

(- X) /. Y is V11() Element of COMPLEX

(f2 /. Y) + ((- X) /. Y) is V11() Element of COMPLEX

X . Y is V11() set

- (X . Y) is V11() set

X /. Y is V11() Element of COMPLEX

(M,V,(f2 - X),f1) /. Y is Element of the U1 of V

f1 /. Y is Element of the U1 of V

(f2 /. Y) - (X /. Y) is V11() Element of COMPLEX

((f2 /. Y) - (X /. Y)) * (f1 /. Y) is Element of the U1 of V

(f2 /. Y) * (f1 /. Y) is Element of the U1 of V

(X /. Y) * (f1 /. Y) is Element of the U1 of V

((f2 /. Y) * (f1 /. Y)) - ((X /. Y) * (f1 /. Y)) is Element of the U1 of V

- ((X /. Y) * (f1 /. Y)) is Element of the U1 of V

K164(V,((f2 /. Y) * (f1 /. Y)),(- ((X /. Y) * (f1 /. Y)))) is Element of the U1 of V

(M,V,f2,f1) /. Y is Element of the U1 of V

((M,V,f2,f1) /. Y) - ((X /. Y) * (f1 /. Y)) is Element of the U1 of V

K164(V,((M,V,f2,f1) /. Y),(- ((X /. Y) * (f1 /. Y)))) is Element of the U1 of V

(M,V,X,f1) /. Y is Element of the U1 of V

((M,V,f2,f1) /. Y) - ((M,V,X,f1) /. Y) is Element of the U1 of V

- ((M,V,X,f1) /. Y) is Element of the U1 of V

K164(V,((M,V,f2,f1) /. Y),(- ((M,V,X,f1) /. Y))) is Element of the U1 of V

((M,V,f2,f1) - (M,V,X,f1)) /. Y is Element of the U1 of V

M is non empty set

K7(M,COMPLEX) is V119() set

K6(K7(M,COMPLEX)) is set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f2 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f1 - f2 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

X is V13() V16(M) V17( COMPLEX ) Function-like V119() Element of K6(K7(M,COMPLEX))

(M,V,X,f1) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,X,f2) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,X,f1) - (M,V,X,f2) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,X,(f1 - f2)) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

dom ((M,V,X,f1) - (M,V,X,f2)) is Element of K6(M)

K6(M) is set

dom (M,V,X,f1) is Element of K6(M)

dom (M,V,X,f2) is Element of K6(M)

(dom (M,V,X,f1)) /\ (dom (M,V,X,f2)) is Element of K6(M)

dom X is Element of K6(M)

dom f2 is Element of K6(M)

(dom X) /\ (dom f2) is Element of K6(M)

(dom (M,V,X,f1)) /\ ((dom X) /\ (dom f2)) is Element of K6(M)

dom f1 is Element of K6(M)

(dom X) /\ (dom f1) is Element of K6(M)

((dom X) /\ (dom f1)) /\ ((dom X) /\ (dom f2)) is Element of K6(M)

(dom X) /\ ((dom X) /\ (dom f1)) is Element of K6(M)

((dom X) /\ ((dom X) /\ (dom f1))) /\ (dom f2) is Element of K6(M)

(dom X) /\ (dom X) is Element of K6(M)

((dom X) /\ (dom X)) /\ (dom f1) is Element of K6(M)

(((dom X) /\ (dom X)) /\ (dom f1)) /\ (dom f2) is Element of K6(M)

(dom f1) /\ (dom f2) is Element of K6(M)

(dom X) /\ ((dom f1) /\ (dom f2)) is Element of K6(M)

dom (f1 - f2) is Element of K6(M)

(dom X) /\ (dom (f1 - f2)) is Element of K6(M)

dom (M,V,X,(f1 - f2)) is Element of K6(M)

Y is Element of M

(M,V,X,(f1 - f2)) /. Y is Element of the U1 of V

(f1 - f2) /. Y is Element of the U1 of V

X /. Y is V11() Element of COMPLEX

(X /. Y) * ((f1 - f2) /. Y) is Element of the U1 of V

f1 /. Y is Element of the U1 of V

f2 /. Y is Element of the U1 of V

(f1 /. Y) - (f2 /. Y) is Element of the U1 of V

- (f2 /. Y) is Element of the U1 of V

K164(V,(f1 /. Y),(- (f2 /. Y))) is Element of the U1 of V

(X /. Y) * ((f1 /. Y) - (f2 /. Y)) is Element of the U1 of V

(X /. Y) * (f1 /. Y) is Element of the U1 of V

(X /. Y) * (f2 /. Y) is Element of the U1 of V

((X /. Y) * (f1 /. Y)) - ((X /. Y) * (f2 /. Y)) is Element of the U1 of V

- ((X /. Y) * (f2 /. Y)) is Element of the U1 of V

K164(V,((X /. Y) * (f1 /. Y)),(- ((X /. Y) * (f2 /. Y)))) is Element of the U1 of V

(M,V,X,f1) /. Y is Element of the U1 of V

((M,V,X,f1) /. Y) - ((X /. Y) * (f2 /. Y)) is Element of the U1 of V

K164(V,((M,V,X,f1) /. Y),(- ((X /. Y) * (f2 /. Y)))) is Element of the U1 of V

(M,V,X,f2) /. Y is Element of the U1 of V

((M,V,X,f1) /. Y) - ((M,V,X,f2) /. Y) is Element of the U1 of V

- ((M,V,X,f2) /. Y) is Element of the U1 of V

K164(V,((M,V,X,f1) /. Y),(- ((M,V,X,f2) /. Y))) is Element of the U1 of V

((M,V,X,f1) - (M,V,X,f2)) /. Y is Element of the U1 of V

M is non empty set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f2 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,f1,f2) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

X is V11() Element of COMPLEX

(M,V,(M,V,f1,f2),X) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,f1,X) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,f2,X) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,(M,V,f1,X),(M,V,f2,X)) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

dom (M,V,(M,V,f1,f2),X) is Element of K6(M)

K6(M) is set

dom (M,V,f1,f2) is Element of K6(M)

dom f1 is Element of K6(M)

dom f2 is Element of K6(M)

(dom f1) /\ (dom f2) is Element of K6(M)

dom (M,V,f2,X) is Element of K6(M)

(dom f1) /\ (dom (M,V,f2,X)) is Element of K6(M)

dom (M,V,f1,X) is Element of K6(M)

(dom (M,V,f1,X)) /\ (dom (M,V,f2,X)) is Element of K6(M)

dom (M,V,(M,V,f1,X),(M,V,f2,X)) is Element of K6(M)

Y is Element of M

(M,V,(M,V,f1,f2),X) /. Y is Element of the U1 of V

(M,V,f1,f2) /. Y is Element of the U1 of V

X * ((M,V,f1,f2) /. Y) is Element of the U1 of V

f1 /. Y is Element of the U1 of V

f2 /. Y is Element of the U1 of V

(f1 /. Y) + (f2 /. Y) is Element of the U1 of V

X * ((f1 /. Y) + (f2 /. Y)) is Element of the U1 of V

X * (f1 /. Y) is Element of the U1 of V

X * (f2 /. Y) is Element of the U1 of V

(X * (f1 /. Y)) + (X * (f2 /. Y)) is Element of the U1 of V

(M,V,f1,X) /. Y is Element of the U1 of V

((M,V,f1,X) /. Y) + (X * (f2 /. Y)) is Element of the U1 of V

(M,V,f2,X) /. Y is Element of the U1 of V

((M,V,f1,X) /. Y) + ((M,V,f2,X) /. Y) is Element of the U1 of V

(M,V,(M,V,f1,X),(M,V,f2,X)) /. Y is Element of the U1 of V

M is non empty set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f2 is V11() Element of COMPLEX

X is V11() Element of COMPLEX

f2 * X is V11() Element of COMPLEX

(M,V,f1,(f2 * X)) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,f1,X) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,(M,V,f1,X),f2) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

dom (M,V,f1,(f2 * X)) is Element of K6(M)

K6(M) is set

dom f1 is Element of K6(M)

dom (M,V,f1,X) is Element of K6(M)

dom (M,V,(M,V,f1,X),f2) is Element of K6(M)

Y is Element of M

(M,V,f1,(f2 * X)) /. Y is Element of the U1 of V

f1 /. Y is Element of the U1 of V

(f2 * X) * (f1 /. Y) is Element of the U1 of V

X * (f1 /. Y) is Element of the U1 of V

f2 * (X * (f1 /. Y)) is Element of the U1 of V

(M,V,f1,X) /. Y is Element of the U1 of V

f2 * ((M,V,f1,X) /. Y) is Element of the U1 of V

(M,V,(M,V,f1,X),f2) /. Y is Element of the U1 of V

M is non empty set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f2 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f1 - f2 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

X is V11() Element of COMPLEX

(M,V,(f1 - f2),X) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,f1,X) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,f2,X) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,f1,X) - (M,V,f2,X) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

dom (M,V,(f1 - f2),X) is Element of K6(M)

K6(M) is set

dom (f1 - f2) is Element of K6(M)

dom f1 is Element of K6(M)

dom f2 is Element of K6(M)

(dom f1) /\ (dom f2) is Element of K6(M)

dom (M,V,f2,X) is Element of K6(M)

(dom f1) /\ (dom (M,V,f2,X)) is Element of K6(M)

dom (M,V,f1,X) is Element of K6(M)

(dom (M,V,f1,X)) /\ (dom (M,V,f2,X)) is Element of K6(M)

dom ((M,V,f1,X) - (M,V,f2,X)) is Element of K6(M)

Y is Element of M

(M,V,(f1 - f2),X) /. Y is Element of the U1 of V

(f1 - f2) /. Y is Element of the U1 of V

X * ((f1 - f2) /. Y) is Element of the U1 of V

f1 /. Y is Element of the U1 of V

f2 /. Y is Element of the U1 of V

(f1 /. Y) - (f2 /. Y) is Element of the U1 of V

- (f2 /. Y) is Element of the U1 of V

K164(V,(f1 /. Y),(- (f2 /. Y))) is Element of the U1 of V

X * ((f1 /. Y) - (f2 /. Y)) is Element of the U1 of V

X * (f1 /. Y) is Element of the U1 of V

X * (f2 /. Y) is Element of the U1 of V

(X * (f1 /. Y)) - (X * (f2 /. Y)) is Element of the U1 of V

- (X * (f2 /. Y)) is Element of the U1 of V

K164(V,(X * (f1 /. Y)),(- (X * (f2 /. Y)))) is Element of the U1 of V

(M,V,f1,X) /. Y is Element of the U1 of V

((M,V,f1,X) /. Y) - (X * (f2 /. Y)) is Element of the U1 of V

K164(V,((M,V,f1,X) /. Y),(- (X * (f2 /. Y)))) is Element of the U1 of V

(M,V,f2,X) /. Y is Element of the U1 of V

((M,V,f1,X) /. Y) - ((M,V,f2,X) /. Y) is Element of the U1 of V

- ((M,V,f2,X) /. Y) is Element of the U1 of V

K164(V,((M,V,f1,X) /. Y),(- ((M,V,f2,X) /. Y))) is Element of the U1 of V

((M,V,f1,X) - (M,V,f2,X)) /. Y is Element of the U1 of V

M is non empty set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f2 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f1 - f2 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f2 - f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,(f2 - f1),(- 1r)) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

dom (f1 - f2) is Element of K6(M)

K6(M) is set

dom f2 is Element of K6(M)

dom f1 is Element of K6(M)

(dom f2) /\ (dom f1) is Element of K6(M)

dom (f2 - f1) is Element of K6(M)

dom (M,V,(f2 - f1),(- 1r)) is Element of K6(M)

X is Element of M

(f1 - f2) /. X is Element of the U1 of V

f1 /. X is Element of the U1 of V

f2 /. X is Element of the U1 of V

(f1 /. X) - (f2 /. X) is Element of the U1 of V

- (f2 /. X) is Element of the U1 of V

K164(V,(f1 /. X),(- (f2 /. X))) is Element of the U1 of V

(f2 /. X) - (f1 /. X) is Element of the U1 of V

- (f1 /. X) is Element of the U1 of V

K164(V,(f2 /. X),(- (f1 /. X))) is Element of the U1 of V

- ((f2 /. X) - (f1 /. X)) is Element of the U1 of V

(- 1r) * ((f2 /. X) - (f1 /. X)) is Element of the U1 of V

(f2 - f1) /. X is Element of the U1 of V

(- 1r) * ((f2 - f1) /. X) is Element of the U1 of V

(M,V,(f2 - f1),(- 1r)) /. X is Element of the U1 of V

M is non empty set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f2 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f1 - f2 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

X is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,f2,X) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f1 - (M,V,f2,X) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(f1 - f2) - X is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

dom (f1 - (M,V,f2,X)) is Element of K6(M)

K6(M) is set

dom f1 is Element of K6(M)

dom (M,V,f2,X) is Element of K6(M)

(dom f1) /\ (dom (M,V,f2,X)) is Element of K6(M)

dom f2 is Element of K6(M)

dom X is Element of K6(M)

(dom f2) /\ (dom X) is Element of K6(M)

(dom f1) /\ ((dom f2) /\ (dom X)) is Element of K6(M)

(dom f1) /\ (dom f2) is Element of K6(M)

((dom f1) /\ (dom f2)) /\ (dom X) is Element of K6(M)

dom (f1 - f2) is Element of K6(M)

(dom (f1 - f2)) /\ (dom X) is Element of K6(M)

dom ((f1 - f2) - X) is Element of K6(M)

Y is Element of M

(f1 - (M,V,f2,X)) /. Y is Element of the U1 of V

f1 /. Y is Element of the U1 of V

(M,V,f2,X) /. Y is Element of the U1 of V

(f1 /. Y) - ((M,V,f2,X) /. Y) is Element of the U1 of V

- ((M,V,f2,X) /. Y) is Element of the U1 of V

K164(V,(f1 /. Y),(- ((M,V,f2,X) /. Y))) is Element of the U1 of V

f2 /. Y is Element of the U1 of V

X /. Y is Element of the U1 of V

(f2 /. Y) + (X /. Y) is Element of the U1 of V

(f1 /. Y) - ((f2 /. Y) + (X /. Y)) is Element of the U1 of V

- ((f2 /. Y) + (X /. Y)) is Element of the U1 of V

K164(V,(f1 /. Y),(- ((f2 /. Y) + (X /. Y)))) is Element of the U1 of V

(f1 /. Y) - (f2 /. Y) is Element of the U1 of V

- (f2 /. Y) is Element of the U1 of V

K164(V,(f1 /. Y),(- (f2 /. Y))) is Element of the U1 of V

((f1 /. Y) - (f2 /. Y)) - (X /. Y) is Element of the U1 of V

- (X /. Y) is Element of the U1 of V

K164(V,((f1 /. Y) - (f2 /. Y)),(- (X /. Y))) is Element of the U1 of V

(f1 - f2) /. Y is Element of the U1 of V

((f1 - f2) /. Y) - (X /. Y) is Element of the U1 of V

K164(V,((f1 - f2) /. Y),(- (X /. Y))) is Element of the U1 of V

((f1 - f2) - X) /. Y is Element of the U1 of V

M is non empty set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,f1,1r) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f2 is Element of M

dom (M,V,f1,1r) is Element of K6(M)

K6(M) is set

(M,V,f1,1r) /. f2 is Element of the U1 of V

f1 /. f2 is Element of the U1 of V

1r * (f1 /. f2) is Element of the U1 of V

dom f1 is Element of K6(M)

M is non empty set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f2 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f1 - f2 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

X is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f2 - X is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f1 - (f2 - X) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,(f1 - f2),X) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

dom (f1 - (f2 - X)) is Element of K6(M)

K6(M) is set

dom f1 is Element of K6(M)

dom (f2 - X) is Element of K6(M)

(dom f1) /\ (dom (f2 - X)) is Element of K6(M)

dom f2 is Element of K6(M)

dom X is Element of K6(M)

(dom f2) /\ (dom X) is Element of K6(M)

(dom f1) /\ ((dom f2) /\ (dom X)) is Element of K6(M)

(dom f1) /\ (dom f2) is Element of K6(M)

((dom f1) /\ (dom f2)) /\ (dom X) is Element of K6(M)

dom (f1 - f2) is Element of K6(M)

(dom (f1 - f2)) /\ (dom X) is Element of K6(M)

dom (M,V,(f1 - f2),X) is Element of K6(M)

Y is Element of M

(f1 - (f2 - X)) /. Y is Element of the U1 of V

f1 /. Y is Element of the U1 of V

(f2 - X) /. Y is Element of the U1 of V

(f1 /. Y) - ((f2 - X) /. Y) is Element of the U1 of V

- ((f2 - X) /. Y) is Element of the U1 of V

K164(V,(f1 /. Y),(- ((f2 - X) /. Y))) is Element of the U1 of V

f2 /. Y is Element of the U1 of V

X /. Y is Element of the U1 of V

(f2 /. Y) - (X /. Y) is Element of the U1 of V

- (X /. Y) is Element of the U1 of V

K164(V,(f2 /. Y),(- (X /. Y))) is Element of the U1 of V

(f1 /. Y) - ((f2 /. Y) - (X /. Y)) is Element of the U1 of V

- ((f2 /. Y) - (X /. Y)) is Element of the U1 of V

K164(V,(f1 /. Y),(- ((f2 /. Y) - (X /. Y)))) is Element of the U1 of V

(f1 /. Y) - (f2 /. Y) is Element of the U1 of V

- (f2 /. Y) is Element of the U1 of V

K164(V,(f1 /. Y),(- (f2 /. Y))) is Element of the U1 of V

((f1 /. Y) - (f2 /. Y)) + (X /. Y) is Element of the U1 of V

(f1 - f2) /. Y is Element of the U1 of V

((f1 - f2) /. Y) + (X /. Y) is Element of the U1 of V

(M,V,(f1 - f2),X) /. Y is Element of the U1 of V

M is non empty set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f2 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,f1,f2) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

X is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f2 - X is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,f1,(f2 - X)) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,f1,f2) - X is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

dom (M,V,f1,(f2 - X)) is Element of K6(M)

K6(M) is set

dom f1 is Element of K6(M)

dom (f2 - X) is Element of K6(M)

(dom f1) /\ (dom (f2 - X)) is Element of K6(M)

dom f2 is Element of K6(M)

dom X is Element of K6(M)

(dom f2) /\ (dom X) is Element of K6(M)

(dom f1) /\ ((dom f2) /\ (dom X)) is Element of K6(M)

(dom f1) /\ (dom f2) is Element of K6(M)

((dom f1) /\ (dom f2)) /\ (dom X) is Element of K6(M)

dom (M,V,f1,f2) is Element of K6(M)

(dom (M,V,f1,f2)) /\ (dom X) is Element of K6(M)

dom ((M,V,f1,f2) - X) is Element of K6(M)

Y is Element of M

(M,V,f1,(f2 - X)) /. Y is Element of the U1 of V

f1 /. Y is Element of the U1 of V

(f2 - X) /. Y is Element of the U1 of V

(f1 /. Y) + ((f2 - X) /. Y) is Element of the U1 of V

f2 /. Y is Element of the U1 of V

X /. Y is Element of the U1 of V

(f2 /. Y) - (X /. Y) is Element of the U1 of V

- (X /. Y) is Element of the U1 of V

K164(V,(f2 /. Y),(- (X /. Y))) is Element of the U1 of V

(f1 /. Y) + ((f2 /. Y) - (X /. Y)) is Element of the U1 of V

(f1 /. Y) + (f2 /. Y) is Element of the U1 of V

((f1 /. Y) + (f2 /. Y)) - (X /. Y) is Element of the U1 of V

K164(V,((f1 /. Y) + (f2 /. Y)),(- (X /. Y))) is Element of the U1 of V

(M,V,f1,f2) /. Y is Element of the U1 of V

((M,V,f1,f2) /. Y) - (X /. Y) is Element of the U1 of V

K164(V,((M,V,f1,f2) /. Y),(- (X /. Y))) is Element of the U1 of V

((M,V,f1,f2) - X) /. Y is Element of the U1 of V

M is non empty set

K7(M,COMPLEX) is V119() set

K6(K7(M,COMPLEX)) is set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

||.f1.|| is V13() V16(M) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(M,REAL))

K7(M,REAL) is V119() V120() V121() set

K6(K7(M,REAL)) is set

f2 is V13() V16(M) V17( COMPLEX ) Function-like V119() Element of K6(K7(M,COMPLEX))

(M,V,f2,f1) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

||.(M,V,f2,f1).|| is V13() V16(M) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(M,REAL))

|.f2.| is V13() V16(M) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(M,REAL))

|.f2.| (#) ||.f1.|| is V13() V16(M) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(M,REAL))

dom (M,V,f2,f1) is Element of K6(M)

K6(M) is set

dom f2 is Element of K6(M)

dom f1 is Element of K6(M)

(dom f2) /\ (dom f1) is Element of K6(M)

dom ||.f1.|| is Element of K6(M)

(dom f2) /\ (dom ||.f1.||) is Element of K6(M)

dom |.f2.| is Element of K6(M)

(dom |.f2.|) /\ (dom ||.f1.||) is Element of K6(M)

dom (|.f2.| (#) ||.f1.||) is Element of K6(M)

dom ||.(M,V,f2,f1).|| is Element of K6(M)

X is Element of M

f2 /. X is V11() Element of COMPLEX

f2 . X is V11() set

||.(M,V,f2,f1).|| . X is V11() real ext-real set

(M,V,f2,f1) /. X is Element of the U1 of V

||.((M,V,f2,f1) /. X).|| is V11() real ext-real Element of REAL

f1 /. X is Element of the U1 of V

(f2 /. X) * (f1 /. X) is Element of the U1 of V

||.((f2 /. X) * (f1 /. X)).|| is V11() real ext-real Element of REAL

|.(f2 /. X).| is V11() real ext-real Element of REAL

||.(f1 /. X).|| is V11() real ext-real Element of REAL

|.(f2 /. X).| * ||.(f1 /. X).|| is V11() real ext-real Element of REAL

|.f2.| . X is V11() real ext-real set

(|.f2.| . X) * ||.(f1 /. X).|| is V11() real ext-real Element of REAL

||.f1.|| . X is V11() real ext-real set

(|.f2.| . X) * (||.f1.|| . X) is V11() real ext-real set

(|.f2.| (#) ||.f1.||) . X is V11() real ext-real set

M is non empty set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

||.f1.|| is V13() V16(M) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(M,REAL))

K7(M,REAL) is V119() V120() V121() set

K6(K7(M,REAL)) is set

f2 is V11() Element of COMPLEX

(M,V,f1,f2) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

||.(M,V,f1,f2).|| is V13() V16(M) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(M,REAL))

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

|.f2.| (#) ||.f1.|| is V13() V16(M) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(M,REAL))

dom ||.(M,V,f1,f2).|| is Element of K6(M)

K6(M) is set

dom (M,V,f1,f2) is Element of K6(M)

dom f1 is Element of K6(M)

dom ||.f1.|| is Element of K6(M)

dom (|.f2.| (#) ||.f1.||) is Element of K6(M)

X is Element of M

||.(M,V,f1,f2).|| . X is V11() real ext-real set

(M,V,f1,f2) /. X is Element of the U1 of V

||.((M,V,f1,f2) /. X).|| is V11() real ext-real Element of REAL

f1 /. X is Element of the U1 of V

f2 * (f1 /. X) is Element of the U1 of V

||.(f2 * (f1 /. X)).|| is V11() real ext-real Element of REAL

||.(f1 /. X).|| is V11() real ext-real Element of REAL

|.f2.| * ||.(f1 /. X).|| is V11() real ext-real Element of REAL

||.f1.|| . X is V11() real ext-real set

|.f2.| * (||.f1.|| . X) is V11() real ext-real Element of REAL

(|.f2.| (#) ||.f1.||) . X is V11() real ext-real set

M is non empty set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

- f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,f1,(- 1r)) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

dom (- f1) is Element of K6(M)

K6(M) is set

dom f1 is Element of K6(M)

dom (M,V,f1,(- 1r)) is Element of K6(M)

f2 is Element of M

(- f1) /. f2 is Element of the U1 of V

f1 /. f2 is Element of the U1 of V

- (f1 /. f2) is Element of the U1 of V

(- 1r) * (f1 /. f2) is Element of the U1 of V

(M,V,f1,(- 1r)) /. f2 is Element of the U1 of V

M is non empty set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

- f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

- (- f1) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,(- f1),(- 1r)) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,f1,(- 1r)) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,(M,V,f1,(- 1r)),(- 1r)) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(- 1r) * (- 1r) is V11() Element of COMPLEX

(M,V,f1,((- 1r) * (- 1r))) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

M is non empty set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f2 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f1 - f2 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

- f2 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,f1,(- f2)) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

dom (f1 - f2) is Element of K6(M)

K6(M) is set

dom f1 is Element of K6(M)

dom f2 is Element of K6(M)

(dom f1) /\ (dom f2) is Element of K6(M)

dom (- f2) is Element of K6(M)

(dom f1) /\ (dom (- f2)) is Element of K6(M)

dom (M,V,f1,(- f2)) is Element of K6(M)

X is Element of M

(M,V,f1,(- f2)) /. X is Element of the U1 of V

f1 /. X is Element of the U1 of V

(- f2) /. X is Element of the U1 of V

(f1 /. X) + ((- f2) /. X) is Element of the U1 of V

f2 /. X is Element of the U1 of V

(f1 /. X) - (f2 /. X) is Element of the U1 of V

- (f2 /. X) is Element of the U1 of V

K164(V,(f1 /. X),(- (f2 /. X))) is Element of the U1 of V

(f1 - f2) /. X is Element of the U1 of V

M is non empty set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f2 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

- f2 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f1 - (- f2) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,f1,f2) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

- (- f2) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,f1,(- (- f2))) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

M is non empty set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f2 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,f1,f2) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

X is set

(M,V,f1,f2) | X is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f1 | X is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f2 | X is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,(f1 | X),(f2 | X)) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,(f1 | X),f2) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

(M,V,f1,(f2 | X)) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

Y is Element of M

dom ((M,V,f1,f2) | X) is Element of K6(M)

K6(M) is set

dom (M,V,f1,f2) is Element of K6(M)

(dom (M,V,f1,f2)) /\ X is Element of K6(M)

dom f1 is Element of K6(M)

dom f2 is Element of K6(M)

(dom f1) /\ (dom f2) is Element of K6(M)

(dom f2) /\ X is Element of K6(M)

dom (f2 | X) is Element of K6(M)

(dom f1) /\ X is Element of K6(M)

dom (f1 | X) is Element of K6(M)

(dom (f1 | X)) /\ (dom (f2 | X)) is Element of K6(M)

dom (M,V,(f1 | X),(f2 | X)) is Element of K6(M)

((M,V,f1,f2) | X) /. Y is Element of the U1 of V

(M,V,f1,f2) /. Y is Element of the U1 of V

f1 /. Y is Element of the U1 of V

f2 /. Y is Element of the U1 of V

(f1 /. Y) + (f2 /. Y) is Element of the U1 of V

(f1 | X) /. Y is Element of the U1 of V

((f1 | X) /. Y) + (f2 /. Y) is Element of the U1 of V

(f2 | X) /. Y is Element of the U1 of V

((f1 | X) /. Y) + ((f2 | X) /. Y) is Element of the U1 of V

(M,V,(f1 | X),(f2 | X)) /. Y is Element of the U1 of V

X /\ X is set

((dom f1) /\ (dom f2)) /\ (X /\ X) is Element of K6(M)

(dom f2) /\ (X /\ X) is Element of K6(M)

(dom f1) /\ ((dom f2) /\ (X /\ X)) is Element of K6(M)

((dom f2) /\ X) /\ X is Element of K6(M)

(dom f1) /\ (((dom f2) /\ X) /\ X) is Element of K6(M)

X /\ (dom (f2 | X)) is Element of K6(M)

(dom f1) /\ (X /\ (dom (f2 | X))) is Element of K6(M)

((dom f1) /\ X) /\ (dom (f2 | X)) is Element of K6(M)

Y is Element of M

(dom (f1 | X)) /\ (dom f2) is Element of K6(M)

dom (M,V,(f1 | X),f2) is Element of K6(M)

((M,V,f1,f2) | X) /. Y is Element of the U1 of V

(M,V,f1,f2) /. Y is Element of the U1 of V

f1 /. Y is Element of the U1 of V

f2 /. Y is Element of the U1 of V

(f1 /. Y) + (f2 /. Y) is Element of the U1 of V

(f1 | X) /. Y is Element of the U1 of V

((f1 | X) /. Y) + (f2 /. Y) is Element of the U1 of V

(M,V,(f1 | X),f2) /. Y is Element of the U1 of V

((dom f1) /\ (dom f2)) /\ X is Element of K6(M)

((dom f1) /\ X) /\ (dom f2) is Element of K6(M)

Y is Element of M

(dom f1) /\ (dom (f2 | X)) is Element of K6(M)

dom (M,V,f1,(f2 | X)) is Element of K6(M)

((M,V,f1,f2) | X) /. Y is Element of the U1 of V

(M,V,f1,f2) /. Y is Element of the U1 of V

f1 /. Y is Element of the U1 of V

f2 /. Y is Element of the U1 of V

(f1 /. Y) + (f2 /. Y) is Element of the U1 of V

(f2 | X) /. Y is Element of the U1 of V

(f1 /. Y) + ((f2 | X) /. Y) is Element of the U1 of V

(M,V,f1,(f2 | X)) /. Y is Element of the U1 of V

(dom f1) /\ ((dom f2) /\ X) is Element of K6(M)

M is non empty set

K7(M,COMPLEX) is V119() set

K6(K7(M,COMPLEX)) is set

V is non empty V68() Abelian add-associative right_zeroed V103() V104() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the U1 of V is non empty set

K7(M, the U1 of V) is set

K6(K7(M, the U1 of V)) is set

f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))

f2 is set

f1