:: 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 | 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,f1) | f2 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))
X | f2 is V13() V16(M) V17( COMPLEX ) Function-like V119() Element of K6(K7(M,COMPLEX))
(M,V,(X | f2),(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 | 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 | f2)) 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,X,f1) | f2) is Element of K6(M)
K6(M) is set
dom (M,V,X,f1) is Element of K6(M)
(dom (M,V,X,f1)) /\ f2 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 X) /\ f2 is Element of K6(M)
dom (X | f2) is Element of K6(M)
(X | f2) /. Y is V11() Element of COMPLEX
(X | f2) . Y is V11() set
X . Y is V11() set
X /. Y is V11() Element of COMPLEX
(dom f1) /\ f2 is Element of K6(M)
dom (f1 | f2) is Element of K6(M)
(dom (X | f2)) /\ (dom (f1 | f2)) is Element of K6(M)
dom (M,V,(X | f2),(f1 | f2)) is Element of K6(M)
((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
f1 /. Y is Element of the U1 of V
(X /. Y) * (f1 /. Y) is Element of the U1 of V
(f1 | f2) /. Y is Element of the U1 of V
((X | f2) /. Y) * ((f1 | f2) /. Y) is Element of the U1 of V
(M,V,(X | f2),(f1 | f2)) /. Y is Element of the U1 of V
f2 /\ f2 is set
((dom X) /\ (dom f1)) /\ (f2 /\ f2) is Element of K6(M)
(dom f1) /\ (f2 /\ f2) is Element of K6(M)
(dom X) /\ ((dom f1) /\ (f2 /\ f2)) is Element of K6(M)
((dom f1) /\ f2) /\ f2 is Element of K6(M)
(dom X) /\ (((dom f1) /\ f2) /\ f2) is Element of K6(M)
f2 /\ (dom (f1 | f2)) is Element of K6(M)
(dom X) /\ (f2 /\ (dom (f1 | f2))) is Element of K6(M)
((dom X) /\ f2) /\ (dom (f1 | f2)) is Element of K6(M)
Y is Element of M
(X | f2) /. Y is V11() Element of COMPLEX
(X | f2) . Y is V11() set
X . Y is V11() set
(dom (X | f2)) /\ (dom f1) is Element of K6(M)
dom (M,V,(X | f2),f1) is Element of K6(M)
((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
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
((X | f2) /. Y) * (f1 /. Y) is Element of the U1 of V
(M,V,(X | f2),f1) /. Y is Element of the U1 of V
((dom X) /\ (dom f1)) /\ f2 is Element of K6(M)
((dom X) /\ f2) /\ (dom f1) is Element of K6(M)
Y is Element of M
(dom X) /\ (dom (f1 | f2)) is Element of K6(M)
dom (M,V,X,(f1 | f2)) is Element of K6(M)
((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
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
(f1 | f2) /. Y is Element of the U1 of V
(X /. Y) * ((f1 | f2) /. Y) is Element of the U1 of V
(M,V,X,(f1 | f2)) /. Y is Element of the U1 of V
(dom X) /\ ((dom f1) /\ f2) 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))
- 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 set
(- f1) | 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))
- (f1 | 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( REAL ) Function-like V119() V120() V121() Element of K6(K7(M,REAL))
||.(f1 | f2).|| is V13() V16(M) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(M,REAL))
X is Element of M
dom ((- f1) | f2) is Element of K6(M)
K6(M) is set
dom (- f1) is Element of K6(M)
(dom (- f1)) /\ f2 is Element of K6(M)
dom f1 is Element of K6(M)
(dom f1) /\ f2 is Element of K6(M)
dom (f1 | f2) is Element of K6(M)
dom (- (f1 | f2)) is Element of K6(M)
((- f1) | f2) /. X is Element of the U1 of V
(- f1) /. X is Element of the U1 of V
f1 /. X is Element of the U1 of V
- (f1 /. X) is Element of the U1 of V
(f1 | f2) /. X is Element of the U1 of V
- ((f1 | f2) /. X) is Element of the U1 of V
(- (f1 | f2)) /. X is Element of the U1 of V
dom (||.f1.|| | f2) is Element of K6(M)
dom ||.f1.|| is Element of K6(M)
(dom ||.f1.||) /\ f2 is Element of K6(M)
dom ||.(f1 | f2).|| is Element of K6(M)
X is Element of M
(||.f1.|| | f2) . X is V11() real ext-real set
||.f1.|| . X is V11() real ext-real set
f1 /. X is Element of the U1 of V
||.(f1 /. X).|| is V11() real ext-real Element of REAL
(f1 | f2) /. X is Element of the U1 of V
||.((f1 | f2) /. X).|| is V11() real ext-real Element of REAL
||.(f1 | f2).|| . 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))
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 set
(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))
(f1 | X) - (f2 | X) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))
(f1 | X) - f2 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))
- 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,V,f1,(- f2)) | 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))
- (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))
(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 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
(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))
(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))
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 f1) /\ X is Element of K6(M)
dom (f1 | X) 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 * (f1 /. Y) is Element of the U1 of V
(f1 | X) /. Y is Element of the U1 of V
f2 * ((f1 | X) /. Y) is Element of the U1 of 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))
(M,V,f1,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))
dom f1 is Element of K6(M)
K6(M) is set
dom f2 is Element of K6(M)
dom (M,V,f1,f2) is Element of K6(M)
M /\ M is set
dom (M,V,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 f1 is Element of K6(M)
K6(M) is set
dom f2 is Element of K6(M)
dom (f1 - f2) is Element of K6(M)
M /\ M is set
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)
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))
(M,V,f2,f1) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))
dom f2 is Element of K6(M)
K6(M) is set
dom f1 is Element of K6(M)
dom (M,V,f2,f1) is Element of K6(M)
M /\ M is set
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)
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
(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 is Element of K6(M)
K6(M) is set
dom (M,V,f1,f2) is Element of K6(M)
dom (M,V,f1,f2) is Element of K6(M)
K6(M) is set
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))
- 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 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
dom f1 is Element of K6(M)
K6(M) is set
dom ||.f1.|| is Element of K6(M)
dom ||.f1.|| is Element of K6(M)
K6(M) is set
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))
(M,V,f1,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 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
(f1 - 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
dom (M,V,f1,f2) is Element of K6(M)
K6(M) is set
dom (f1 - f2) 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 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))
X is Element of M
(M,V,f2,f1) /. X is Element of the U1 of V
f1 /. X is Element of the U1 of V
f2 /. X is V11() Element of COMPLEX
(f2 /. X) * (f1 /. X) is Element of the U1 of V
dom (M,V,f2,f1) is Element of K6(M)
K6(M) is 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))
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 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 * (f1 /. X) is Element of the U1 of V
dom (M,V,f1,f2) is Element of K6(M)
K6(M) is 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))
||.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 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
||.f1.|| . f2 is V11() real ext-real set
||.(f1 /. f2).|| is V11() real ext-real Element of REAL
dom (- f1) is Element of K6(M)
K6(M) is set
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
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 set
X is set
dom f1 is Element of K6(M)
K6(M) is set
X /\ (dom f1) is Element of K6(M)
Y is V11() real ext-real Element of REAL
f2 /\ (dom f1) is Element of K6(M)
c is Element of M
f1 /. c is Element of the U1 of V
||.(f1 /. c).|| is V11() real ext-real Element of REAL
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))
dom f1 is Element of K6(M)
K6(M) is set
f2 is set
f2 /\ (dom f1) is Element of K6(M)
X is Element of M
f1 /. X is Element of the U1 of V
||.(f1 /. X).|| is V11() real ext-real Element of REAL
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,0c) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))
f2 is set
|.0c.| is V11() real ext-real Element of REAL
Y is Element of M
f1 /. Y is Element of the U1 of V
||.(f1 /. Y).|| is V11() real ext-real Element of REAL
|.0c.| * ||.(f1 /. Y).|| is V11() real ext-real Element of REAL
0c * (f1 /. Y) is Element of the U1 of V
||.(0c * (f1 /. Y)).|| is V11() real ext-real Element of REAL
dom (M,V,f1,0c) is Element of K6(M)
K6(M) is set
f2 /\ (dom (M,V,f1,0c)) is Element of K6(M)
(M,V,f1,0c) /. Y is Element of the U1 of V
||.((M,V,f1,0c) /. Y).|| is V11() real ext-real Element of REAL
X is natural V11() real V114() V115() ext-real V129() V130() V131() V132() V133() V134() Element of NAT
X is natural V11() real V114() V115() ext-real V129() V130() V131() V132() V133() V134() Element of NAT
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
(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
dom f1 is Element of K6(M)
K6(M) is set
X /\ (dom f1) is Element of K6(M)
Y is V11() real ext-real Element of REAL
|.f2.| is V11() real ext-real Element of REAL
abs Y is V11() real ext-real Element of REAL
|.f2.| * (abs Y) is V11() real ext-real Element of REAL
dom (M,V,f1,f2) is Element of K6(M)
X /\ (dom (M,V,f1,f2)) is Element of K6(M)
c is V11() real ext-real Element of REAL
r2 is Element of M
(M,V,f1,f2) /. r2 is Element of the U1 of V
||.((M,V,f1,f2) /. r2).|| is V11() real ext-real Element of REAL
f1 /. r2 is Element of the U1 of V
||.(f1 /. r2).|| is V11() real ext-real Element of REAL
|.f2.| * ||.(f1 /. r2).|| is V11() real ext-real Element of REAL
f2 * (f1 /. r2) is Element of the U1 of V
||.(f2 * (f1 /. r2)).|| is V11() real ext-real Element of REAL
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
- 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.|| | f2 is V13() V16(M) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(M,REAL))
dom f1 is Element of K6(M)
K6(M) is set
f2 /\ (dom f1) is Element of K6(M)
X is V11() real ext-real Element of REAL
Y is set
dom ||.f1.|| is Element of K6(M)
f2 /\ (dom ||.f1.||) is Element of K6(M)
f1 /. Y is Element of the U1 of V
||.(f1 /. Y).|| is V11() real ext-real Element of REAL
abs ||.(f1 /. Y).|| is V11() real ext-real Element of REAL
||.f1.|| . Y is V11() real ext-real set
abs (||.f1.|| . Y) is V11() real ext-real Element of REAL
(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 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
Y is set
X /\ Y is set
dom f1 is Element of K6(M)
K6(M) is set
X /\ (dom f1) is Element of K6(M)
c is V11() real ext-real Element of REAL
dom f2 is Element of K6(M)
Y /\ (dom f2) is Element of K6(M)
r2 is V11() real ext-real Element of REAL
c + r2 is V11() real ext-real Element of REAL
dom (M,V,f1,f2) is Element of K6(M)
(X /\ Y) /\ (dom (M,V,f1,f2)) is Element of K6(M)
c is V11() real ext-real Element of REAL
r is Element of M
(M,V,f1,f2) /. r is Element of the U1 of V
||.((M,V,f1,f2) /. r).|| is V11() real ext-real Element of REAL
(dom f1) /\ (dom f2) is Element of K6(M)
f2 /. r is Element of the U1 of V
||.(f2 /. r).|| is V11() real ext-real Element of REAL
f1 /. r is Element of the U1 of V
||.(f1 /. r).|| is V11() real ext-real Element of REAL
(f1 /. r) + (f2 /. r) is Element of the U1 of V
||.((f1 /. r) + (f2 /. r)).|| is V11() real ext-real Element of REAL
||.(f1 /. r).|| + ||.(f2 /. r).|| 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
f1 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))
f2 is set
X is set
f2 /\ X is set
Y is V13() V16(M) V17( COMPLEX ) Function-like V119() Element of K6(K7(M,COMPLEX))
Y | f2 is V13() V16(M) V17( COMPLEX ) Function-like V119() Element of K6(K7(M,COMPLEX))
(M,V,Y,f1) 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)
K6(M) is set
f2 /\ (dom Y) is Element of K6(M)
c is V11() real ext-real set
dom f1 is Element of K6(M)
X /\ (dom f1) is Element of K6(M)
r2 is V11() real ext-real Element of REAL
c is V11() real ext-real Element of REAL
c * r2 is V11() real ext-real Element of REAL
c is Element of M
dom (M,V,Y,f1) is Element of K6(M)
(f2 /\ X) /\ (dom (M,V,Y,f1)) is Element of K6(M)
(dom Y) /\ (dom f1) is Element of K6(M)
Y /. c is V11() Element of COMPLEX
|.(Y /. c).| is V11() real ext-real Element of REAL
f1 /. c is Element of the U1 of V
||.(f1 /. c).|| is V11() real ext-real Element of REAL
|.(Y /. c).| * ||.(f1 /. c).|| is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
(Y /. c) * (f1 /. c) is Element of the U1 of V
||.((Y /. c) * (f1 /. c)).|| is V11() real ext-real Element of REAL
(M,V,Y,f1) /. c is Element of the U1 of V
||.((M,V,Y,f1) /. c).|| is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
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 set
Y is set
X /\ Y is set
- 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 set
X is set
f2 \/ X is set
dom f1 is Element of K6(M)
K6(M) is set
f2 /\ (dom f1) is Element of K6(M)
Y is V11() real ext-real Element of REAL
X /\ (dom f1) is Element of K6(M)
c is V11() real ext-real Element of REAL
abs Y is V11() real ext-real Element of REAL
abs c is V11() real ext-real Element of REAL
(abs Y) + (abs c) is V11() real ext-real Element of REAL
(f2 \/ X) /\ (dom f1) is Element of K6(M)
r2 is V11() real ext-real Element of REAL
c is Element of M
f1 /. c is Element of the U1 of V
||.(f1 /. c).|| is V11() real ext-real Element of REAL
||.(f1 /. c).|| + 0 is V11() real ext-real Element of REAL
0 + ||.(f1 /. c).|| is V11() real ext-real Element of REAL
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))
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
f1 | X is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))
Y is set
f2 | Y is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))
X /\ Y is set
(M,V,f1,f2) | (X /\ Y) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))
(f1 - f2) | (X /\ Y) 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
X /\ (dom f1) is Element of K6(M)
c is Element of the U1 of V
dom f2 is Element of K6(M)
Y /\ (dom f2) is Element of K6(M)
r2 is Element of the U1 of V
c is Element of M
dom (M,V,f1,f2) is Element of K6(M)
(X /\ Y) /\ (dom (M,V,f1,f2)) is Element of K6(M)
(dom f1) /\ (dom f2) is Element of K6(M)
(M,V,f1,f2) /. c is Element of the U1 of V
f1 /. c is Element of the U1 of V
f2 /. c is Element of the U1 of V
(f1 /. c) + (f2 /. c) is Element of the U1 of V
c + (f2 /. c) is Element of the U1 of V
c + r2 is Element of the U1 of V
c is Element of M
dom (f1 - f2) is Element of K6(M)
(X /\ Y) /\ (dom (f1 - f2)) is Element of K6(M)
(f1 - f2) /. c is Element of the U1 of V
f1 /. c is Element of the U1 of V
f2 /. c is Element of the U1 of V
(f1 /. c) - (f2 /. c) is Element of the U1 of V
- (f2 /. c) is Element of the U1 of V
K164(V,(f1 /. c),(- (f2 /. c))) is Element of the U1 of V
c - (f2 /. c) is Element of the U1 of V
K164(V,c,(- (f2 /. c))) is Element of the U1 of V
c - r2 is Element of the U1 of V
- r2 is Element of the U1 of V
K164(V,c,(- r2)) 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 set
X is set
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 set
Y is V13() V16(M) V17( COMPLEX ) Function-like V119() Element of K6(K7(M,COMPLEX))
Y | f2 is V13() V16(M) V17( COMPLEX ) Function-like V119() Element of K6(K7(M,COMPLEX))
(M,V,Y,f1) is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))
(M,V,Y,f1) | (f2 /\ X) 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)
K6(M) is set
f2 /\ (dom Y) is Element of K6(M)
c is V11() Element of COMPLEX
dom f1 is Element of K6(M)
X /\ (dom f1) is Element of K6(M)
r2 is Element of the U1 of V
c is Element of M
dom (M,V,Y,f1) is Element of K6(M)
(f2 /\ X) /\ (dom (M,V,Y,f1)) is Element of K6(M)
(dom Y) /\ (dom f1) is Element of K6(M)
Y /. c is V11() Element of COMPLEX
Y . c is V11() set
(M,V,Y,f1) /. c is Element of the U1 of V
f1 /. c is Element of the U1 of V
(Y /. c) * (f1 /. c) is Element of the U1 of V
c * (f1 /. c) is Element of the U1 of V
c * r2 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
(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
f1 | 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 is Element of K6(M)
K6(M) is set
X /\ (dom f1) is Element of K6(M)
Y is Element of the U1 of V
c is Element of M
dom (M,V,f1,f2) is Element of K6(M)
X /\ (dom (M,V,f1,f2)) is Element of K6(M)
(M,V,f1,f2) /. 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
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))
||.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 is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))
f2 is set
f1 | 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( REAL ) Function-like V119() V120() V121() Element of K6(K7(M,REAL))
(- f1) | f2 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
f2 /\ (dom f1) is Element of K6(M)
X is Element of the U1 of V
Y is Element of M
dom ||.f1.|| is Element of K6(M)
f2 /\ (dom ||.f1.||) is Element of K6(M)
||.f1.|| . Y is V11() real ext-real set
f1 /. Y is Element of the U1 of V
||.(f1 /. Y).|| is V11() real ext-real Element of REAL
||.X.|| is V11() real ext-real Element of REAL
- X is Element of the U1 of V
c is Element of M
dom (- f1) is Element of K6(M)
f2 /\ (dom (- f1)) is Element of K6(M)
f1 /. c is Element of the U1 of V
- (f1 /. c) is Element of the U1 of V
Y is Element of the U1 of V
(- f1) /. c is Element of the U1 of V
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 set
f1 | f2 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
f2 /\ (dom f1) is Element of K6(M)
X is Element of the U1 of V
||.X.|| is V11() real ext-real Element of REAL
c is Element of M
f1 /. c is Element of the U1 of V
||.(f1 /. c).|| is V11() real ext-real Element of REAL
Y is V11() real ext-real Element of REAL
Y is V11() real ext-real Element of REAL
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( 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 set
f1 | 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( REAL ) Function-like V119() V120() V121() Element of K6(K7(M,REAL))
X is V11() Element of COMPLEX
(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,f1,X) | 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 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
Y is set
f2 | Y is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))
X /\ Y is 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))
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))
X is set
Y is set
f2 | Y is V13() V16(M) V17( the U1 of V) Function-like Element of K6(K7(M, the U1 of V))
X /\ Y is set
- 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))
- 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))
Y /\ X is set