:: VFUNCT_1 semantic presentation

REAL is non empty V46() V47() V48() V52() V53() set
NAT is V46() V47() V48() V49() V50() V51() V52() Element of K19(REAL)
K19(REAL) is set
COMPLEX is non empty V46() V52() V53() set
{} is set
the empty V46() V47() V48() V49() V50() V51() V52() set is empty V46() V47() V48() V49() V50() V51() V52() set
1 is non empty ext-real natural V25() real V46() V47() V48() V49() V50() V51() V131() V132() Element of NAT
{{},1} is set
omega is V46() V47() V48() V49() V50() V51() V52() set
K19(omega) is set
K19(NAT) is set
K20(NAT,REAL) is V36() V37() V38() set
K19(K20(NAT,REAL)) is set
RAT is non empty V46() V47() V48() V49() V52() V53() set
INT is non empty V46() V47() V48() V49() V50() V52() V53() set
0 is ext-real natural V25() real V46() V47() V48() V49() V50() V51() V131() V132() Element of NAT
- 1 is ext-real V25() real Element of REAL
X is non empty set
Y is non empty addLoopStr
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
V is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom C is Element of K19(X)
K19(X) is set
dom V is Element of K19(X)
(dom C) /\ (dom V) is Element of K19(X)
f2 is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom f2 is Element of K19(X)
c is Element of X
f2 /. c is Element of the U1 of Y
C /. c is Element of the U1 of Y
V /. c is Element of the U1 of Y
(C /. c) + (V /. c) is Element of the U1 of Y
f2 is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom f2 is Element of K19(X)
c is Element of X
f2 /. c is Element of the U1 of Y
C /. c is Element of the U1 of Y
V /. c is Element of the U1 of Y
(C /. c) - (V /. c) is Element of the U1 of Y
- (V /. c) is Element of the U1 of Y
(C /. c) + (- (V /. c)) is Element of the U1 of Y
X is non empty set
Y is non empty addLoopStr
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() non empty total V30(X, the U1 of Y) Element of K19(K20(X, the U1 of Y))
V is V1() V4(X) V5( the U1 of Y) V6() non empty total V30(X, the U1 of Y) Element of K19(K20(X, the U1 of Y))
(X,Y,C,V) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom (X,Y,C,V) is Element of K19(X)
K19(X) is set
dom C is Element of K19(X)
dom V is Element of K19(X)
(dom C) /\ (dom V) is Element of K19(X)
X /\ (dom V) is Element of K19(X)
X /\ X is set
(X,Y,C,V) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom (X,Y,C,V) is Element of K19(X)
K19(X) is set
dom C is Element of K19(X)
dom V is Element of K19(X)
(dom C) /\ (dom V) is Element of K19(X)
X /\ (dom V) is Element of K19(X)
X /\ X is set
X is non empty set
K20(X,REAL) is V36() V37() V38() set
K19(K20(X,REAL)) is set
Y is non empty RLSStruct
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
V is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
C is V1() V4(X) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(X,REAL))
dom C is Element of K19(X)
K19(X) is set
dom V is Element of K19(X)
(dom C) /\ (dom V) is Element of K19(X)
f2 is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom f2 is Element of K19(X)
c is Element of X
f2 /. c is Element of the U1 of Y
V /. c is Element of the U1 of Y
C . c is ext-real V25() real Element of REAL
(C . c) * (V /. c) is Element of the U1 of Y
X is non empty set
K20(X,REAL) is V36() V37() V38() set
K19(K20(X,REAL)) is set
Y is non empty RLSStruct
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( REAL ) V6() non empty total V30(X, REAL ) V36() V37() V38() Element of K19(K20(X,REAL))
V is V1() V4(X) V5( the U1 of Y) V6() non empty total V30(X, the U1 of Y) Element of K19(K20(X, the U1 of Y))
(X,Y,C,V) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom (X,Y,C,V) is Element of K19(X)
K19(X) is set
dom C is Element of K19(X)
dom V is Element of K19(X)
(dom C) /\ (dom V) is Element of K19(X)
X /\ (dom V) is Element of K19(X)
X /\ X is set
X is non empty set
Y is non empty RLSStruct
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
V is ext-real V25() real Element of REAL
dom C is Element of K19(X)
K19(X) is set
f1 is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom f1 is Element of K19(X)
f2 is Element of X
f1 /. f2 is Element of the U1 of Y
C /. f2 is Element of the U1 of Y
V * (C /. f2) is Element of the U1 of Y
X is non empty set
Y is non empty RLSStruct
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() non empty total V30(X, the U1 of Y) Element of K19(K20(X, the U1 of Y))
V is ext-real V25() real Element of REAL
(X,Y,C,V) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom (X,Y,C,V) is Element of K19(X)
K19(X) is set
dom C is Element of K19(X)
X is non empty set
Y is non empty addLoopStr
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom C is Element of K19(X)
K19(X) is set
V is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom V is Element of K19(X)
f1 is Element of X
V /. f1 is Element of the U1 of Y
C /. f1 is Element of the U1 of Y
- (C /. f1) is Element of the U1 of Y
X is non empty set
Y is non empty addLoopStr
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() non empty total V30(X, the U1 of Y) Element of K19(K20(X, the U1 of Y))
(X,Y,C) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom (X,Y,C) is Element of K19(X)
K19(X) is set
dom C is Element of K19(X)
{0} is V46() V47() V48() V49() V50() V51() set
X is non empty set
K20(X,REAL) is V36() V37() V38() set
K19(K20(X,REAL)) is set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
0. Y is V72(Y) left_complementable right_complementable complementable Element of the U1 of Y
{(0. Y)} is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom C is Element of K19(X)
K19(X) is set
C " {(0. Y)} is Element of K19(X)
(dom C) \ (C " {(0. Y)}) is Element of K19(X)
V is V1() V4(X) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(X,REAL))
(X,Y,V,C) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom (X,Y,V,C) is Element of K19(X)
(X,Y,V,C) " {(0. Y)} is Element of K19(X)
(dom (X,Y,V,C)) \ ((X,Y,V,C) " {(0. Y)}) is Element of K19(X)
dom V is Element of K19(X)
V " {0} is Element of K19(X)
(dom V) \ (V " {0}) is Element of K19(X)
((dom V) \ (V " {0})) /\ ((dom C) \ (C " {(0. Y)})) is Element of K19(X)
f1 is set
f2 is Element of X
(X,Y,V,C) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
C /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
V . f2 is ext-real V25() real Element of REAL
(V . f2) * (C /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(dom V) /\ (dom C) is Element of K19(X)
f1 is set
f2 is Element of X
C /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
(dom V) /\ (dom C) is Element of K19(X)
V . f2 is ext-real V25() real Element of REAL
(V . f2) * (C /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,V,C) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
X is non empty set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
0. Y is V72(Y) left_complementable right_complementable complementable Element of the U1 of Y
{(0. Y)} is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
||.C.|| is V1() V4(X) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(X,REAL))
K20(X,REAL) is V36() V37() V38() set
K19(K20(X,REAL)) is set
||.C.|| " {0} is Element of K19(X)
K19(X) is set
C " {(0. Y)} is Element of K19(X)
(X,Y,C) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C) " {(0. Y)} is Element of K19(X)
V is Element of X
dom ||.C.|| is Element of K19(X)
||.C.|| . V is ext-real V25() real Element of REAL
C /. V is left_complementable right_complementable complementable Element of the U1 of Y
||.(C /. V).|| is ext-real non negative V25() real Element of REAL
the U8 of Y is V1() V4( the U1 of Y) V5( REAL ) V6() non empty total V30( the U1 of Y, REAL ) V36() V37() V38() Element of K19(K20( the U1 of Y,REAL))
K20( the U1 of Y,REAL) is V36() V37() V38() set
K19(K20( the U1 of Y,REAL)) is set
the U8 of Y . (C /. V) is ext-real V25() real Element of REAL
dom C is Element of K19(X)
dom C is Element of K19(X)
dom ||.C.|| is Element of K19(X)
C /. V is left_complementable right_complementable complementable Element of the U1 of Y
||.(C /. V).|| is ext-real non negative V25() real Element of REAL
the U8 of Y is V1() V4( the U1 of Y) V5( REAL ) V6() non empty total V30( the U1 of Y, REAL ) V36() V37() V38() Element of K19(K20( the U1 of Y,REAL))
K20( the U1 of Y,REAL) is V36() V37() V38() set
K19(K20( the U1 of Y,REAL)) is set
the U8 of Y . (C /. V) is ext-real V25() real Element of REAL
||.C.|| . V is ext-real V25() real Element of REAL
V is Element of X
dom (X,Y,C) is Element of K19(X)
(X,Y,C) /. V is left_complementable right_complementable complementable Element of the U1 of Y
C /. V is left_complementable right_complementable complementable Element of the U1 of Y
- (C /. V) is left_complementable right_complementable complementable Element of the U1 of Y
- (- (C /. V)) is left_complementable right_complementable complementable Element of the U1 of Y
- (0. Y) is left_complementable right_complementable complementable Element of the U1 of Y
dom (X,Y,C) is Element of K19(X)
C /. V is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,C) /. V is left_complementable right_complementable complementable Element of the U1 of Y
- (0. Y) is left_complementable right_complementable complementable Element of the U1 of Y
X is non empty set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
0. Y is V72(Y) left_complementable right_complementable complementable Element of the U1 of Y
{(0. Y)} is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
C " {(0. Y)} is Element of K19(X)
K19(X) is set
V is ext-real V25() real Element of REAL
(X,Y,C,V) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C,V) " {(0. Y)} is Element of K19(X)
f1 is Element of X
dom (X,Y,C,V) is Element of K19(X)
(X,Y,C,V) /. f1 is left_complementable right_complementable complementable Element of the U1 of Y
C /. f1 is left_complementable right_complementable complementable Element of the U1 of Y
V * (C /. f1) is left_complementable right_complementable complementable Element of the U1 of Y
V * (0. Y) is left_complementable right_complementable complementable Element of the U1 of Y
dom C is Element of K19(X)
dom C is Element of K19(X)
dom (X,Y,C,V) is Element of K19(X)
C /. f1 is left_complementable right_complementable complementable Element of the U1 of Y
V * (C /. f1) is left_complementable right_complementable complementable Element of the U1 of Y
V * (0. Y) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,C,V) /. f1 is left_complementable right_complementable complementable Element of the U1 of Y
X is non empty set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
V is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C,V) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,V,C) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom (X,Y,C,V) is Element of K19(X)
K19(X) is set
dom V is Element of K19(X)
dom C is Element of K19(X)
(dom V) /\ (dom C) is Element of K19(X)
dom (X,Y,V,C) is Element of K19(X)
f1 is Element of X
(X,Y,C,V) /. f1 is left_complementable right_complementable complementable Element of the U1 of Y
V /. f1 is left_complementable right_complementable complementable Element of the U1 of Y
C /. f1 is left_complementable right_complementable complementable Element of the U1 of Y
(V /. f1) + (C /. f1) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,V,C) /. f1 is left_complementable right_complementable complementable Element of the U1 of Y
X is non empty set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
f1 is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
f2 is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,f1,f2) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,f2,f1) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
X is non empty set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
V is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C,V) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
f1 is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,(X,Y,C,V),f1) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,V,f1) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C,(X,Y,V,f1)) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom (X,Y,(X,Y,C,V),f1) is Element of K19(X)
K19(X) is set
dom (X,Y,C,V) is Element of K19(X)
dom f1 is Element of K19(X)
(dom (X,Y,C,V)) /\ (dom f1) is Element of K19(X)
dom C is Element of K19(X)
dom V is Element of K19(X)
(dom C) /\ (dom V) is Element of K19(X)
((dom C) /\ (dom V)) /\ (dom f1) is Element of K19(X)
(dom V) /\ (dom f1) is Element of K19(X)
(dom C) /\ ((dom V) /\ (dom f1)) is Element of K19(X)
dom (X,Y,V,f1) is Element of K19(X)
(dom C) /\ (dom (X,Y,V,f1)) is Element of K19(X)
dom (X,Y,C,(X,Y,V,f1)) is Element of K19(X)
f2 is Element of X
(X,Y,(X,Y,C,V),f1) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,C,V) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
f1 /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
((X,Y,C,V) /. f2) + (f1 /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
C /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
V /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
(C /. f2) + (V /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
((C /. f2) + (V /. f2)) + (f1 /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(V /. f2) + (f1 /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(C /. f2) + ((V /. f2) + (f1 /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,V,f1) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
(C /. f2) + ((X,Y,V,f1) /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,C,(X,Y,V,f1)) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
X is non empty set
K20(X,REAL) is V36() V37() V38() set
K19(K20(X,REAL)) is set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(X,REAL))
V is V1() V4(X) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(X,REAL))
C (#) V is V1() V4(X) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(X,REAL))
f1 is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,(C (#) V),f1) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,V,f1) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C,(X,Y,V,f1)) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom (X,Y,(C (#) V),f1) is Element of K19(X)
K19(X) is set
dom (C (#) V) is Element of K19(X)
dom f1 is Element of K19(X)
(dom (C (#) V)) /\ (dom f1) is Element of K19(X)
dom C is Element of K19(X)
dom V is Element of K19(X)
(dom C) /\ (dom V) is Element of K19(X)
((dom C) /\ (dom V)) /\ (dom f1) is Element of K19(X)
(dom V) /\ (dom f1) is Element of K19(X)
(dom C) /\ ((dom V) /\ (dom f1)) is Element of K19(X)
dom (X,Y,V,f1) is Element of K19(X)
(dom C) /\ (dom (X,Y,V,f1)) is Element of K19(X)
dom (X,Y,C,(X,Y,V,f1)) is Element of K19(X)
f2 is Element of X
(X,Y,(C (#) V),f1) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
f1 /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
(C (#) V) . f2 is ext-real V25() real Element of REAL
((C (#) V) . f2) * (f1 /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
C . f2 is ext-real V25() real Element of REAL
V . f2 is ext-real V25() real Element of REAL
(C . f2) * (V . f2) is ext-real V25() real Element of REAL
((C . f2) * (V . f2)) * (f1 /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(V . f2) * (f1 /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(C . f2) * ((V . f2) * (f1 /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,V,f1) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
(C . f2) * ((X,Y,V,f1) /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,C,(X,Y,V,f1)) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
X is non empty set
K20(X,REAL) is V36() V37() V38() set
K19(K20(X,REAL)) is set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
V is V1() V4(X) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(X,REAL))
f1 is V1() V4(X) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(X,REAL))
V + f1 is V1() V4(X) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(X,REAL))
(X,Y,(V + f1),C) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,V,C) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,f1,C) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,(X,Y,V,C),(X,Y,f1,C)) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom (X,Y,(V + f1),C) is Element of K19(X)
K19(X) is set
dom (V + f1) is Element of K19(X)
dom C is Element of K19(X)
(dom (V + f1)) /\ (dom C) is Element of K19(X)
dom V is Element of K19(X)
dom f1 is Element of K19(X)
(dom V) /\ (dom f1) is Element of K19(X)
(dom C) /\ (dom C) is Element of K19(X)
((dom V) /\ (dom f1)) /\ ((dom C) /\ (dom C)) is Element of K19(X)
((dom V) /\ (dom f1)) /\ (dom C) is Element of K19(X)
(((dom V) /\ (dom f1)) /\ (dom C)) /\ (dom C) is Element of K19(X)
(dom V) /\ (dom C) is Element of K19(X)
((dom V) /\ (dom C)) /\ (dom f1) is Element of K19(X)
(((dom V) /\ (dom C)) /\ (dom f1)) /\ (dom C) is Element of K19(X)
(dom f1) /\ (dom C) is Element of K19(X)
((dom V) /\ (dom C)) /\ ((dom f1) /\ (dom C)) is Element of K19(X)
dom (X,Y,V,C) is Element of K19(X)
(dom (X,Y,V,C)) /\ ((dom f1) /\ (dom C)) is Element of K19(X)
dom (X,Y,f1,C) is Element of K19(X)
(dom (X,Y,V,C)) /\ (dom (X,Y,f1,C)) is Element of K19(X)
dom (X,Y,(X,Y,V,C),(X,Y,f1,C)) is Element of K19(X)
f2 is Element of X
(X,Y,(V + f1),C) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
C /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
(V + f1) . f2 is ext-real V25() real Element of REAL
((V + f1) . f2) * (C /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
V . f2 is ext-real V25() real Element of REAL
f1 . f2 is ext-real V25() real Element of REAL
(V . f2) + (f1 . f2) is ext-real V25() real Element of REAL
((V . f2) + (f1 . f2)) * (C /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(V . f2) * (C /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(f1 . f2) * (C /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
((V . f2) * (C /. f2)) + ((f1 . f2) * (C /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,V,C) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
((X,Y,V,C) /. f2) + ((f1 . f2) * (C /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,f1,C) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
((X,Y,V,C) /. f2) + ((X,Y,f1,C) /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,(X,Y,V,C),(X,Y,f1,C)) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
X is non empty set
K20(X,REAL) is V36() V37() V38() set
K19(K20(X,REAL)) is set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
V is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C,V) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
f1 is V1() V4(X) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(X,REAL))
(X,Y,f1,(X,Y,C,V)) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,f1,C) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,f1,V) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,(X,Y,f1,C),(X,Y,f1,V)) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom (X,Y,f1,(X,Y,C,V)) is Element of K19(X)
K19(X) is set
dom f1 is Element of K19(X)
dom (X,Y,C,V) is Element of K19(X)
(dom f1) /\ (dom (X,Y,C,V)) is Element of K19(X)
dom C is Element of K19(X)
dom V is Element of K19(X)
(dom C) /\ (dom V) is Element of K19(X)
(dom f1) /\ ((dom C) /\ (dom V)) is Element of K19(X)
(dom f1) /\ (dom f1) is Element of K19(X)
((dom f1) /\ (dom f1)) /\ (dom C) is Element of K19(X)
(((dom f1) /\ (dom f1)) /\ (dom C)) /\ (dom V) is Element of K19(X)
(dom f1) /\ (dom C) is Element of K19(X)
((dom f1) /\ (dom C)) /\ (dom f1) is Element of K19(X)
(((dom f1) /\ (dom C)) /\ (dom f1)) /\ (dom V) is Element of K19(X)
(dom f1) /\ (dom V) is Element of K19(X)
((dom f1) /\ (dom C)) /\ ((dom f1) /\ (dom V)) is Element of K19(X)
dom (X,Y,f1,C) is Element of K19(X)
(dom (X,Y,f1,C)) /\ ((dom f1) /\ (dom V)) is Element of K19(X)
dom (X,Y,f1,V) is Element of K19(X)
(dom (X,Y,f1,C)) /\ (dom (X,Y,f1,V)) is Element of K19(X)
dom (X,Y,(X,Y,f1,C),(X,Y,f1,V)) is Element of K19(X)
f2 is Element of X
(X,Y,f1,(X,Y,C,V)) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,C,V) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
f1 . f2 is ext-real V25() real Element of REAL
(f1 . f2) * ((X,Y,C,V) /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
C /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
V /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
(C /. f2) + (V /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(f1 . f2) * ((C /. f2) + (V /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
(f1 . f2) * (C /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(f1 . f2) * (V /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
((f1 . f2) * (C /. f2)) + ((f1 . f2) * (V /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,f1,C) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
((X,Y,f1,C) /. f2) + ((f1 . f2) * (V /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,f1,V) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
((X,Y,f1,C) /. f2) + ((X,Y,f1,V) /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,(X,Y,f1,C),(X,Y,f1,V)) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
X is non empty set
K20(X,REAL) is V36() V37() V38() set
K19(K20(X,REAL)) is set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
V is ext-real V25() real Element of REAL
f1 is V1() V4(X) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(X,REAL))
(X,Y,f1,C) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,(X,Y,f1,C),V) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
V (#) f1 is V1() V4(X) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(X,REAL))
(X,Y,(V (#) f1),C) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom (X,Y,(X,Y,f1,C),V) is Element of K19(X)
K19(X) is set
dom (X,Y,f1,C) is Element of K19(X)
dom f1 is Element of K19(X)
dom C is Element of K19(X)
(dom f1) /\ (dom C) is Element of K19(X)
dom (V (#) f1) is Element of K19(X)
(dom (V (#) f1)) /\ (dom C) is Element of K19(X)
dom (X,Y,(V (#) f1),C) is Element of K19(X)
f2 is Element of X
(X,Y,(X,Y,f1,C),V) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,f1,C) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
V * ((X,Y,f1,C) /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
C /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
f1 . f2 is ext-real V25() real Element of REAL
(f1 . f2) * (C /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
V * ((f1 . f2) * (C /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
V * (f1 . f2) is ext-real V25() real Element of REAL
(V * (f1 . f2)) * (C /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(V (#) f1) . f2 is ext-real V25() real Element of REAL
((V (#) f1) . f2) * (C /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,(V (#) f1),C) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
X is non empty set
K20(X,REAL) is V36() V37() V38() set
K19(K20(X,REAL)) is set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
V is ext-real V25() real Element of REAL
(X,Y,C,V) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
f1 is V1() V4(X) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(X,REAL))
(X,Y,f1,C) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,(X,Y,f1,C),V) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,f1,(X,Y,C,V)) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom (X,Y,(X,Y,f1,C),V) is Element of K19(X)
K19(X) is set
dom (X,Y,f1,C) is Element of K19(X)
dom f1 is Element of K19(X)
dom C is Element of K19(X)
(dom f1) /\ (dom C) is Element of K19(X)
dom (X,Y,C,V) is Element of K19(X)
(dom f1) /\ (dom (X,Y,C,V)) is Element of K19(X)
dom (X,Y,f1,(X,Y,C,V)) is Element of K19(X)
f2 is Element of X
(X,Y,(X,Y,f1,C),V) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,f1,C) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
V * ((X,Y,f1,C) /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
C /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
f1 . f2 is ext-real V25() real Element of REAL
(f1 . f2) * (C /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
V * ((f1 . f2) * (C /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
(f1 . f2) * V is ext-real V25() real Element of REAL
((f1 . f2) * V) * (C /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
V * (C /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(f1 . f2) * (V * (C /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,C,V) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
(f1 . f2) * ((X,Y,C,V) /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,f1,(X,Y,C,V)) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
X is non empty set
K20(X,REAL) is V36() V37() V38() set
K19(K20(X,REAL)) is set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
V is V1() V4(X) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(X,REAL))
f1 is V1() V4(X) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(X,REAL))
V - f1 is V1() V4(X) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(X,REAL))
(X,Y,(V - f1),C) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,V,C) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,f1,C) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,(X,Y,V,C),(X,Y,f1,C)) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom (X,Y,(V - f1),C) is Element of K19(X)
K19(X) is set
dom (V - f1) is Element of K19(X)
dom C is Element of K19(X)
(dom (V - f1)) /\ (dom C) is Element of K19(X)
dom V is Element of K19(X)
dom f1 is Element of K19(X)
(dom V) /\ (dom f1) is Element of K19(X)
(dom C) /\ (dom C) is Element of K19(X)
((dom V) /\ (dom f1)) /\ ((dom C) /\ (dom C)) is Element of K19(X)
((dom V) /\ (dom f1)) /\ (dom C) is Element of K19(X)
(((dom V) /\ (dom f1)) /\ (dom C)) /\ (dom C) is Element of K19(X)
(dom V) /\ (dom C) is Element of K19(X)
((dom V) /\ (dom C)) /\ (dom f1) is Element of K19(X)
(((dom V) /\ (dom C)) /\ (dom f1)) /\ (dom C) is Element of K19(X)
(dom f1) /\ (dom C) is Element of K19(X)
((dom V) /\ (dom C)) /\ ((dom f1) /\ (dom C)) is Element of K19(X)
dom (X,Y,V,C) is Element of K19(X)
(dom (X,Y,V,C)) /\ ((dom f1) /\ (dom C)) is Element of K19(X)
dom (X,Y,f1,C) is Element of K19(X)
(dom (X,Y,V,C)) /\ (dom (X,Y,f1,C)) is Element of K19(X)
dom (X,Y,(X,Y,V,C),(X,Y,f1,C)) is Element of K19(X)
f2 is Element of X
(X,Y,(V - f1),C) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
C /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
(V - f1) . f2 is ext-real V25() real Element of REAL
((V - f1) . f2) * (C /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
V . f2 is ext-real V25() real Element of REAL
f1 . f2 is ext-real V25() real Element of REAL
(V . f2) - (f1 . f2) is ext-real V25() real Element of REAL
((V . f2) - (f1 . f2)) * (C /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(V . f2) * (C /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(f1 . f2) * (C /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
((V . f2) * (C /. f2)) - ((f1 . f2) * (C /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
- ((f1 . f2) * (C /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
((V . f2) * (C /. f2)) + (- ((f1 . f2) * (C /. f2))) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,V,C) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
((X,Y,V,C) /. f2) - ((f1 . f2) * (C /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
((X,Y,V,C) /. f2) + (- ((f1 . f2) * (C /. f2))) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,f1,C) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
((X,Y,V,C) /. f2) - ((X,Y,f1,C) /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
- ((X,Y,f1,C) /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
((X,Y,V,C) /. f2) + (- ((X,Y,f1,C) /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,(X,Y,V,C),(X,Y,f1,C)) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
X is non empty set
K20(X,REAL) is V36() V37() V38() set
K19(K20(X,REAL)) is set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
V is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C,V) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
f1 is V1() V4(X) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(X,REAL))
(X,Y,f1,C) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,f1,V) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,(X,Y,f1,C),(X,Y,f1,V)) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,f1,(X,Y,C,V)) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom (X,Y,(X,Y,f1,C),(X,Y,f1,V)) is Element of K19(X)
K19(X) is set
dom (X,Y,f1,C) is Element of K19(X)
dom (X,Y,f1,V) is Element of K19(X)
(dom (X,Y,f1,C)) /\ (dom (X,Y,f1,V)) is Element of K19(X)
dom f1 is Element of K19(X)
dom V is Element of K19(X)
(dom f1) /\ (dom V) is Element of K19(X)
(dom (X,Y,f1,C)) /\ ((dom f1) /\ (dom V)) is Element of K19(X)
dom C is Element of K19(X)
(dom f1) /\ (dom C) is Element of K19(X)
((dom f1) /\ (dom C)) /\ ((dom f1) /\ (dom V)) is Element of K19(X)
(dom f1) /\ ((dom f1) /\ (dom C)) is Element of K19(X)
((dom f1) /\ ((dom f1) /\ (dom C))) /\ (dom V) is Element of K19(X)
(dom f1) /\ (dom f1) is Element of K19(X)
((dom f1) /\ (dom f1)) /\ (dom C) is Element of K19(X)
(((dom f1) /\ (dom f1)) /\ (dom C)) /\ (dom V) is Element of K19(X)
(dom C) /\ (dom V) is Element of K19(X)
(dom f1) /\ ((dom C) /\ (dom V)) is Element of K19(X)
dom (X,Y,C,V) is Element of K19(X)
(dom f1) /\ (dom (X,Y,C,V)) is Element of K19(X)
dom (X,Y,f1,(X,Y,C,V)) is Element of K19(X)
f2 is Element of X
(X,Y,f1,(X,Y,C,V)) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,C,V) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
f1 . f2 is ext-real V25() real Element of REAL
(f1 . f2) * ((X,Y,C,V) /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
C /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
V /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
(C /. f2) - (V /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
- (V /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(C /. f2) + (- (V /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
(f1 . f2) * ((C /. f2) - (V /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
(f1 . f2) * (C /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(f1 . f2) * (V /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
((f1 . f2) * (C /. f2)) - ((f1 . f2) * (V /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
- ((f1 . f2) * (V /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
((f1 . f2) * (C /. f2)) + (- ((f1 . f2) * (V /. f2))) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,f1,C) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
((X,Y,f1,C) /. f2) - ((f1 . f2) * (V /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
((X,Y,f1,C) /. f2) + (- ((f1 . f2) * (V /. f2))) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,f1,V) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
((X,Y,f1,C) /. f2) - ((X,Y,f1,V) /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
- ((X,Y,f1,V) /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
((X,Y,f1,C) /. f2) + (- ((X,Y,f1,V) /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,(X,Y,f1,C),(X,Y,f1,V)) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
X is non empty set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
V is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C,V) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
f1 is ext-real V25() real Element of REAL
(X,Y,(X,Y,C,V),f1) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C,f1) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,V,f1) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,(X,Y,C,f1),(X,Y,V,f1)) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom (X,Y,(X,Y,C,V),f1) is Element of K19(X)
K19(X) is set
dom (X,Y,C,V) is Element of K19(X)
dom C is Element of K19(X)
dom V is Element of K19(X)
(dom C) /\ (dom V) is Element of K19(X)
dom (X,Y,V,f1) is Element of K19(X)
(dom C) /\ (dom (X,Y,V,f1)) is Element of K19(X)
dom (X,Y,C,f1) is Element of K19(X)
(dom (X,Y,C,f1)) /\ (dom (X,Y,V,f1)) is Element of K19(X)
dom (X,Y,(X,Y,C,f1),(X,Y,V,f1)) is Element of K19(X)
f2 is Element of X
(X,Y,(X,Y,C,V),f1) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,C,V) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
f1 * ((X,Y,C,V) /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
C /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
V /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
(C /. f2) + (V /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
f1 * ((C /. f2) + (V /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
f1 * (C /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
f1 * (V /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(f1 * (C /. f2)) + (f1 * (V /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,C,f1) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
((X,Y,C,f1) /. f2) + (f1 * (V /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,V,f1) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
((X,Y,C,f1) /. f2) + ((X,Y,V,f1) /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,(X,Y,C,f1),(X,Y,V,f1)) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
X is non empty set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
V is ext-real V25() real Element of REAL
f1 is ext-real V25() real Element of REAL
V * f1 is ext-real V25() real Element of REAL
(X,Y,C,(V * f1)) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C,f1) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,(X,Y,C,f1),V) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom (X,Y,C,(V * f1)) is Element of K19(X)
K19(X) is set
dom C is Element of K19(X)
dom (X,Y,C,f1) is Element of K19(X)
dom (X,Y,(X,Y,C,f1),V) is Element of K19(X)
f2 is Element of X
(X,Y,C,(V * f1)) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
C /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
(V * f1) * (C /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
f1 * (C /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
V * (f1 * (C /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,C,f1) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
V * ((X,Y,C,f1) /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,(X,Y,C,f1),V) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
X is non empty set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
V is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C,V) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
f1 is ext-real V25() real Element of REAL
(X,Y,(X,Y,C,V),f1) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C,f1) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,V,f1) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,(X,Y,C,f1),(X,Y,V,f1)) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom (X,Y,(X,Y,C,V),f1) is Element of K19(X)
K19(X) is set
dom (X,Y,C,V) is Element of K19(X)
dom C is Element of K19(X)
dom V is Element of K19(X)
(dom C) /\ (dom V) is Element of K19(X)
dom (X,Y,V,f1) is Element of K19(X)
(dom C) /\ (dom (X,Y,V,f1)) is Element of K19(X)
dom (X,Y,C,f1) is Element of K19(X)
(dom (X,Y,C,f1)) /\ (dom (X,Y,V,f1)) is Element of K19(X)
dom (X,Y,(X,Y,C,f1),(X,Y,V,f1)) is Element of K19(X)
f2 is Element of X
(X,Y,(X,Y,C,V),f1) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,C,V) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
f1 * ((X,Y,C,V) /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
C /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
V /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
(C /. f2) - (V /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
- (V /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(C /. f2) + (- (V /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
f1 * ((C /. f2) - (V /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
f1 * (C /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
f1 * (V /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(f1 * (C /. f2)) - (f1 * (V /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
- (f1 * (V /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
(f1 * (C /. f2)) + (- (f1 * (V /. f2))) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,C,f1) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
((X,Y,C,f1) /. f2) - (f1 * (V /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
((X,Y,C,f1) /. f2) + (- (f1 * (V /. f2))) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,V,f1) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
((X,Y,C,f1) /. f2) - ((X,Y,V,f1) /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
- ((X,Y,V,f1) /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
((X,Y,C,f1) /. f2) + (- ((X,Y,V,f1) /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,(X,Y,C,f1),(X,Y,V,f1)) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
X is non empty set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
V is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C,V) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,V,C) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,(X,Y,V,C),(- 1)) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom (X,Y,C,V) is Element of K19(X)
K19(X) is set
dom V is Element of K19(X)
dom C is Element of K19(X)
(dom V) /\ (dom C) is Element of K19(X)
dom (X,Y,V,C) is Element of K19(X)
dom (X,Y,(X,Y,V,C),(- 1)) is Element of K19(X)
f1 is Element of X
(X,Y,C,V) /. f1 is left_complementable right_complementable complementable Element of the U1 of Y
C /. f1 is left_complementable right_complementable complementable Element of the U1 of Y
V /. f1 is left_complementable right_complementable complementable Element of the U1 of Y
(C /. f1) - (V /. f1) is left_complementable right_complementable complementable Element of the U1 of Y
- (V /. f1) is left_complementable right_complementable complementable Element of the U1 of Y
(C /. f1) + (- (V /. f1)) is left_complementable right_complementable complementable Element of the U1 of Y
(V /. f1) - (C /. f1) is left_complementable right_complementable complementable Element of the U1 of Y
- (C /. f1) is left_complementable right_complementable complementable Element of the U1 of Y
(V /. f1) + (- (C /. f1)) is left_complementable right_complementable complementable Element of the U1 of Y
- ((V /. f1) - (C /. f1)) is left_complementable right_complementable complementable Element of the U1 of Y
(- 1) * ((V /. f1) - (C /. f1)) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,V,C) /. f1 is left_complementable right_complementable complementable Element of the U1 of Y
(- 1) * ((X,Y,V,C) /. f1) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,(X,Y,V,C),(- 1)) /. f1 is left_complementable right_complementable complementable Element of the U1 of Y
X is non empty set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
V is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C,V) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
f1 is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,V,f1) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C,(X,Y,V,f1)) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,(X,Y,C,V),f1) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom (X,Y,C,(X,Y,V,f1)) is Element of K19(X)
K19(X) is set
dom C is Element of K19(X)
dom (X,Y,V,f1) is Element of K19(X)
(dom C) /\ (dom (X,Y,V,f1)) is Element of K19(X)
dom V is Element of K19(X)
dom f1 is Element of K19(X)
(dom V) /\ (dom f1) is Element of K19(X)
(dom C) /\ ((dom V) /\ (dom f1)) is Element of K19(X)
(dom C) /\ (dom V) is Element of K19(X)
((dom C) /\ (dom V)) /\ (dom f1) is Element of K19(X)
dom (X,Y,C,V) is Element of K19(X)
(dom (X,Y,C,V)) /\ (dom f1) is Element of K19(X)
dom (X,Y,(X,Y,C,V),f1) is Element of K19(X)
f2 is Element of X
(X,Y,C,(X,Y,V,f1)) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
C /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,V,f1) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
(C /. f2) - ((X,Y,V,f1) /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
- ((X,Y,V,f1) /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(C /. f2) + (- ((X,Y,V,f1) /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
V /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
f1 /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
(V /. f2) + (f1 /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(C /. f2) - ((V /. f2) + (f1 /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
- ((V /. f2) + (f1 /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
(C /. f2) + (- ((V /. f2) + (f1 /. f2))) is left_complementable right_complementable complementable Element of the U1 of Y
(C /. f2) - (V /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
- (V /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(C /. f2) + (- (V /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
((C /. f2) - (V /. f2)) - (f1 /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
- (f1 /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
((C /. f2) - (V /. f2)) + (- (f1 /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,C,V) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
((X,Y,C,V) /. f2) - (f1 /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
((X,Y,C,V) /. f2) + (- (f1 /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,(X,Y,C,V),f1) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
X is non empty set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C,1) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
V is Element of X
dom (X,Y,C,1) is Element of K19(X)
K19(X) is set
(X,Y,C,1) /. V is left_complementable right_complementable complementable Element of the U1 of Y
C /. V is left_complementable right_complementable complementable Element of the U1 of Y
1 * (C /. V) is left_complementable right_complementable complementable Element of the U1 of Y
dom C is Element of K19(X)
X is non empty set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
V is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C,V) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
f1 is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,V,f1) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C,(X,Y,V,f1)) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,(X,Y,C,V),f1) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom (X,Y,C,(X,Y,V,f1)) is Element of K19(X)
K19(X) is set
dom C is Element of K19(X)
dom (X,Y,V,f1) is Element of K19(X)
(dom C) /\ (dom (X,Y,V,f1)) is Element of K19(X)
dom V is Element of K19(X)
dom f1 is Element of K19(X)
(dom V) /\ (dom f1) is Element of K19(X)
(dom C) /\ ((dom V) /\ (dom f1)) is Element of K19(X)
(dom C) /\ (dom V) is Element of K19(X)
((dom C) /\ (dom V)) /\ (dom f1) is Element of K19(X)
dom (X,Y,C,V) is Element of K19(X)
(dom (X,Y,C,V)) /\ (dom f1) is Element of K19(X)
dom (X,Y,(X,Y,C,V),f1) is Element of K19(X)
f2 is Element of X
(X,Y,C,(X,Y,V,f1)) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
C /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,V,f1) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
(C /. f2) - ((X,Y,V,f1) /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
- ((X,Y,V,f1) /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(C /. f2) + (- ((X,Y,V,f1) /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
V /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
f1 /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
(V /. f2) - (f1 /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
- (f1 /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(V /. f2) + (- (f1 /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
(C /. f2) - ((V /. f2) - (f1 /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
- ((V /. f2) - (f1 /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
(C /. f2) + (- ((V /. f2) - (f1 /. f2))) is left_complementable right_complementable complementable Element of the U1 of Y
(C /. f2) - (V /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
- (V /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(C /. f2) + (- (V /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
((C /. f2) - (V /. f2)) + (f1 /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,C,V) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
((X,Y,C,V) /. f2) + (f1 /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,(X,Y,C,V),f1) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
X is non empty set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
V is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C,V) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
f1 is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,V,f1) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C,(X,Y,V,f1)) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,(X,Y,C,V),f1) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom (X,Y,C,(X,Y,V,f1)) is Element of K19(X)
K19(X) is set
dom C is Element of K19(X)
dom (X,Y,V,f1) is Element of K19(X)
(dom C) /\ (dom (X,Y,V,f1)) is Element of K19(X)
dom V is Element of K19(X)
dom f1 is Element of K19(X)
(dom V) /\ (dom f1) is Element of K19(X)
(dom C) /\ ((dom V) /\ (dom f1)) is Element of K19(X)
(dom C) /\ (dom V) is Element of K19(X)
((dom C) /\ (dom V)) /\ (dom f1) is Element of K19(X)
dom (X,Y,C,V) is Element of K19(X)
(dom (X,Y,C,V)) /\ (dom f1) is Element of K19(X)
dom (X,Y,(X,Y,C,V),f1) is Element of K19(X)
f2 is Element of X
(X,Y,C,(X,Y,V,f1)) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
C /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,V,f1) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
(C /. f2) + ((X,Y,V,f1) /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
V /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
f1 /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
(V /. f2) - (f1 /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
- (f1 /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
(V /. f2) + (- (f1 /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
(C /. f2) + ((V /. f2) - (f1 /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
(C /. f2) + (V /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
((C /. f2) + (V /. f2)) - (f1 /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
((C /. f2) + (V /. f2)) + (- (f1 /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,C,V) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
((X,Y,C,V) /. f2) - (f1 /. f2) is left_complementable right_complementable complementable Element of the U1 of Y
((X,Y,C,V) /. f2) + (- (f1 /. f2)) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,(X,Y,C,V),f1) /. f2 is left_complementable right_complementable complementable Element of the U1 of Y
X is non empty set
K20(X,REAL) is V36() V37() V38() set
K19(K20(X,REAL)) is set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
||.C.|| is V1() V4(X) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(X,REAL))
V is V1() V4(X) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(X,REAL))
(X,Y,V,C) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
||.(X,Y,V,C).|| is V1() V4(X) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(X,REAL))
abs V is V1() V4(X) V5( REAL ) V6() V36() V37() V38() bounded_below Element of K19(K20(X,REAL))
(abs V) (#) ||.C.|| is V1() V4(X) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(X,REAL))
dom ||.(X,Y,V,C).|| is Element of K19(X)
K19(X) is set
dom (X,Y,V,C) is Element of K19(X)
dom V is Element of K19(X)
dom C is Element of K19(X)
(dom V) /\ (dom C) is Element of K19(X)
dom ||.C.|| is Element of K19(X)
(dom V) /\ (dom ||.C.||) is Element of K19(X)
dom (abs V) is Element of K19(X)
(dom (abs V)) /\ (dom ||.C.||) is Element of K19(X)
dom ((abs V) (#) ||.C.||) is Element of K19(X)
f1 is Element of X
||.(X,Y,V,C).|| . f1 is ext-real V25() real Element of REAL
(X,Y,V,C) /. f1 is left_complementable right_complementable complementable Element of the U1 of Y
||.((X,Y,V,C) /. f1).|| is ext-real non negative V25() real Element of REAL
the U8 of Y is V1() V4( the U1 of Y) V5( REAL ) V6() non empty total V30( the U1 of Y, REAL ) V36() V37() V38() Element of K19(K20( the U1 of Y,REAL))
K20( the U1 of Y,REAL) is V36() V37() V38() set
K19(K20( the U1 of Y,REAL)) is set
the U8 of Y . ((X,Y,V,C) /. f1) is ext-real V25() real Element of REAL
C /. f1 is left_complementable right_complementable complementable Element of the U1 of Y
V . f1 is ext-real V25() real Element of REAL
(V . f1) * (C /. f1) is left_complementable right_complementable complementable Element of the U1 of Y
||.((V . f1) * (C /. f1)).|| is ext-real non negative V25() real Element of REAL
the U8 of Y . ((V . f1) * (C /. f1)) is ext-real V25() real Element of REAL
abs (V . f1) is ext-real V25() real Element of REAL
||.(C /. f1).|| is ext-real non negative V25() real Element of REAL
the U8 of Y . (C /. f1) is ext-real V25() real Element of REAL
(abs (V . f1)) * ||.(C /. f1).|| is ext-real V25() real Element of REAL
(abs V) . f1 is ext-real V25() real Element of REAL
((abs V) . f1) * ||.(C /. f1).|| is ext-real V25() real Element of REAL
||.C.|| . f1 is ext-real V25() real Element of REAL
((abs V) . f1) * (||.C.|| . f1) is ext-real V25() real Element of REAL
((abs V) (#) ||.C.||) . f1 is ext-real V25() real Element of REAL
X is non empty set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
||.C.|| is V1() V4(X) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(X,REAL))
K20(X,REAL) is V36() V37() V38() set
K19(K20(X,REAL)) is set
V is ext-real V25() real Element of REAL
(X,Y,C,V) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
||.(X,Y,C,V).|| is V1() V4(X) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(X,REAL))
abs V is ext-real V25() real Element of REAL
(abs V) (#) ||.C.|| is V1() V4(X) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(X,REAL))
dom ||.(X,Y,C,V).|| is Element of K19(X)
K19(X) is set
dom (X,Y,C,V) is Element of K19(X)
dom C is Element of K19(X)
dom ||.C.|| is Element of K19(X)
dom ((abs V) (#) ||.C.||) is Element of K19(X)
f1 is Element of X
||.(X,Y,C,V).|| . f1 is ext-real V25() real Element of REAL
(X,Y,C,V) /. f1 is left_complementable right_complementable complementable Element of the U1 of Y
||.((X,Y,C,V) /. f1).|| is ext-real non negative V25() real Element of REAL
the U8 of Y is V1() V4( the U1 of Y) V5( REAL ) V6() non empty total V30( the U1 of Y, REAL ) V36() V37() V38() Element of K19(K20( the U1 of Y,REAL))
K20( the U1 of Y,REAL) is V36() V37() V38() set
K19(K20( the U1 of Y,REAL)) is set
the U8 of Y . ((X,Y,C,V) /. f1) is ext-real V25() real Element of REAL
C /. f1 is left_complementable right_complementable complementable Element of the U1 of Y
V * (C /. f1) is left_complementable right_complementable complementable Element of the U1 of Y
||.(V * (C /. f1)).|| is ext-real non negative V25() real Element of REAL
the U8 of Y . (V * (C /. f1)) is ext-real V25() real Element of REAL
||.(C /. f1).|| is ext-real non negative V25() real Element of REAL
the U8 of Y . (C /. f1) is ext-real V25() real Element of REAL
(abs V) * ||.(C /. f1).|| is ext-real V25() real Element of REAL
||.C.|| . f1 is ext-real V25() real Element of REAL
(abs V) * (||.C.|| . f1) is ext-real V25() real Element of REAL
((abs V) (#) ||.C.||) . f1 is ext-real V25() real Element of REAL
X is non empty set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C,(- 1)) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom (X,Y,C) is Element of K19(X)
K19(X) is set
dom C is Element of K19(X)
dom (X,Y,C,(- 1)) is Element of K19(X)
V is Element of X
(X,Y,C) /. V is left_complementable right_complementable complementable Element of the U1 of Y
C /. V is left_complementable right_complementable complementable Element of the U1 of Y
- (C /. V) is left_complementable right_complementable complementable Element of the U1 of Y
(- 1) * (C /. V) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,C,(- 1)) /. V is left_complementable right_complementable complementable Element of the U1 of Y
X is non empty set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,(X,Y,C)) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,(X,Y,C),(- 1)) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C,(- 1)) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,(X,Y,C,(- 1)),(- 1)) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(- 1) * (- 1) is ext-real V25() real Element of REAL
(X,Y,C,((- 1) * (- 1))) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
X is non empty set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
V is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C,V) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,V) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C,(X,Y,V)) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom (X,Y,C,V) is Element of K19(X)
K19(X) is set
dom C is Element of K19(X)
dom V is Element of K19(X)
(dom C) /\ (dom V) is Element of K19(X)
dom (X,Y,V) is Element of K19(X)
(dom C) /\ (dom (X,Y,V)) is Element of K19(X)
dom (X,Y,C,(X,Y,V)) is Element of K19(X)
f1 is Element of X
(X,Y,C,(X,Y,V)) /. f1 is left_complementable right_complementable complementable Element of the U1 of Y
C /. f1 is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,V) /. f1 is left_complementable right_complementable complementable Element of the U1 of Y
(C /. f1) + ((X,Y,V) /. f1) is left_complementable right_complementable complementable Element of the U1 of Y
V /. f1 is left_complementable right_complementable complementable Element of the U1 of Y
(C /. f1) - (V /. f1) is left_complementable right_complementable complementable Element of the U1 of Y
- (V /. f1) is left_complementable right_complementable complementable Element of the U1 of Y
(C /. f1) + (- (V /. f1)) is left_complementable right_complementable complementable Element of the U1 of Y
(X,Y,C,V) /. f1 is left_complementable right_complementable complementable Element of the U1 of Y
X is non empty set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
V is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,V) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C,(X,Y,V)) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C,V) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,(X,Y,V)) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C,(X,Y,(X,Y,V))) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
X is set
Y is non empty set
C is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of C is non empty set
K20(Y, the U1 of C) is set
K19(K20(Y, the U1 of C)) is set
V is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
V | X is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
f1 is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,V,f1) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,V,f1) | X is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
f1 | X is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,(V | X),(f1 | X)) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,(V | X),f1) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,V,(f1 | X)) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
f2 is Element of Y
dom ((Y,C,V,f1) | X) is Element of K19(Y)
K19(Y) is set
dom (Y,C,V,f1) is Element of K19(Y)
(dom (Y,C,V,f1)) /\ X is Element of K19(Y)
dom V is Element of K19(Y)
dom f1 is Element of K19(Y)
(dom V) /\ (dom f1) is Element of K19(Y)
(dom f1) /\ X is Element of K19(Y)
dom (f1 | X) is Element of K19(Y)
(dom V) /\ X is Element of K19(Y)
dom (V | X) is Element of K19(Y)
(dom (V | X)) /\ (dom (f1 | X)) is Element of K19(Y)
dom (Y,C,(V | X),(f1 | X)) is Element of K19(Y)
((Y,C,V,f1) | X) /. f2 is left_complementable right_complementable complementable Element of the U1 of C
(Y,C,V,f1) /. f2 is left_complementable right_complementable complementable Element of the U1 of C
V /. f2 is left_complementable right_complementable complementable Element of the U1 of C
f1 /. f2 is left_complementable right_complementable complementable Element of the U1 of C
(V /. f2) + (f1 /. f2) is left_complementable right_complementable complementable Element of the U1 of C
(V | X) /. f2 is left_complementable right_complementable complementable Element of the U1 of C
((V | X) /. f2) + (f1 /. f2) is left_complementable right_complementable complementable Element of the U1 of C
(f1 | X) /. f2 is left_complementable right_complementable complementable Element of the U1 of C
((V | X) /. f2) + ((f1 | X) /. f2) is left_complementable right_complementable complementable Element of the U1 of C
(Y,C,(V | X),(f1 | X)) /. f2 is left_complementable right_complementable complementable Element of the U1 of C
X /\ X is set
((dom V) /\ (dom f1)) /\ (X /\ X) is Element of K19(Y)
(dom f1) /\ (X /\ X) is Element of K19(Y)
(dom V) /\ ((dom f1) /\ (X /\ X)) is Element of K19(Y)
((dom f1) /\ X) /\ X is Element of K19(Y)
(dom V) /\ (((dom f1) /\ X) /\ X) is Element of K19(Y)
X /\ (dom (f1 | X)) is Element of K19(Y)
(dom V) /\ (X /\ (dom (f1 | X))) is Element of K19(Y)
((dom V) /\ X) /\ (dom (f1 | X)) is Element of K19(Y)
f2 is Element of Y
(dom (V | X)) /\ (dom f1) is Element of K19(Y)
dom (Y,C,(V | X),f1) is Element of K19(Y)
((Y,C,V,f1) | X) /. f2 is left_complementable right_complementable complementable Element of the U1 of C
(Y,C,V,f1) /. f2 is left_complementable right_complementable complementable Element of the U1 of C
V /. f2 is left_complementable right_complementable complementable Element of the U1 of C
f1 /. f2 is left_complementable right_complementable complementable Element of the U1 of C
(V /. f2) + (f1 /. f2) is left_complementable right_complementable complementable Element of the U1 of C
(V | X) /. f2 is left_complementable right_complementable complementable Element of the U1 of C
((V | X) /. f2) + (f1 /. f2) is left_complementable right_complementable complementable Element of the U1 of C
(Y,C,(V | X),f1) /. f2 is left_complementable right_complementable complementable Element of the U1 of C
((dom V) /\ (dom f1)) /\ X is Element of K19(Y)
((dom V) /\ X) /\ (dom f1) is Element of K19(Y)
f2 is Element of Y
(dom V) /\ (dom (f1 | X)) is Element of K19(Y)
dom (Y,C,V,(f1 | X)) is Element of K19(Y)
((Y,C,V,f1) | X) /. f2 is left_complementable right_complementable complementable Element of the U1 of C
(Y,C,V,f1) /. f2 is left_complementable right_complementable complementable Element of the U1 of C
V /. f2 is left_complementable right_complementable complementable Element of the U1 of C
f1 /. f2 is left_complementable right_complementable complementable Element of the U1 of C
(V /. f2) + (f1 /. f2) is left_complementable right_complementable complementable Element of the U1 of C
(f1 | X) /. f2 is left_complementable right_complementable complementable Element of the U1 of C
(V /. f2) + ((f1 | X) /. f2) is left_complementable right_complementable complementable Element of the U1 of C
(Y,C,V,(f1 | X)) /. f2 is left_complementable right_complementable complementable Element of the U1 of C
(dom V) /\ ((dom f1) /\ X) is Element of K19(Y)
X is set
Y is non empty set
K20(Y,REAL) is V36() V37() V38() set
K19(K20(Y,REAL)) is set
C is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of C is non empty set
K20(Y, the U1 of C) is set
K19(K20(Y, the U1 of C)) is set
V is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
V | X is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
f1 is V1() V4(Y) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(Y,REAL))
(Y,C,f1,V) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,f1,V) | X is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
f1 | X is V1() V4(Y) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(Y,REAL))
(Y,C,(f1 | X),(V | X)) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,(f1 | X),V) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,f1,(V | X)) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
f2 is Element of Y
dom ((Y,C,f1,V) | X) is Element of K19(Y)
K19(Y) is set
dom (Y,C,f1,V) is Element of K19(Y)
(dom (Y,C,f1,V)) /\ X is Element of K19(Y)
dom f1 is Element of K19(Y)
dom V is Element of K19(Y)
(dom f1) /\ (dom V) is Element of K19(Y)
(dom V) /\ X is Element of K19(Y)
dom (V | X) is Element of K19(Y)
(dom f1) /\ X is Element of K19(Y)
dom (f1 | X) is Element of K19(Y)
(dom (f1 | X)) /\ (dom (V | X)) is Element of K19(Y)
dom (Y,C,(f1 | X),(V | X)) is Element of K19(Y)
((Y,C,f1,V) | X) /. f2 is left_complementable right_complementable complementable Element of the U1 of C
(Y,C,f1,V) /. f2 is left_complementable right_complementable complementable Element of the U1 of C
V /. f2 is left_complementable right_complementable complementable Element of the U1 of C
f1 . f2 is ext-real V25() real Element of REAL
(f1 . f2) * (V /. f2) is left_complementable right_complementable complementable Element of the U1 of C
(f1 | X) . f2 is ext-real V25() real Element of REAL
((f1 | X) . f2) * (V /. f2) is left_complementable right_complementable complementable Element of the U1 of C
(V | X) /. f2 is left_complementable right_complementable complementable Element of the U1 of C
((f1 | X) . f2) * ((V | X) /. f2) is left_complementable right_complementable complementable Element of the U1 of C
(Y,C,(f1 | X),(V | X)) /. f2 is left_complementable right_complementable complementable Element of the U1 of C
X /\ X is set
((dom f1) /\ (dom V)) /\ (X /\ X) is Element of K19(Y)
(dom V) /\ (X /\ X) is Element of K19(Y)
(dom f1) /\ ((dom V) /\ (X /\ X)) is Element of K19(Y)
((dom V) /\ X) /\ X is Element of K19(Y)
(dom f1) /\ (((dom V) /\ X) /\ X) is Element of K19(Y)
X /\ (dom (V | X)) is Element of K19(Y)
(dom f1) /\ (X /\ (dom (V | X))) is Element of K19(Y)
((dom f1) /\ X) /\ (dom (V | X)) is Element of K19(Y)
f2 is Element of Y
(dom (f1 | X)) /\ (dom V) is Element of K19(Y)
dom (Y,C,(f1 | X),V) is Element of K19(Y)
((Y,C,f1,V) | X) /. f2 is left_complementable right_complementable complementable Element of the U1 of C
(Y,C,f1,V) /. f2 is left_complementable right_complementable complementable Element of the U1 of C
V /. f2 is left_complementable right_complementable complementable Element of the U1 of C
f1 . f2 is ext-real V25() real Element of REAL
(f1 . f2) * (V /. f2) is left_complementable right_complementable complementable Element of the U1 of C
(f1 | X) . f2 is ext-real V25() real Element of REAL
((f1 | X) . f2) * (V /. f2) is left_complementable right_complementable complementable Element of the U1 of C
(Y,C,(f1 | X),V) /. f2 is left_complementable right_complementable complementable Element of the U1 of C
((dom f1) /\ (dom V)) /\ X is Element of K19(Y)
((dom f1) /\ X) /\ (dom V) is Element of K19(Y)
f2 is Element of Y
(dom f1) /\ (dom (V | X)) is Element of K19(Y)
dom (Y,C,f1,(V | X)) is Element of K19(Y)
((Y,C,f1,V) | X) /. f2 is left_complementable right_complementable complementable Element of the U1 of C
(Y,C,f1,V) /. f2 is left_complementable right_complementable complementable Element of the U1 of C
V /. f2 is left_complementable right_complementable complementable Element of the U1 of C
f1 . f2 is ext-real V25() real Element of REAL
(f1 . f2) * (V /. f2) is left_complementable right_complementable complementable Element of the U1 of C
(V | X) /. f2 is left_complementable right_complementable complementable Element of the U1 of C
(f1 . f2) * ((V | X) /. f2) is left_complementable right_complementable complementable Element of the U1 of C
(Y,C,f1,(V | X)) /. f2 is left_complementable right_complementable complementable Element of the U1 of C
(dom f1) /\ ((dom V) /\ X) is Element of K19(Y)
X is set
Y is non empty set
C is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of C is non empty set
K20(Y, the U1 of C) is set
K19(K20(Y, the U1 of C)) is set
V is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,V) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,V) | X is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
V | X is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,(V | X)) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
||.V.|| is V1() V4(Y) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(Y,REAL))
K20(Y,REAL) is V36() V37() V38() set
K19(K20(Y,REAL)) is set
||.V.|| | X is V1() V4(Y) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(Y,REAL))
||.(V | X).|| is V1() V4(Y) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(Y,REAL))
f1 is Element of Y
dom ((Y,C,V) | X) is Element of K19(Y)
K19(Y) is set
dom (Y,C,V) is Element of K19(Y)
(dom (Y,C,V)) /\ X is Element of K19(Y)
dom V is Element of K19(Y)
(dom V) /\ X is Element of K19(Y)
dom (V | X) is Element of K19(Y)
dom (Y,C,(V | X)) is Element of K19(Y)
((Y,C,V) | X) /. f1 is left_complementable right_complementable complementable Element of the U1 of C
(Y,C,V) /. f1 is left_complementable right_complementable complementable Element of the U1 of C
V /. f1 is left_complementable right_complementable complementable Element of the U1 of C
- (V /. f1) is left_complementable right_complementable complementable Element of the U1 of C
(V | X) /. f1 is left_complementable right_complementable complementable Element of the U1 of C
- ((V | X) /. f1) is left_complementable right_complementable complementable Element of the U1 of C
(Y,C,(V | X)) /. f1 is left_complementable right_complementable complementable Element of the U1 of C
dom (||.V.|| | X) is Element of K19(Y)
dom ||.V.|| is Element of K19(Y)
(dom ||.V.||) /\ X is Element of K19(Y)
dom ||.(V | X).|| is Element of K19(Y)
f1 is Element of Y
(||.V.|| | X) . f1 is ext-real V25() real Element of REAL
||.V.|| . f1 is ext-real V25() real Element of REAL
V /. f1 is left_complementable right_complementable complementable Element of the U1 of C
||.(V /. f1).|| is ext-real non negative V25() real Element of REAL
the U8 of C is V1() V4( the U1 of C) V5( REAL ) V6() non empty total V30( the U1 of C, REAL ) V36() V37() V38() Element of K19(K20( the U1 of C,REAL))
K20( the U1 of C,REAL) is V36() V37() V38() set
K19(K20( the U1 of C,REAL)) is set
the U8 of C . (V /. f1) is ext-real V25() real Element of REAL
(V | X) /. f1 is left_complementable right_complementable complementable Element of the U1 of C
||.((V | X) /. f1).|| is ext-real non negative V25() real Element of REAL
the U8 of C . ((V | X) /. f1) is ext-real V25() real Element of REAL
||.(V | X).|| . f1 is ext-real V25() real Element of REAL
X is set
Y is non empty set
C is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of C is non empty set
K20(Y, the U1 of C) is set
K19(K20(Y, the U1 of C)) is set
V is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
V | X is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
f1 is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,V,f1) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,V,f1) | X is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
f1 | X is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,(V | X),(f1 | X)) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,(V | X),f1) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,V,(f1 | X)) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,f1) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,V,(Y,C,f1)) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,V,(Y,C,f1)) | X is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,f1) | X is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,(V | X),((Y,C,f1) | X)) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,(f1 | X)) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,(V | X),(Y,C,(f1 | X))) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,(V | X),(Y,C,f1)) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,V,((Y,C,f1) | X)) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,V,(Y,C,(f1 | X))) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
X is set
Y is non empty set
C is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of C is non empty set
K20(Y, the U1 of C) is set
K19(K20(Y, the U1 of C)) is set
V is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
V | X is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
f1 is ext-real V25() real Element of REAL
(Y,C,V,f1) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,V,f1) | X is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,(V | X),f1) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
f2 is Element of Y
dom ((Y,C,V,f1) | X) is Element of K19(Y)
K19(Y) is set
dom (Y,C,V,f1) is Element of K19(Y)
(dom (Y,C,V,f1)) /\ X is Element of K19(Y)
dom V is Element of K19(Y)
(dom V) /\ X is Element of K19(Y)
dom (V | X) is Element of K19(Y)
dom (Y,C,(V | X),f1) is Element of K19(Y)
((Y,C,V,f1) | X) /. f2 is left_complementable right_complementable complementable Element of the U1 of C
(Y,C,V,f1) /. f2 is left_complementable right_complementable complementable Element of the U1 of C
V /. f2 is left_complementable right_complementable complementable Element of the U1 of C
f1 * (V /. f2) is left_complementable right_complementable complementable Element of the U1 of C
(V | X) /. f2 is left_complementable right_complementable complementable Element of the U1 of C
f1 * ((V | X) /. f2) is left_complementable right_complementable complementable Element of the U1 of C
(Y,C,(V | X),f1) /. f2 is left_complementable right_complementable complementable Element of the U1 of C
X is non empty set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
V is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C,V) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C,V) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom (X,Y,C,V) is Element of K19(X)
K19(X) is set
dom C is Element of K19(X)
dom V is Element of K19(X)
(dom C) /\ (dom V) is Element of K19(X)
dom (X,Y,C,V) is Element of K19(X)
K19(X) is set
dom C is Element of K19(X)
dom V is Element of K19(X)
(dom C) /\ (dom V) is Element of K19(X)
X is non empty set
K20(X,REAL) is V36() V37() V38() set
K19(K20(X,REAL)) is set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
V is V1() V4(X) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(X,REAL))
(X,Y,V,C) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom (X,Y,V,C) is Element of K19(X)
K19(X) is set
dom V is Element of K19(X)
dom C is Element of K19(X)
(dom V) /\ (dom C) is Element of K19(X)
X is non empty set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
V is ext-real V25() real Element of REAL
(X,Y,C,V) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
dom (X,Y,C,V) is Element of K19(X)
K19(X) is set
dom C is Element of K19(X)
X is non empty set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
(X,Y,C,(- 1)) is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
X is non empty set
Y is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
C is V1() V4(X) V5( the U1 of Y) V6() Element of K19(K20(X, the U1 of Y))
||.C.|| is V1() V4(X) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(X,REAL))
K20(X,REAL) is V36() V37() V38() set
K19(K20(X,REAL)) is set
dom C is Element of K19(X)
K19(X) is set
dom ||.C.|| is Element of K19(X)
dom ||.C.|| is Element of K19(X)
K19(X) is set
dom C is Element of K19(X)
X is non empty set
Y is Element of X
C is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of C is non empty set
K20(X, the U1 of C) is set
K19(K20(X, the U1 of C)) is set
V is V1() V4(X) V5( the U1 of C) V6() Element of K19(K20(X, the U1 of C))
V /. Y is left_complementable right_complementable complementable Element of the U1 of C
f1 is V1() V4(X) V5( the U1 of C) V6() Element of K19(K20(X, the U1 of C))
(X,C,V,f1) is V1() V4(X) V5( the U1 of C) V6() Element of K19(K20(X, the U1 of C))
(X,C,V,f1) /. Y is left_complementable right_complementable complementable Element of the U1 of C
f1 /. Y is left_complementable right_complementable complementable Element of the U1 of C
(V /. Y) + (f1 /. Y) is left_complementable right_complementable complementable Element of the U1 of C
(X,C,V,f1) is V1() V4(X) V5( the U1 of C) V6() Element of K19(K20(X, the U1 of C))
(X,C,V,f1) /. Y is left_complementable right_complementable complementable Element of the U1 of C
(V /. Y) - (f1 /. Y) is left_complementable right_complementable complementable Element of the U1 of C
- (f1 /. Y) is left_complementable right_complementable complementable Element of the U1 of C
(V /. Y) + (- (f1 /. Y)) is left_complementable right_complementable complementable Element of the U1 of C
dom (X,C,V,f1) is Element of K19(X)
K19(X) is set
dom (X,C,V,f1) is Element of K19(X)
X is non empty set
K20(X,REAL) is V36() V37() V38() set
K19(K20(X,REAL)) is set
Y is Element of X
C is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of C is non empty set
K20(X, the U1 of C) is set
K19(K20(X, the U1 of C)) is set
V is V1() V4(X) V5( the U1 of C) V6() Element of K19(K20(X, the U1 of C))
V /. Y is left_complementable right_complementable complementable Element of the U1 of C
f1 is V1() V4(X) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(X,REAL))
(X,C,f1,V) is V1() V4(X) V5( the U1 of C) V6() Element of K19(K20(X, the U1 of C))
(X,C,f1,V) /. Y is left_complementable right_complementable complementable Element of the U1 of C
f1 . Y is ext-real V25() real Element of REAL
(f1 . Y) * (V /. Y) is left_complementable right_complementable complementable Element of the U1 of C
dom (X,C,f1,V) is Element of K19(X)
K19(X) is set
X is non empty set
Y is Element of X
C is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of C is non empty set
K20(X, the U1 of C) is set
K19(K20(X, the U1 of C)) is set
V is V1() V4(X) V5( the U1 of C) V6() Element of K19(K20(X, the U1 of C))
V /. Y is left_complementable right_complementable complementable Element of the U1 of C
f1 is ext-real V25() real Element of REAL
(X,C,V,f1) is V1() V4(X) V5( the U1 of C) V6() Element of K19(K20(X, the U1 of C))
(X,C,V,f1) /. Y is left_complementable right_complementable complementable Element of the U1 of C
f1 * (V /. Y) is left_complementable right_complementable complementable Element of the U1 of C
dom (X,C,V,f1) is Element of K19(X)
K19(X) is set
X is non empty set
Y is Element of X
C is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of C is non empty set
K20(X, the U1 of C) is set
K19(K20(X, the U1 of C)) is set
V is V1() V4(X) V5( the U1 of C) V6() Element of K19(K20(X, the U1 of C))
(X,C,V) is V1() V4(X) V5( the U1 of C) V6() Element of K19(K20(X, the U1 of C))
(X,C,V) /. Y is left_complementable right_complementable complementable Element of the U1 of C
V /. Y is left_complementable right_complementable complementable Element of the U1 of C
- (V /. Y) is left_complementable right_complementable complementable Element of the U1 of C
||.V.|| is V1() V4(X) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(X,REAL))
K20(X,REAL) is V36() V37() V38() set
K19(K20(X,REAL)) is set
||.V.|| . Y is ext-real V25() real Element of REAL
||.(V /. Y).|| is ext-real non negative V25() real Element of REAL
the U8 of C is V1() V4( the U1 of C) V5( REAL ) V6() non empty total V30( the U1 of C, REAL ) V36() V37() V38() Element of K19(K20( the U1 of C,REAL))
K20( the U1 of C,REAL) is V36() V37() V38() set
K19(K20( the U1 of C,REAL)) is set
the U8 of C . (V /. Y) is ext-real V25() real Element of REAL
dom (X,C,V) is Element of K19(X)
K19(X) is set
dom ||.V.|| is Element of K19(X)
X is non empty set
Y is non empty NORMSTR
the U1 of Y is non empty set
K20(X, the U1 of Y) is set
K19(K20(X, the U1 of Y)) is set
X is set
Y is set
C is non empty set
V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of V is non empty set
K20(C, the U1 of V) is set
K19(K20(C, the U1 of V)) is set
f1 is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
dom f1 is Element of K19(C)
K19(C) is set
Y /\ (dom f1) is Element of K19(C)
f2 is ext-real V25() real Element of REAL
X /\ (dom f1) is Element of K19(C)
c is Element of C
f1 /. c is left_complementable right_complementable complementable Element of the U1 of V
||.(f1 /. c).|| is ext-real non negative V25() real Element of REAL
the U8 of V is V1() V4( the U1 of V) V5( REAL ) V6() non empty total V30( the U1 of V, REAL ) V36() V37() V38() Element of K19(K20( the U1 of V,REAL))
K20( the U1 of V,REAL) is V36() V37() V38() set
K19(K20( the U1 of V,REAL)) is set
the U8 of V . (f1 /. c) is ext-real V25() real Element of REAL
X is set
Y is non empty set
C is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of C is non empty set
K20(Y, the U1 of C) is set
K19(K20(Y, the U1 of C)) is set
V is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
dom V is Element of K19(Y)
K19(Y) is set
X /\ (dom V) is Element of K19(Y)
f1 is Element of Y
V /. f1 is left_complementable right_complementable complementable Element of the U1 of C
||.(V /. f1).|| is ext-real non negative V25() real Element of REAL
the U8 of C is V1() V4( the U1 of C) V5( REAL ) V6() non empty total V30( the U1 of C, REAL ) V36() V37() V38() Element of K19(K20( the U1 of C,REAL))
K20( the U1 of C,REAL) is V36() V37() V38() set
K19(K20( the U1 of C,REAL)) is set
the U8 of C . (V /. f1) is ext-real V25() real Element of REAL
X is set
Y is non empty set
C is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of C is non empty set
K20(Y, the U1 of C) is set
K19(K20(Y, the U1 of C)) is set
V is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,V,0) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
f2 is Element of Y
V /. f2 is left_complementable right_complementable complementable Element of the U1 of C
||.(V /. f2).|| is ext-real non negative V25() real Element of REAL
the U8 of C is V1() V4( the U1 of C) V5( REAL ) V6() non empty total V30( the U1 of C, REAL ) V36() V37() V38() Element of K19(K20( the U1 of C,REAL))
K20( the U1 of C,REAL) is V36() V37() V38() set
K19(K20( the U1 of C,REAL)) is set
the U8 of C . (V /. f2) is ext-real V25() real Element of REAL
0 * ||.(V /. f2).|| is ext-real V25() real Element of REAL
abs 0 is ext-real V25() real Element of REAL
(abs 0) * ||.(V /. f2).|| is ext-real V25() real Element of REAL
0 * (V /. f2) is left_complementable right_complementable complementable Element of the U1 of C
||.(0 * (V /. f2)).|| is ext-real non negative V25() real Element of REAL
the U8 of C . (0 * (V /. f2)) is ext-real V25() real Element of REAL
dom (Y,C,V,0) is Element of K19(Y)
K19(Y) is set
X /\ (dom (Y,C,V,0)) is Element of K19(Y)
(Y,C,V,0) /. f2 is left_complementable right_complementable complementable Element of the U1 of C
||.((Y,C,V,0) /. f2).|| is ext-real non negative V25() real Element of REAL
the U8 of C . ((Y,C,V,0) /. f2) is ext-real V25() real Element of REAL
f1 is ext-real natural V25() real V46() V47() V48() V49() V50() V51() V131() V132() Element of NAT
f1 is ext-real natural V25() real V46() V47() V48() V49() V50() V51() V131() V132() Element of NAT
X is set
Y is non empty set
C is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of C is non empty set
K20(Y, the U1 of C) is set
K19(K20(Y, the U1 of C)) is set
V is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
f1 is ext-real V25() real Element of REAL
(Y,C,V,f1) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
dom V is Element of K19(Y)
K19(Y) is set
X /\ (dom V) is Element of K19(Y)
f2 is ext-real V25() real Element of REAL
abs f1 is ext-real V25() real Element of REAL
abs f2 is ext-real V25() real Element of REAL
(abs f1) * (abs f2) is ext-real V25() real Element of REAL
dom (Y,C,V,f1) is Element of K19(Y)
X /\ (dom (Y,C,V,f1)) is Element of K19(Y)
c is ext-real V25() real Element of REAL
r2 is Element of Y
(Y,C,V,f1) /. r2 is left_complementable right_complementable complementable Element of the U1 of C
||.((Y,C,V,f1) /. r2).|| is ext-real non negative V25() real Element of REAL
the U8 of C is V1() V4( the U1 of C) V5( REAL ) V6() non empty total V30( the U1 of C, REAL ) V36() V37() V38() Element of K19(K20( the U1 of C,REAL))
K20( the U1 of C,REAL) is V36() V37() V38() set
K19(K20( the U1 of C,REAL)) is set
the U8 of C . ((Y,C,V,f1) /. r2) is ext-real V25() real Element of REAL
V /. r2 is left_complementable right_complementable complementable Element of the U1 of C
||.(V /. r2).|| is ext-real non negative V25() real Element of REAL
the U8 of C . (V /. r2) is ext-real V25() real Element of REAL
(abs f1) * ||.(V /. r2).|| is ext-real V25() real Element of REAL
f1 * (V /. r2) is left_complementable right_complementable complementable Element of the U1 of C
||.(f1 * (V /. r2)).|| is ext-real non negative V25() real Element of REAL
the U8 of C . (f1 * (V /. r2)) is ext-real V25() real Element of REAL
X is set
Y is non empty set
C is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of C is non empty set
K20(Y, the U1 of C) is set
K19(K20(Y, the U1 of C)) is set
V is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
||.V.|| is V1() V4(Y) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(Y,REAL))
K20(Y,REAL) is V36() V37() V38() set
K19(K20(Y,REAL)) is set
||.V.|| | X is V1() V4(Y) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(Y,REAL))
(Y,C,V) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
dom V is Element of K19(Y)
K19(Y) is set
X /\ (dom V) is Element of K19(Y)
f1 is ext-real V25() real Element of REAL
f2 is set
dom ||.V.|| is Element of K19(Y)
X /\ (dom ||.V.||) is Element of K19(Y)
V /. f2 is left_complementable right_complementable complementable Element of the U1 of C
||.(V /. f2).|| is ext-real non negative V25() real Element of REAL
the U8 of C is V1() V4( the U1 of C) V5( REAL ) V6() non empty total V30( the U1 of C, REAL ) V36() V37() V38() Element of K19(K20( the U1 of C,REAL))
K20( the U1 of C,REAL) is V36() V37() V38() set
K19(K20( the U1 of C,REAL)) is set
the U8 of C . (V /. f2) is ext-real V25() real Element of REAL
abs ||.(V /. f2).|| is ext-real V25() real Element of REAL
||.V.|| . f2 is ext-real V25() real Element of REAL
abs (||.V.|| . f2) is ext-real V25() real Element of REAL
(Y,C,V,(- 1)) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
X is set
Y is set
X /\ Y is set
C is non empty set
V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of V is non empty set
K20(C, the U1 of V) is set
K19(K20(C, the U1 of V)) is set
f1 is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
f2 is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
(C,V,f1,f2) is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
dom f1 is Element of K19(C)
K19(C) is set
X /\ (dom f1) is Element of K19(C)
c is ext-real V25() real Element of REAL
dom f2 is Element of K19(C)
Y /\ (dom f2) is Element of K19(C)
r2 is ext-real V25() real Element of REAL
c + r2 is ext-real V25() real Element of REAL
dom (C,V,f1,f2) is Element of K19(C)
(X /\ Y) /\ (dom (C,V,f1,f2)) is Element of K19(C)
c is ext-real V25() real Element of REAL
r is Element of C
(C,V,f1,f2) /. r is left_complementable right_complementable complementable Element of the U1 of V
||.((C,V,f1,f2) /. r).|| is ext-real non negative V25() real Element of REAL
the U8 of V is V1() V4( the U1 of V) V5( REAL ) V6() non empty total V30( the U1 of V, REAL ) V36() V37() V38() Element of K19(K20( the U1 of V,REAL))
K20( the U1 of V,REAL) is V36() V37() V38() set
K19(K20( the U1 of V,REAL)) is set
the U8 of V . ((C,V,f1,f2) /. r) is ext-real V25() real Element of REAL
(dom f1) /\ (dom f2) is Element of K19(C)
f2 /. r is left_complementable right_complementable complementable Element of the U1 of V
||.(f2 /. r).|| is ext-real non negative V25() real Element of REAL
the U8 of V . (f2 /. r) is ext-real V25() real Element of REAL
f1 /. r is left_complementable right_complementable complementable Element of the U1 of V
||.(f1 /. r).|| is ext-real non negative V25() real Element of REAL
the U8 of V . (f1 /. r) is ext-real V25() real Element of REAL
(f1 /. r) + (f2 /. r) is left_complementable right_complementable complementable Element of the U1 of V
||.((f1 /. r) + (f2 /. r)).|| is ext-real non negative V25() real Element of REAL
the U8 of V . ((f1 /. r) + (f2 /. r)) is ext-real V25() real Element of REAL
||.(f1 /. r).|| + ||.(f2 /. r).|| is ext-real non negative V25() real Element of REAL
X is set
Y is set
X /\ Y is set
C is non empty set
K20(C,REAL) is V36() V37() V38() set
K19(K20(C,REAL)) is set
V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of V is non empty set
K20(C, the U1 of V) is set
K19(K20(C, the U1 of V)) is set
f1 is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
f2 is V1() V4(C) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(C,REAL))
f2 | X is V1() V4(C) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(C,REAL))
(C,V,f2,f1) is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
dom f2 is Element of K19(C)
K19(C) is set
X /\ (dom f2) is Element of K19(C)
c is ext-real V25() real set
dom f1 is Element of K19(C)
Y /\ (dom f1) is Element of K19(C)
r2 is ext-real V25() real Element of REAL
c is ext-real V25() real Element of REAL
c * r2 is ext-real V25() real Element of REAL
c is Element of C
dom (C,V,f2,f1) is Element of K19(C)
(X /\ Y) /\ (dom (C,V,f2,f1)) is Element of K19(C)
(dom f2) /\ (dom f1) is Element of K19(C)
f2 . c is ext-real V25() real Element of REAL
abs (f2 . c) is ext-real V25() real Element of REAL
f1 /. c is left_complementable right_complementable complementable Element of the U1 of V
||.(f1 /. c).|| is ext-real non negative V25() real Element of REAL
the U8 of V is V1() V4( the U1 of V) V5( REAL ) V6() non empty total V30( the U1 of V, REAL ) V36() V37() V38() Element of K19(K20( the U1 of V,REAL))
K20( the U1 of V,REAL) is V36() V37() V38() set
K19(K20( the U1 of V,REAL)) is set
the U8 of V . (f1 /. c) is ext-real V25() real Element of REAL
(abs (f2 . c)) * ||.(f1 /. c).|| is ext-real V25() real Element of REAL
r is ext-real V25() real Element of REAL
(f2 . c) * (f1 /. c) is left_complementable right_complementable complementable Element of the U1 of V
||.((f2 . c) * (f1 /. c)).|| is ext-real non negative V25() real Element of REAL
the U8 of V . ((f2 . c) * (f1 /. c)) is ext-real V25() real Element of REAL
(C,V,f2,f1) /. c is left_complementable right_complementable complementable Element of the U1 of V
||.((C,V,f2,f1) /. c).|| is ext-real non negative V25() real Element of REAL
the U8 of V . ((C,V,f2,f1) /. c) is ext-real V25() real Element of REAL
r is ext-real V25() real Element of REAL
X is set
Y is set
X /\ Y is set
C is non empty set
V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of V is non empty set
K20(C, the U1 of V) is set
K19(K20(C, the U1 of V)) is set
f1 is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
f2 is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
(C,V,f1,f2) is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
(C,V,f2) is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
(C,V,f1,(C,V,f2)) is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
X is set
Y is set
X \/ Y is set
C is non empty set
V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of V is non empty set
K20(C, the U1 of V) is set
K19(K20(C, the U1 of V)) is set
f1 is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
dom f1 is Element of K19(C)
K19(C) is set
X /\ (dom f1) is Element of K19(C)
f2 is ext-real V25() real Element of REAL
Y /\ (dom f1) is Element of K19(C)
c is ext-real V25() real Element of REAL
abs f2 is ext-real V25() real Element of REAL
abs c is ext-real V25() real Element of REAL
(abs f2) + (abs c) is ext-real V25() real Element of REAL
(X \/ Y) /\ (dom f1) is Element of K19(C)
r2 is ext-real V25() real Element of REAL
c is Element of C
f1 /. c is left_complementable right_complementable complementable Element of the U1 of V
||.(f1 /. c).|| is ext-real non negative V25() real Element of REAL
the U8 of V is V1() V4( the U1 of V) V5( REAL ) V6() non empty total V30( the U1 of V, REAL ) V36() V37() V38() Element of K19(K20( the U1 of V,REAL))
K20( the U1 of V,REAL) is V36() V37() V38() set
K19(K20( the U1 of V,REAL)) is set
the U8 of V . (f1 /. c) is ext-real V25() real Element of REAL
||.(f1 /. c).|| + 0 is ext-real V25() real Element of REAL
0 + ||.(f1 /. c).|| is ext-real V25() real Element of REAL
X is set
Y is set
X /\ Y is set
C is non empty set
V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of V is non empty set
K20(C, the U1 of V) is set
K19(K20(C, the U1 of V)) is set
f1 is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
f1 | X is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
f2 is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
f2 | Y is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
(C,V,f1,f2) is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
(C,V,f1,f2) | (X /\ Y) is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
(C,V,f1,f2) is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
(C,V,f1,f2) | (X /\ Y) is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
dom f1 is Element of K19(C)
K19(C) is set
X /\ (dom f1) is Element of K19(C)
c is left_complementable right_complementable complementable Element of the U1 of V
dom f2 is Element of K19(C)
Y /\ (dom f2) is Element of K19(C)
r2 is left_complementable right_complementable complementable Element of the U1 of V
c is Element of C
dom (C,V,f1,f2) is Element of K19(C)
(X /\ Y) /\ (dom (C,V,f1,f2)) is Element of K19(C)
(dom f1) /\ (dom f2) is Element of K19(C)
(C,V,f1,f2) /. c is left_complementable right_complementable complementable Element of the U1 of V
f1 /. c is left_complementable right_complementable complementable Element of the U1 of V
f2 /. c is left_complementable right_complementable complementable Element of the U1 of V
(f1 /. c) + (f2 /. c) is left_complementable right_complementable complementable Element of the U1 of V
c + (f2 /. c) is left_complementable right_complementable complementable Element of the U1 of V
c + r2 is left_complementable right_complementable complementable Element of the U1 of V
c is Element of C
dom (C,V,f1,f2) is Element of K19(C)
(X /\ Y) /\ (dom (C,V,f1,f2)) is Element of K19(C)
(C,V,f1,f2) /. c is left_complementable right_complementable complementable Element of the U1 of V
f1 /. c is left_complementable right_complementable complementable Element of the U1 of V
f2 /. c is left_complementable right_complementable complementable Element of the U1 of V
(f1 /. c) - (f2 /. c) is left_complementable right_complementable complementable Element of the U1 of V
- (f2 /. c) is left_complementable right_complementable complementable Element of the U1 of V
(f1 /. c) + (- (f2 /. c)) is left_complementable right_complementable complementable Element of the U1 of V
c - (f2 /. c) is left_complementable right_complementable complementable Element of the U1 of V
c + (- (f2 /. c)) is left_complementable right_complementable complementable Element of the U1 of V
c - r2 is left_complementable right_complementable complementable Element of the U1 of V
- r2 is left_complementable right_complementable complementable Element of the U1 of V
c + (- r2) is left_complementable right_complementable complementable Element of the U1 of V
X is set
Y is set
X /\ Y is set
C is non empty set
K20(C,REAL) is V36() V37() V38() set
K19(K20(C,REAL)) is set
V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of V is non empty set
K20(C, the U1 of V) is set
K19(K20(C, the U1 of V)) is set
f1 is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
f1 | Y is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
f2 is V1() V4(C) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(C,REAL))
f2 | X is V1() V4(C) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(C,REAL))
(C,V,f2,f1) is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
(C,V,f2,f1) | (X /\ Y) is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
dom f2 is Element of K19(C)
K19(C) is set
X /\ (dom f2) is Element of K19(C)
c is ext-real V25() real Element of REAL
dom f1 is Element of K19(C)
Y /\ (dom f1) is Element of K19(C)
r2 is left_complementable right_complementable complementable Element of the U1 of V
c is Element of C
dom (C,V,f2,f1) is Element of K19(C)
(X /\ Y) /\ (dom (C,V,f2,f1)) is Element of K19(C)
(dom f2) /\ (dom f1) is Element of K19(C)
(C,V,f2,f1) /. c is left_complementable right_complementable complementable Element of the U1 of V
f1 /. c is left_complementable right_complementable complementable Element of the U1 of V
f2 . c is ext-real V25() real Element of REAL
(f2 . c) * (f1 /. c) is left_complementable right_complementable complementable Element of the U1 of V
c * (f1 /. c) is left_complementable right_complementable complementable Element of the U1 of V
c * r2 is left_complementable right_complementable complementable Element of the U1 of V
X is set
Y is non empty set
C is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of C is non empty set
K20(Y, the U1 of C) is set
K19(K20(Y, the U1 of C)) is set
V is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
V | X is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
f1 is ext-real V25() real Element of REAL
(Y,C,V,f1) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,V,f1) | X is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
dom V is Element of K19(Y)
K19(Y) is set
X /\ (dom V) is Element of K19(Y)
f2 is left_complementable right_complementable complementable Element of the U1 of C
c is Element of Y
dom (Y,C,V,f1) is Element of K19(Y)
X /\ (dom (Y,C,V,f1)) is Element of K19(Y)
(Y,C,V,f1) /. c is left_complementable right_complementable complementable Element of the U1 of C
V /. c is left_complementable right_complementable complementable Element of the U1 of C
f1 * (V /. c) is left_complementable right_complementable complementable Element of the U1 of C
f1 * f2 is left_complementable right_complementable complementable Element of the U1 of C
X is set
Y is non empty set
C is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of C is non empty set
K20(Y, the U1 of C) is set
K19(K20(Y, the U1 of C)) is set
V is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
V | X is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
||.V.|| is V1() V4(Y) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(Y,REAL))
K20(Y,REAL) is V36() V37() V38() set
K19(K20(Y,REAL)) is set
||.V.|| | X is V1() V4(Y) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(Y,REAL))
(Y,C,V) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,V) | X is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
dom V is Element of K19(Y)
K19(Y) is set
X /\ (dom V) is Element of K19(Y)
f1 is left_complementable right_complementable complementable Element of the U1 of C
f2 is Element of Y
dom ||.V.|| is Element of K19(Y)
X /\ (dom ||.V.||) is Element of K19(Y)
||.V.|| . f2 is ext-real V25() real Element of REAL
V /. f2 is left_complementable right_complementable complementable Element of the U1 of C
||.(V /. f2).|| is ext-real non negative V25() real Element of REAL
the U8 of C is V1() V4( the U1 of C) V5( REAL ) V6() non empty total V30( the U1 of C, REAL ) V36() V37() V38() Element of K19(K20( the U1 of C,REAL))
K20( the U1 of C,REAL) is V36() V37() V38() set
K19(K20( the U1 of C,REAL)) is set
the U8 of C . (V /. f2) is ext-real V25() real Element of REAL
||.f1.|| is ext-real non negative V25() real Element of REAL
the U8 of C . f1 is ext-real V25() real Element of REAL
- f1 is left_complementable right_complementable complementable Element of the U1 of C
c is Element of Y
dom (Y,C,V) is Element of K19(Y)
X /\ (dom (Y,C,V)) is Element of K19(Y)
V /. c is left_complementable right_complementable complementable Element of the U1 of C
- (V /. c) is left_complementable right_complementable complementable Element of the U1 of C
f2 is left_complementable right_complementable complementable Element of the U1 of C
(Y,C,V) /. c is left_complementable right_complementable complementable Element of the U1 of C
f2 is left_complementable right_complementable complementable Element of the U1 of C
X is set
Y is non empty set
C is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of C is non empty set
K20(Y, the U1 of C) is set
K19(K20(Y, the U1 of C)) is set
V is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
V | X is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
dom V is Element of K19(Y)
K19(Y) is set
X /\ (dom V) is Element of K19(Y)
f1 is left_complementable right_complementable complementable Element of the U1 of C
||.f1.|| is ext-real non negative V25() real Element of REAL
the U8 of C is V1() V4( the U1 of C) V5( REAL ) V6() non empty total V30( the U1 of C, REAL ) V36() V37() V38() Element of K19(K20( the U1 of C,REAL))
K20( the U1 of C,REAL) is V36() V37() V38() set
K19(K20( the U1 of C,REAL)) is set
the U8 of C . f1 is ext-real V25() real Element of REAL
c is Element of Y
V /. c is left_complementable right_complementable complementable Element of the U1 of C
||.(V /. c).|| is ext-real non negative V25() real Element of REAL
the U8 of C . (V /. c) is ext-real V25() real Element of REAL
f2 is ext-real non negative V25() real Element of REAL
f2 is ext-real non negative V25() real Element of REAL
X is set
Y is non empty set
C is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of C is non empty set
K20(Y, the U1 of C) is set
K19(K20(Y, the U1 of C)) is set
V is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
V | X is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,V) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
||.V.|| is V1() V4(Y) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(Y,REAL))
K20(Y,REAL) is V36() V37() V38() set
K19(K20(Y,REAL)) is set
||.V.|| | X is V1() V4(Y) V5( REAL ) V6() V36() V37() V38() Element of K19(K20(Y,REAL))
f1 is ext-real V25() real Element of REAL
(Y,C,V,f1) is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,V,f1) | X is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
(Y,C,V) | X is V1() V4(Y) V5( the U1 of C) V6() Element of K19(K20(Y, the U1 of C))
X is set
Y is set
X /\ Y is set
C is non empty set
V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of V is non empty set
K20(C, the U1 of V) is set
K19(K20(C, the U1 of V)) is set
f1 is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
f2 is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
f2 | Y is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
(C,V,f1,f2) is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
X is set
Y is set
X /\ Y is set
C is non empty set
V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() V126() V127() RealNormSpace-like NORMSTR
the U1 of V is non empty set
K20(C, the U1 of V) is set
K19(K20(C, the U1 of V)) is set
f1 is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
f2 is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
f2 | Y is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
(C,V,f1,f2) is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
(C,V,f2,f1) is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
(C,V,f2) is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
(C,V,f1,(C,V,f2)) is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
(C,V,f1) is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
(C,V,f2,(C,V,f1)) is V1() V4(C) V5( the U1 of V) V6() Element of K19(K20(C, the U1 of V))
Y /\ X is set