let V be RealLinearSpace; :: thesis: for X being Subspace of V
for v being VECTOR of V st not v in the carrier of X holds
for q being Banach-Functional of V
for fi being linear-Functional of X st ( for x being VECTOR of X
for v being VECTOR of V st x = v holds
fi . x <= q . v ) holds
ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & ( for x being VECTOR of (X + (Lin {v}))
for v being VECTOR of V st x = v holds
psi . x <= q . v ) )
let X be Subspace of V; :: thesis: for v being VECTOR of V st not v in the carrier of X holds
for q being Banach-Functional of V
for fi being linear-Functional of X st ( for x being VECTOR of X
for v being VECTOR of V st x = v holds
fi . x <= q . v ) holds
ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & ( for x being VECTOR of (X + (Lin {v}))
for v being VECTOR of V st x = v holds
psi . x <= q . v ) )
let v be VECTOR of V; :: thesis: ( not v in the carrier of X implies for q being Banach-Functional of V
for fi being linear-Functional of X st ( for x being VECTOR of X
for v being VECTOR of V st x = v holds
fi . x <= q . v ) holds
ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & ( for x being VECTOR of (X + (Lin {v}))
for v being VECTOR of V st x = v holds
psi . x <= q . v ) ) )
assume not v in the carrier of X ; :: thesis: for q being Banach-Functional of V
for fi being linear-Functional of X st ( for x being VECTOR of X
for v being VECTOR of V st x = v holds
fi . x <= q . v ) holds
ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & ( for x being VECTOR of (X + (Lin {v}))
for v being VECTOR of V st x = v holds
psi . x <= q . v ) )
then A1: not v in X ;
v in Lin {v} by RLVECT_4:9;
then A2: v in the carrier of (Lin {v}) ;
the carrier of (Lin {v}) c= the carrier of ((Lin {v}) + X) by Th1;
then reconsider x0 = v as VECTOR of (X + (Lin {v})) by A2, RLSUB_2:5;
set x1 = the VECTOR of X;
let q be Banach-Functional of V; :: thesis: for fi being linear-Functional of X st ( for x being VECTOR of X
for v being VECTOR of V st x = v holds
fi . x <= q . v ) holds
ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & ( for x being VECTOR of (X + (Lin {v}))
for v being VECTOR of V st x = v holds
psi . x <= q . v ) )
let fi be linear-Functional of X; :: thesis: ( ( for x being VECTOR of X
for v being VECTOR of V st x = v holds
fi . x <= q . v ) implies ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & ( for x being VECTOR of (X + (Lin {v}))
for v being VECTOR of V st x = v holds
psi . x <= q . v ) ) )
assume A3: for x being VECTOR of X
for v being VECTOR of V st x = v holds
fi . x <= q . v ; :: thesis: ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & ( for x being VECTOR of (X + (Lin {v}))
for v being VECTOR of V st x = v holds
psi . x <= q . v ) )
set A = { ((fi . x) - (q . (y - v))) where x is VECTOR of X, y is VECTOR of V : x = y } ;
set B = { ((fi . x) + (q . (v - y))) where x is VECTOR of X, y is VECTOR of V : x = y } ;

A4: now :: thesis: for x1, x2 being VECTOR of X
for y1, y2 being VECTOR of V st x1 = y1 & x2 = y2 holds
(fi . x1) - (q . (y1 - v)) <= (fi . x2) + (q . (v - y2))

let x1, x2 be VECTOR of X; :: thesis: for y1, y2 being VECTOR of V st x1 = y1 & x2 = y2 holds
(fi . x1) - (q . (y1 - v)) <= (fi . x2) + (q . (v - y2))
let y1, y2 be VECTOR of V; :: thesis: ( x1 = y1 & x2 = y2 implies (fi . x1) - (q . (y1 - v)) <= (fi . x2) + (q . (v - y2)) )
assume ( x1 = y1 & x2 = y2 ) ; :: thesis: (fi . x1) - (q . (y1 - v)) <= (fi . x2) + (q . (v - y2))
then fi . (x1 - x2) <= q . (y1 - y2) by A3, RLSUB_1:16;
then A5: (fi . x1) - (fi . x2) <= q . (y1 - y2) by Th19;
y1 - y2 = (y1 + (0. V)) + (- y2)
.= (y1 + ((- v) + v)) + (- y2) by RLVECT_1:5
.= ((y1 - v) + v) + (- y2) by RLVECT_1:def 3
.= (y1 - v) + (v - y2) by RLVECT_1:def 3 ;
then q . (y1 - y2) <= (q . (y1 - v)) + (q . (v - y2)) by Def1;
then (fi . x1) - (fi . x2) <= (q . (v - y2)) + (q . (y1 - v)) by A5, XXREAL_0:2;
then fi . x1 <= (fi . x2) + ((q . (v - y2)) + (q . (y1 - v))) by XREAL_1:20;
then fi . x1 <= ((fi . x2) + (q . (v - y2))) + (q . (y1 - v)) ;
hence (fi . x1) - (q . (y1 - v)) <= (fi . x2) + (q . (v - y2)) by XREAL_1:20; :: thesis: verum

end;

A6: now :: thesis: for a, b being ExtReal st a in { ((fi . x) - (q . (y - v))) where x is VECTOR of X, y is VECTOR of V : x = y } & b in { ((fi . x) + (q . (v - y))) where x is VECTOR of X, y is VECTOR of V : x = y } holds
a <= b

let a, b be ExtReal; :: thesis: ( a in { ((fi . x) - (q . (y - v))) where x is VECTOR of X, y is VECTOR of V : x = y } & b in { ((fi . x) + (q . (v - y))) where x is VECTOR of X, y is VECTOR of V : x = y } implies a <= b )
assume a in { ((fi . x) - (q . (y - v))) where x is VECTOR of X, y is VECTOR of V : x = y } ; :: thesis: ( b in { ((fi . x) + (q . (v - y))) where x is VECTOR of X, y is VECTOR of V : x = y } implies a <= b )
then A7: ex x1 being VECTOR of X ex y1 being VECTOR of V st
( a = (fi . x1) - (q . (y1 - v)) & x1 = y1 ) ;
assume b in { ((fi . x) + (q . (v - y))) where x is VECTOR of X, y is VECTOR of V : x = y } ; :: thesis: a <= b
then ex x2 being VECTOR of X ex y2 being VECTOR of V st
( b = (fi . x2) + (q . (v - y2)) & x2 = y2 ) ;
hence a <= b by A4, A7; :: thesis: verum

end;

reconsider v1 = the VECTOR of X as VECTOR of V by RLSUB_1:10;
A8: { ((fi . x) - (q . (y - v))) where x is VECTOR of X, y is VECTOR of V : x = y } c= REAL

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((fi . x) - (q . (y - v))) where x is VECTOR of X, y is VECTOR of V : x = y } or a in REAL )
assume a in { ((fi . x) - (q . (y - v))) where x is VECTOR of X, y is VECTOR of V : x = y } ; :: thesis: a in REAL
then ex x being VECTOR of X ex y being VECTOR of V st
( a = (fi . x) - (q . (y - v)) & x = y ) ;
hence a in REAL ; :: thesis: verum

end;

A9: { ((fi . x) + (q . (v - y))) where x is VECTOR of X, y is VECTOR of V : x = y } c= REAL

proof

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in { ((fi . x) + (q . (v - y))) where x is VECTOR of X, y is VECTOR of V : x = y } or b in REAL )
assume b in { ((fi . x) + (q . (v - y))) where x is VECTOR of X, y is VECTOR of V : x = y } ; :: thesis: b in REAL
then ex x being VECTOR of X ex y being VECTOR of V st
( b = (fi . x) + (q . (v - y)) & x = y ) ;
hence b in REAL ; :: thesis: verum

end;

( (fi . the VECTOR of X) - (q . (v1 - v)) in { ((fi . x) - (q . (y - v))) where x is VECTOR of X, y is VECTOR of V : x = y } & (fi . the VECTOR of X) + (q . (v - v1)) in { ((fi . x) + (q . (v - y))) where x is VECTOR of X, y is VECTOR of V : x = y } ) ;
then reconsider A = { ((fi . x) - (q . (y - v))) where x is VECTOR of X, y is VECTOR of V : x = y } , B = { ((fi . x) + (q . (v - y))) where x is VECTOR of X, y is VECTOR of V : x = y } as non empty Subset of ExtREAL by A8, A9, NUMBERS:31, XBOOLE_1:1;
A10: sup A <= inf B by A6, XXREAL_2:96;
A11: A is bounded_above

proof

set b = the Element of B;
reconsider b = the Element of B as Real by A9;
take b ; :: according to XXREAL_2:def 10 :: thesis: b is UpperBound of A
let x be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not x in A or x <= b )
thus ( not x in A or x <= b ) by A6; :: thesis: verum

end;

A <> {-infty}

proof

set x = the Element of A;
assume A = {-infty} ; :: thesis: contradiction
then the Element of A = -infty by TARSKI:def 1;
hence contradiction by A8; :: thesis: verum

end;

then reconsider r = sup A as Element of REAL by A11, XXREAL_2:57;
consider psi being linear-Functional of (X + (Lin {v})) such that
A12: psi | the carrier of X = fi and
A13: psi . x0 = r by A1, Th21;
take psi ; :: thesis: ( psi | the carrier of X = fi & ( for x being VECTOR of (X + (Lin {v}))
for v being VECTOR of V st x = v holds
psi . x <= q . v ) )
thus psi | the carrier of X = fi by A12; :: thesis: for x being VECTOR of (X + (Lin {v}))
for v being VECTOR of V st x = v holds
psi . x <= q . v
let y be VECTOR of (X + (Lin {v})); :: thesis: for v being VECTOR of V st y = v holds
psi . y <= q . v
let u be VECTOR of V; :: thesis: ( y = u implies psi . y <= q . u )
assume A14: y = u ; :: thesis: psi . y <= q . u
y in X + (Lin {v}) ;
then consider y1, y29 being VECTOR of V such that
A15: y1 in X and
A16: y29 in Lin {v} and
A17: y = y1 + y29 by RLSUB_2:1;
y1 in X + (Lin {v}) by A15, RLSUB_2:2;
then reconsider x = y1 as VECTOR of (X + (Lin {v})) ;
reconsider x1 = x as VECTOR of X by A15;
consider t being Real such that
A18: y29 = t * v by A16, RLVECT_4:8;

per cases ( t = 0 or t > 0 or t < 0 ) ;

suppose t = 0 ; :: thesis: psi . y <= q . u

then y29 = 0. V by A18, RLVECT_1:10;
then A19: y = x1 by A17;
then fi . x1 <= q . u by A3, A14;
hence psi . y <= q . u by A12, A19, FUNCT_1:49; :: thesis: verum

end;

suppose A20: t > 0 ; :: thesis: psi . y <= q . u

reconsider b = (psi . (((- t) ") * x)) + (q . (v - (((- t) ") * y1))) as R_eal by XBOOLE_0:def 3, XXREAL_0:def 4;
A21: v - (((- t) ") * y1) = v - ((- (t ")) * y1) by XCMPLX_1:222
.= v + (- (- ((t ") * y1))) by RLVECT_4:3
.= v + ((t ") * y1) ;
A22: ((- t) ") * x1 = ((- t) ") * y1 by RLSUB_1:14;
then ((- t) ") * x1 = ((- t) ") * x by RLSUB_1:14;
then fi . (((- t) ") * x1) = psi . (((- t) ") * x) by A12, FUNCT_1:49;
then (psi . (((- t) ") * x)) + (q . (v - (((- t) ") * y1))) in B by A22;
then inf B <= b by XXREAL_2:3;
then sup A <= b by A10, XXREAL_0:2;
then psi . (((- t) ") * x) >= r - (q . (v - (((- t) ") * y1))) by XREAL_1:20;
then A23: - (psi . (((- t) ") * x)) <= - (r - (q . (v - (((- t) ") * y1)))) by XREAL_1:24;
- (psi . (((- t) ") * x)) = (- 1) * (psi . (((- t) ") * x))
.= psi . ((- 1) * (((- t) ") * x)) by Def3
.= psi . (((- 1) * ((- t) ")) * x) by RLVECT_1:def 7
.= psi . (((- 1) * (- (t "))) * x) by XCMPLX_1:222
.= psi . ((t ") * x) ;
then A24: psi . ((t ") * x) <= (q . (v + ((t ") * y1))) - r by A23, A21;
(t ") * u = ((t ") * y1) + ((t ") * y29) by A14, A17, RLVECT_1:def 5
.= ((t ") * y1) + (((t ") * t) * v) by A18, RLVECT_1:def 7
.= ((t ") * y1) + (1 * v) by A20, XCMPLX_0:def 7
.= v + ((t ") * y1) by RLVECT_1:def 8 ;
then (psi . ((t ") * x)) + r <= q . ((t ") * u) by A24, XREAL_1:19;
then A25: (psi . ((t ") * x)) + r <= (t ") * (q . u) by A20, Def4;
y29 in X + (Lin {v}) by A16, RLSUB_2:2;
then reconsider y2 = y29 as VECTOR of (X + (Lin {v})) ;
y2 = t * x0 by A18, RLSUB_1:14;
then A26: y = x + (t * x0) by A17, RLSUB_1:13;
A27: t * ((t ") * (q . u)) = (t * (t ")) * (q . u)
.= 1 * (q . u) by A20, XCMPLX_0:def 7
.= q . u ;
psi . (x + (t * x0)) = (psi . x) + (psi . (t * x0)) by Def2
.= 1 * ((psi . x) + (t * (psi . x0))) by Def3
.= (t * (t ")) * ((psi . x) + (t * (psi . x0))) by A20, XCMPLX_0:def 7
.= t * (((t ") * (psi . x)) + (((t ") * t) * (psi . x0)))
.= t * (((t ") * (psi . x)) + (1 * (psi . x0))) by A20, XCMPLX_0:def 7
.= t * ((psi . ((t ") * x)) + r) by A13, Def3 ;
hence psi . y <= q . u by A20, A26, A27, A25, XREAL_1:64; :: thesis: verum

end;

suppose A28: t < 0 ; :: thesis: psi . y <= q . u

- y29 in Lin {v} by A16, RLSUB_1:22;
then - y29 in X + (Lin {v}) by RLSUB_2:2;
then reconsider y2 = - y29 as VECTOR of (X + (Lin {v})) ;
reconsider a = (psi . (((- t) ") * x)) - (q . ((((- t) ") * y1) - v)) as R_eal by XBOOLE_0:def 3, XXREAL_0:def 4;
A29: y = y1 - (- y29) by A17;
A30: - y29 = (- t) * v by A18, RLVECT_4:3;
then y2 = (- t) * x0 by RLSUB_1:14;
then A31: y = x - ((- t) * x0) by A29, RLSUB_1:16;
A32: ((- t) ") * x1 = ((- t) ") * y1 by RLSUB_1:14;
then ((- t) ") * x1 = ((- t) ") * x by RLSUB_1:14;
then fi . (((- t) ") * x1) = psi . (((- t) ") * x) by A12, FUNCT_1:49;
then (psi . (((- t) ") * x)) - (q . ((((- t) ") * y1) - v)) in A by A32;
then a <= sup A by XXREAL_2:4;
then A33: psi . (((- t) ") * x) <= r + (q . ((((- t) ") * y1) - v)) by XREAL_1:20;
A34: - t > 0 by A28, XREAL_1:58;
((- t) ") * u = (((- t) ") * y1) - (((- t) ") * (- y29)) by A14, A29, RLVECT_1:34
.= (((- t) ") * y1) - ((((- t) ") * (- t)) * v) by A30, RLVECT_1:def 7
.= (((- t) ") * y1) - (1 * v) by A34, XCMPLX_0:def 7
.= (((- t) ") * y1) - v by RLVECT_1:def 8 ;
then (psi . (((- t) ") * x)) - r <= q . (((- t) ") * u) by A33, XREAL_1:20;
then A35: (psi . (((- t) ") * x)) - r <= ((- t) ") * (q . u) by A34, Def4;
A36: (- t) * (((- t) ") * (q . u)) = ((- t) * ((- t) ")) * (q . u)
.= 1 * (q . u) by A34, XCMPLX_0:def 7
.= q . u ;
psi . (x - ((- t) * x0)) = (psi . x) - (psi . ((- t) * x0)) by Th19
.= 1 * ((psi . x) - ((- t) * (psi . x0))) by Def3
.= ((- t) * ((- t) ")) * ((psi . x) - ((- t) * (psi . x0))) by A34, XCMPLX_0:def 7
.= (- t) * ((((- t) ") * (psi . x)) - ((((- t) ") * (- t)) * (psi . x0)))
.= (- t) * ((((- t) ") * (psi . x)) - (1 * (psi . x0))) by A34, XCMPLX_0:def 7
.= (- t) * ((psi . (((- t) ") * x)) - r) by A13, Def3 ;
hence psi . y <= q . u by A28, A31, A36, A35, XREAL_1:64; :: thesis: verum

end;

end;