:: HAHNBAN semantic presentation

begin

theorem Th1: :: HAHNBAN:1
for V being RealLinearSpace
for W1, W2 being Subspace of V holds the carrier of W1 c= the carrier of (W1 + W2)
proof
let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V holds the carrier of W1 c= the carrier of (W1 + W2)
let W1, W2 be Subspace of V; ::_thesis: the carrier of W1 c= the carrier of (W1 + W2)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W1 or x in the carrier of (W1 + W2) )
assume A1: x in the carrier of W1 ; ::_thesis: x in the carrier of (W1 + W2)
 the carrier of W1 c= the carrier of V by RLSUB_1:def_2;
then reconsider w = x as VECTOR of V by A1;
A2: ( w + (0. V) = w & 0. V in W2 ) by RLSUB_1:17, RLVECT_1:4;
 x in W1 by A1, STRUCT_0:def_5;
then  x in  {  (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 )  }  by A2;
hence  x in the carrier of (W1 + W2) by RLSUB_2:def_1; ::_thesis: verum
end;

theorem Th2: :: HAHNBAN:2
for V being RealLinearSpace
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v, v1, v2 being VECTOR of V st v1 in W1 & v2 in W2 & v = v1 + v2 holds
v |-- (W1,W2) = [v1,v2]
proof
let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v, v1, v2 being VECTOR of V st v1 in W1 & v2 in W2 & v = v1 + v2 holds
v |-- (W1,W2) = [v1,v2]
let W1, W2 be Subspace of V; ::_thesis: ( V is_the_direct_sum_of W1,W2 implies for v, v1, v2 being VECTOR of V st v1 in W1 & v2 in W2 & v = v1 + v2 holds
v |-- (W1,W2) = [v1,v2] )
assume A1: V is_the_direct_sum_of W1,W2 ; ::_thesis: for v, v1, v2 being VECTOR of V st v1 in W1 & v2 in W2 & v = v1 + v2 holds
v |-- (W1,W2) = [v1,v2]
let v, v1, v2 be VECTOR of V; ::_thesis: ( v1 in W1 & v2 in W2 & v = v1 + v2 implies v |-- (W1,W2) = [v1,v2] )
 ( [v1,v2] `1 = v1 & [v1,v2] `2 = v2 ) by MCART_1:7;
hence  ( v1 in W1 & v2 in W2 & v = v1 + v2 implies v |-- (W1,W2) = [v1,v2] ) by A1, RLSUB_2:def_6; ::_thesis: verum
end;

theorem Th3: :: HAHNBAN:3
for V being RealLinearSpace
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v, v1, v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2] holds
v = v1 + v2
proof
let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v, v1, v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2] holds
v = v1 + v2
let W1, W2 be Subspace of V; ::_thesis: ( V is_the_direct_sum_of W1,W2 implies for v, v1, v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2] holds
v = v1 + v2 )
assume A1: V is_the_direct_sum_of W1,W2 ; ::_thesis: for v, v1, v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2] holds
v = v1 + v2
let v, v1, v2 be VECTOR of V; ::_thesis: ( v |-- (W1,W2) = [v1,v2] implies v = v1 + v2 )
assume  v |-- (W1,W2) = [v1,v2] ; ::_thesis: v = v1 + v2
then  ( (v |-- (W1,W2)) `1 = v1 & (v |-- (W1,W2)) `2 = v2 ) by MCART_1:7;
hence  v = v1 + v2 by A1, RLSUB_2:def_6; ::_thesis: verum
end;

theorem Th4: :: HAHNBAN:4
for V being RealLinearSpace
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v, v1, v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2] holds
( v1 in W1 & v2 in W2 )
proof
let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v, v1, v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2] holds
( v1 in W1 & v2 in W2 )
let W1, W2 be Subspace of V; ::_thesis: ( V is_the_direct_sum_of W1,W2 implies for v, v1, v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2] holds
( v1 in W1 & v2 in W2 ) )
assume A1: V is_the_direct_sum_of W1,W2 ; ::_thesis: for v, v1, v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2] holds
( v1 in W1 & v2 in W2 )
let v, v1, v2 be VECTOR of V; ::_thesis: ( v |-- (W1,W2) = [v1,v2] implies ( v1 in W1 & v2 in W2 ) )
assume  v |-- (W1,W2) = [v1,v2] ; ::_thesis: ( v1 in W1 & v2 in W2 )
then  ( (v |-- (W1,W2)) `1 = v1 & (v |-- (W1,W2)) `2 = v2 ) by MCART_1:7;
hence  ( v1 in W1 & v2 in W2 ) by A1, RLSUB_2:def_6; ::_thesis: verum
end;

theorem Th5: :: HAHNBAN:5
for V being RealLinearSpace
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v, v1, v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2] holds
v |-- (W2,W1) = [v2,v1]
proof
let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v, v1, v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2] holds
v |-- (W2,W1) = [v2,v1]
let W1, W2 be Subspace of V; ::_thesis: ( V is_the_direct_sum_of W1,W2 implies for v, v1, v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2] holds
v |-- (W2,W1) = [v2,v1] )
assume A1: V is_the_direct_sum_of W1,W2 ; ::_thesis: for v, v1, v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2] holds
v |-- (W2,W1) = [v2,v1]
let v, v1, v2 be VECTOR of V; ::_thesis: ( v |-- (W1,W2) = [v1,v2] implies v |-- (W2,W1) = [v2,v1] )
assume A2: v |-- (W1,W2) = [v1,v2] ; ::_thesis: v |-- (W2,W1) = [v2,v1]
then A3: (v |-- (W1,W2)) `1 = v1 by MCART_1:7;
then A4: v1 in W1 by A1, RLSUB_2:def_6;
A5: (v |-- (W1,W2)) `2 = v2 by A2, MCART_1:7;
then A6: v2 in W2 by A1, RLSUB_2:def_6;
 v = v2 + v1 by A1, A3, A5, RLSUB_2:def_6;
hence  v |-- (W2,W1) = [v2,v1] by A1, A4, A6, Th2, RLSUB_2:38; ::_thesis: verum
end;

theorem Th6: :: HAHNBAN:6
for V being RealLinearSpace
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v being VECTOR of V st v in W1 holds
v |-- (W1,W2) = [v,(0. V)]
proof
let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v being VECTOR of V st v in W1 holds
v |-- (W1,W2) = [v,(0. V)]
let W1, W2 be Subspace of V; ::_thesis: ( V is_the_direct_sum_of W1,W2 implies for v being VECTOR of V st v in W1 holds
v |-- (W1,W2) = [v,(0. V)] )
assume A1: V is_the_direct_sum_of W1,W2 ; ::_thesis: for v being VECTOR of V st v in W1 holds
v |-- (W1,W2) = [v,(0. V)]
let v be VECTOR of V; ::_thesis: ( v in W1 implies v |-- (W1,W2) = [v,(0. V)] )
assume A2: v in W1 ; ::_thesis: v |-- (W1,W2) = [v,(0. V)]
 ( 0. V in W2 & v + (0. V) = v ) by RLSUB_1:17, RLVECT_1:4;
hence  v |-- (W1,W2) = [v,(0. V)] by A1, A2, Th2; ::_thesis: verum
end;

theorem Th7: :: HAHNBAN:7
for V being RealLinearSpace
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v being VECTOR of V st v in W2 holds
v |-- (W1,W2) = [(0. V),v]
proof
let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v being VECTOR of V st v in W2 holds
v |-- (W1,W2) = [(0. V),v]
let W1, W2 be Subspace of V; ::_thesis: ( V is_the_direct_sum_of W1,W2 implies for v being VECTOR of V st v in W2 holds
v |-- (W1,W2) = [(0. V),v] )
assume A1: V is_the_direct_sum_of W1,W2 ; ::_thesis: for v being VECTOR of V st v in W2 holds
v |-- (W1,W2) = [(0. V),v]
let v be VECTOR of V; ::_thesis: ( v in W2 implies v |-- (W1,W2) = [(0. V),v] )
assume  v in W2 ; ::_thesis: v |-- (W1,W2) = [(0. V),v]
then  v |-- (W2,W1) = [v,(0. V)] by A1, Th6, RLSUB_2:38;
hence  v |-- (W1,W2) = [(0. V),v] by A1, Th5, RLSUB_2:38; ::_thesis: verum
end;

theorem Th8: :: HAHNBAN:8
for V being RealLinearSpace
for V1 being Subspace of V
for W1 being Subspace of V1
for v being VECTOR of V st v in W1 holds
v is VECTOR of V1
proof
let V be RealLinearSpace; ::_thesis: for V1 being Subspace of V
for W1 being Subspace of V1
for v being VECTOR of V st v in W1 holds
v is VECTOR of V1
let V1 be Subspace of V; ::_thesis: for W1 being Subspace of V1
for v being VECTOR of V st v in W1 holds
v is VECTOR of V1
let W1 be Subspace of V1; ::_thesis: for v being VECTOR of V st v in W1 holds
v is VECTOR of V1
let v be VECTOR of V; ::_thesis: ( v in W1 implies v is VECTOR of V1 )
assume  v in W1 ; ::_thesis: v is VECTOR of V1
then  ( the carrier of W1 c= the carrier of V1 & v in the carrier of W1 ) by RLSUB_1:def_2, STRUCT_0:def_5;
hence  v is VECTOR of V1 ; ::_thesis: verum
end;

theorem Th9: :: HAHNBAN:9
for V being RealLinearSpace
for V1, V2, W being Subspace of V
for W1, W2 being Subspace of W st W1 = V1 & W2 = V2 holds
W1 + W2 = V1 + V2
proof
let V be RealLinearSpace; ::_thesis: for V1, V2, W being Subspace of V
for W1, W2 being Subspace of W st W1 = V1 & W2 = V2 holds
W1 + W2 = V1 + V2
let V1, V2, W be Subspace of V; ::_thesis: for W1, W2 being Subspace of W st W1 = V1 & W2 = V2 holds
W1 + W2 = V1 + V2
let W1, W2 be Subspace of W; ::_thesis: ( W1 = V1 & W2 = V2 implies W1 + W2 = V1 + V2 )
assume A1: ( W1 = V1 & W2 = V2 ) ; ::_thesis: W1 + W2 = V1 + V2
reconsider W3 = W1 + W2 as Subspace of V by RLSUB_1:27;
now__::_thesis:_for_v_being_VECTOR_of_V_holds_
(_(_v_in_W3_implies_v_in_V1_+_V2_)_&_(_v_in_V1_+_V2_implies_v_in_W3_)_)
let v be VECTOR of V; ::_thesis: ( ( v in W3 implies v in V1 + V2 ) & ( v in V1 + V2 implies v in W3 ) )
A2: ( the carrier of W1 c= the carrier of W & the carrier of W2 c= the carrier of W ) by RLSUB_1:def_2;
hereby  ::_thesis: ( v in V1 + V2 implies v in W3 )
assume A3: v in W3 ; ::_thesis: v in V1 + V2
then reconsider w = v as VECTOR of W by Th8;
consider w1, w2 being VECTOR of W such that
A4: ( w1 in W1 & w2 in W2 ) and
A5: w = w1 + w2 by A3, RLSUB_2:1;
reconsider v1 = w1, v2 = w2 as VECTOR of V by RLSUB_1:10;
 v = v1 + v2 by A5, RLSUB_1:13;
hence  v in V1 + V2 by A1, A4, RLSUB_2:1; ::_thesis: verum
end;
assume  v in V1 + V2 ; ::_thesis: v in W3
then consider v1, v2 being VECTOR of V such that
A6: ( v1 in V1 & v2 in V2 ) and
A7: v = v1 + v2 by RLSUB_2:1;
 ( v1 in the carrier of W1 & v2 in the carrier of W2 ) by A1, A6, STRUCT_0:def_5;
then reconsider w1 = v1, w2 = v2 as VECTOR of W by A2;
 v = w1 + w2 by A7, RLSUB_1:13;
hence  v in W3 by A1, A6, RLSUB_2:1; ::_thesis: verum
end;
hence  W1 + W2 = V1 + V2 by RLSUB_1:31; ::_thesis: verum
end;

theorem Th10: :: HAHNBAN:10
for V being RealLinearSpace
for W being Subspace of V
for v being VECTOR of V
for w being VECTOR of W st v = w holds
Lin {w} = Lin {v}
proof
let V be RealLinearSpace; ::_thesis: for W being Subspace of V
for v being VECTOR of V
for w being VECTOR of W st v = w holds
Lin {w} = Lin {v}
let W be Subspace of V; ::_thesis: for v being VECTOR of V
for w being VECTOR of W st v = w holds
Lin {w} = Lin {v}
let v be VECTOR of V; ::_thesis: for w being VECTOR of W st v = w holds
Lin {w} = Lin {v}
let w be VECTOR of W; ::_thesis: ( v = w implies Lin {w} = Lin {v} )
assume A1: v = w ; ::_thesis: Lin {w} = Lin {v}
reconsider W1 = Lin {w} as Subspace of V by RLSUB_1:27;
now__::_thesis:_for_u_being_VECTOR_of_V_holds_
(_(_u_in_W1_implies_u_in_Lin_{v}_)_&_(_u_in_Lin_{v}_implies_u_in_W1_)_)
let u be VECTOR of V; ::_thesis: ( ( u in W1 implies u in Lin {v} ) & ( u in Lin {v} implies u in W1 ) )
hereby  ::_thesis: ( u in Lin {v} implies u in W1 )
assume  u in W1 ; ::_thesis: u in Lin {v}
then consider a being Real such that
A2: u = a * w by RLVECT_4:8;
 u = a * v by A1, A2, RLSUB_1:14;
hence  u in Lin {v} by RLVECT_4:8; ::_thesis: verum
end;
assume  u in Lin {v} ; ::_thesis: u in W1
then consider a being Real such that
A3: u = a * v by RLVECT_4:8;
 u = a * w by A1, A3, RLSUB_1:14;
hence  u in W1 by RLVECT_4:8; ::_thesis: verum
end;
hence  Lin {w} = Lin {v} by RLSUB_1:31; ::_thesis: verum
end;

theorem Th11: :: HAHNBAN:11
for V being RealLinearSpace
for v being VECTOR of V
for X being Subspace of V st not v in X holds
for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & W = X holds
X + (Lin {v}) is_the_direct_sum_of W, Lin {y}
proof
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V
for X being Subspace of V st not v in X holds
for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & W = X holds
X + (Lin {v}) is_the_direct_sum_of W, Lin {y}
let v be VECTOR of V; ::_thesis: for X being Subspace of V st not v in X holds
for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & W = X holds
X + (Lin {v}) is_the_direct_sum_of W, Lin {y}
let X be Subspace of V; ::_thesis: ( not v in X implies for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & W = X holds
X + (Lin {v}) is_the_direct_sum_of W, Lin {y} )
assume A1: not v in X ; ::_thesis: for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & W = X holds
X + (Lin {v}) is_the_direct_sum_of W, Lin {y}
let y be VECTOR of (X + (Lin {v})); ::_thesis: for W being Subspace of X + (Lin {v}) st v = y & W = X holds
X + (Lin {v}) is_the_direct_sum_of W, Lin {y}
let W be Subspace of X + (Lin {v}); ::_thesis: ( v = y & W = X implies X + (Lin {v}) is_the_direct_sum_of W, Lin {y} )
assume that
A2: v = y and
A3: W = X ; ::_thesis: X + (Lin {v}) is_the_direct_sum_of W, Lin {y}
 Lin {v} = Lin {y} by A2, Th10;
hence  RLSStruct(# the carrier of (X + (Lin {v})), the ZeroF of (X + (Lin {v})), the addF of (X + (Lin {v})), the Mult of (X + (Lin {v})) #) = W + (Lin {y}) by A3, Th9; :: according to RLSUB_2:def_4 ::_thesis: W /\ (Lin {y}) = (0). (X + (Lin {v}))
assume  W /\ (Lin {y}) <> (0). (X + (Lin {v})) ; ::_thesis: contradiction
then consider z being VECTOR of (X + (Lin {v})) such that
A4: ( ( z in W /\ (Lin {y}) & not z in (0). (X + (Lin {v})) ) or ( z in (0). (X + (Lin {v})) & not z in W /\ (Lin {y}) ) ) by RLSUB_1:31;
percases ( ( z in W /\ (Lin {y}) & not z in (0). (X + (Lin {v})) ) or ( not z in W /\ (Lin {y}) & z in (0). (X + (Lin {v})) ) ) by A4;
supposethat A5: z in W /\ (Lin {y}) and
A6: not z in (0). (X + (Lin {v})) ; ::_thesis: contradiction
 z in Lin {y} by A5, RLSUB_2:3;
then consider a being Real such that
A7: z = a * y by RLVECT_4:8;
A8: z in W by A5, RLSUB_2:3;
now__::_thesis:_contradiction
percases ( a = 0 or a <> 0 ) ;
suppose a = 0 ; ::_thesis: contradiction
then  z = 0. (X + (Lin {v})) by A7, RLVECT_1:10;
hence  contradiction by A6, RLSUB_1:17; ::_thesis: verum
end;
supposeA9: a <> 0 ; ::_thesis: contradiction
y = 1 * y by RLVECT_1:def_8
.= ((a ") * a) * y by A9, XCMPLX_0:def_7
.= (a ") * (a * y) by RLVECT_1:def_7 ;
hence  contradiction by A1, A2, A3, A8, A7, RLSUB_1:21; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
supposethat A10: not z in W /\ (Lin {y}) and
A11: z in (0). (X + (Lin {v})) ; ::_thesis: contradiction
 z = 0. (X + (Lin {v})) by A11, RLVECT_3:29;
hence  contradiction by A10, RLSUB_1:17; ::_thesis: verum
end;
end;
end;

theorem Th12: :: HAHNBAN:12
for V being RealLinearSpace
for v being VECTOR of V
for X being Subspace of V
for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
y |-- (W,(Lin {y})) = [(0. W),y]
proof
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V
for X being Subspace of V
for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
y |-- (W,(Lin {y})) = [(0. W),y]
let v be VECTOR of V; ::_thesis: for X being Subspace of V
for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
y |-- (W,(Lin {y})) = [(0. W),y]
let X be Subspace of V; ::_thesis: for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
y |-- (W,(Lin {y})) = [(0. W),y]
let y be VECTOR of (X + (Lin {v})); ::_thesis: for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
y |-- (W,(Lin {y})) = [(0. W),y]
let W be Subspace of X + (Lin {v}); ::_thesis: ( v = y & X = W & not v in X implies y |-- (W,(Lin {y})) = [(0. W),y] )
assume  ( v = y & X = W & not v in X ) ; ::_thesis: y |-- (W,(Lin {y})) = [(0. W),y]
then  X + (Lin {v}) is_the_direct_sum_of W, Lin {y} by Th11;
then  y |-- (W,(Lin {y})) = [(0. (X + (Lin {v}))),y] by Th7, RLVECT_4:9;
hence  y |-- (W,(Lin {y})) = [(0. W),y] by RLSUB_1:11; ::_thesis: verum
end;

theorem Th13: :: HAHNBAN:13
for V being RealLinearSpace
for v being VECTOR of V
for X being Subspace of V
for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being VECTOR of (X + (Lin {v})) st w in X holds
w |-- (W,(Lin {y})) = [w,(0. V)]
proof
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V
for X being Subspace of V
for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being VECTOR of (X + (Lin {v})) st w in X holds
w |-- (W,(Lin {y})) = [w,(0. V)]
let v be VECTOR of V; ::_thesis: for X being Subspace of V
for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being VECTOR of (X + (Lin {v})) st w in X holds
w |-- (W,(Lin {y})) = [w,(0. V)]
let X be Subspace of V; ::_thesis: for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being VECTOR of (X + (Lin {v})) st w in X holds
w |-- (W,(Lin {y})) = [w,(0. V)]
let y be VECTOR of (X + (Lin {v})); ::_thesis: for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being VECTOR of (X + (Lin {v})) st w in X holds
w |-- (W,(Lin {y})) = [w,(0. V)]
let W be Subspace of X + (Lin {v}); ::_thesis: ( v = y & X = W & not v in X implies for w being VECTOR of (X + (Lin {v})) st w in X holds
w |-- (W,(Lin {y})) = [w,(0. V)] )
assume that
A1: v = y and
A2: X = W and
A3: not v in X ; ::_thesis: for w being VECTOR of (X + (Lin {v})) st w in X holds
w |-- (W,(Lin {y})) = [w,(0. V)]
A4: X + (Lin {v}) is_the_direct_sum_of W, Lin {y} by A1, A2, A3, Th11;
let w be VECTOR of (X + (Lin {v})); ::_thesis: ( w in X implies w |-- (W,(Lin {y})) = [w,(0. V)] )
assume  w in X ; ::_thesis: w |-- (W,(Lin {y})) = [w,(0. V)]
then  w |-- (W,(Lin {y})) = [w,(0. (X + (Lin {v})))] by A2, A4, Th6;
hence  w |-- (W,(Lin {y})) = [w,(0. V)] by RLSUB_1:11; ::_thesis: verum
end;

theorem Th14: :: HAHNBAN:14
for V being RealLinearSpace
for v being VECTOR of V
for W1, W2 being Subspace of V ex v1, v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2]
proof
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V
for W1, W2 being Subspace of V ex v1, v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2]
let v be VECTOR of V; ::_thesis: for W1, W2 being Subspace of V ex v1, v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2]
let W1, W2 be Subspace of V; ::_thesis: ex v1, v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2]
take  (v |-- (W1,W2)) `1 ; ::_thesis: ex v2 being VECTOR of V st v |-- (W1,W2) = [((v |-- (W1,W2)) `1),v2]
take  (v |-- (W1,W2)) `2 ; ::_thesis: v |-- (W1,W2) = [((v |-- (W1,W2)) `1),((v |-- (W1,W2)) `2)]
thus  v |-- (W1,W2) = [((v |-- (W1,W2)) `1),((v |-- (W1,W2)) `2)] by MCART_1:21; ::_thesis: verum
end;

theorem Th15: :: HAHNBAN:15
for V being RealLinearSpace
for v being VECTOR of V
for X being Subspace of V
for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being VECTOR of (X + (Lin {v})) ex x being VECTOR of X ex r being Real st w |-- (W,(Lin {y})) = [x,(r * v)]
proof
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V
for X being Subspace of V
for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being VECTOR of (X + (Lin {v})) ex x being VECTOR of X ex r being Real st w |-- (W,(Lin {y})) = [x,(r * v)]
let v be VECTOR of V; ::_thesis: for X being Subspace of V
for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being VECTOR of (X + (Lin {v})) ex x being VECTOR of X ex r being Real st w |-- (W,(Lin {y})) = [x,(r * v)]
let X be Subspace of V; ::_thesis: for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being VECTOR of (X + (Lin {v})) ex x being VECTOR of X ex r being Real st w |-- (W,(Lin {y})) = [x,(r * v)]
let y be VECTOR of (X + (Lin {v})); ::_thesis: for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being VECTOR of (X + (Lin {v})) ex x being VECTOR of X ex r being Real st w |-- (W,(Lin {y})) = [x,(r * v)]
let W be Subspace of X + (Lin {v}); ::_thesis: ( v = y & X = W & not v in X implies for w being VECTOR of (X + (Lin {v})) ex x being VECTOR of X ex r being Real st w |-- (W,(Lin {y})) = [x,(r * v)] )
assume that
A1: v = y and
A2: X = W and
A3: not v in X ; ::_thesis: for w being VECTOR of (X + (Lin {v})) ex x being VECTOR of X ex r being Real st w |-- (W,(Lin {y})) = [x,(r * v)]
let w be VECTOR of (X + (Lin {v})); ::_thesis: ex x being VECTOR of X ex r being Real st w |-- (W,(Lin {y})) = [x,(r * v)]
consider v1, v2 being VECTOR of (X + (Lin {v})) such that
A4: w |-- (W,(Lin {y})) = [v1,v2] by Th14;
A5: X + (Lin {v}) is_the_direct_sum_of W, Lin {y} by A1, A2, A3, Th11;
then  v1 in W by A4, Th4;
then reconsider x = v1 as VECTOR of X by A2, STRUCT_0:def_5;
 v2 in Lin {y} by A5, A4, Th4;
then consider r being Real such that
A6: v2 = r * y by RLVECT_4:8;
take  x ; ::_thesis: ex r being Real st w |-- (W,(Lin {y})) = [x,(r * v)]
take  r ; ::_thesis: w |-- (W,(Lin {y})) = [x,(r * v)]
thus  w |-- (W,(Lin {y})) = [x,(r * v)] by A1, A4, A6, RLSUB_1:14; ::_thesis: verum
end;

theorem Th16: :: HAHNBAN:16
for V being RealLinearSpace
for v being VECTOR of V
for X being Subspace of V
for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w1, w2 being VECTOR of (X + (Lin {v}))
for x1, x2 being VECTOR of X
for r1, r2 being Real st w1 |-- (W,(Lin {y})) = [x1,(r1 * v)] & w2 |-- (W,(Lin {y})) = [x2,(r2 * v)] holds
(w1 + w2) |-- (W,(Lin {y})) = [(x1 + x2),((r1 + r2) * v)]
proof
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V
for X being Subspace of V
for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w1, w2 being VECTOR of (X + (Lin {v}))
for x1, x2 being VECTOR of X
for r1, r2 being Real st w1 |-- (W,(Lin {y})) = [x1,(r1 * v)] & w2 |-- (W,(Lin {y})) = [x2,(r2 * v)] holds
(w1 + w2) |-- (W,(Lin {y})) = [(x1 + x2),((r1 + r2) * v)]
let v be VECTOR of V; ::_thesis: for X being Subspace of V
for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w1, w2 being VECTOR of (X + (Lin {v}))
for x1, x2 being VECTOR of X
for r1, r2 being Real st w1 |-- (W,(Lin {y})) = [x1,(r1 * v)] & w2 |-- (W,(Lin {y})) = [x2,(r2 * v)] holds
(w1 + w2) |-- (W,(Lin {y})) = [(x1 + x2),((r1 + r2) * v)]
let X be Subspace of V; ::_thesis: for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w1, w2 being VECTOR of (X + (Lin {v}))
for x1, x2 being VECTOR of X
for r1, r2 being Real st w1 |-- (W,(Lin {y})) = [x1,(r1 * v)] & w2 |-- (W,(Lin {y})) = [x2,(r2 * v)] holds
(w1 + w2) |-- (W,(Lin {y})) = [(x1 + x2),((r1 + r2) * v)]
let y be VECTOR of (X + (Lin {v})); ::_thesis: for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w1, w2 being VECTOR of (X + (Lin {v}))
for x1, x2 being VECTOR of X
for r1, r2 being Real st w1 |-- (W,(Lin {y})) = [x1,(r1 * v)] & w2 |-- (W,(Lin {y})) = [x2,(r2 * v)] holds
(w1 + w2) |-- (W,(Lin {y})) = [(x1 + x2),((r1 + r2) * v)]
let W be Subspace of X + (Lin {v}); ::_thesis: ( v = y & X = W & not v in X implies for w1, w2 being VECTOR of (X + (Lin {v}))
for x1, x2 being VECTOR of X
for r1, r2 being Real st w1 |-- (W,(Lin {y})) = [x1,(r1 * v)] & w2 |-- (W,(Lin {y})) = [x2,(r2 * v)] holds
(w1 + w2) |-- (W,(Lin {y})) = [(x1 + x2),((r1 + r2) * v)] )
assume that
A1: v = y and
A2: X = W and
A3: not v in X ; ::_thesis: for w1, w2 being VECTOR of (X + (Lin {v}))
for x1, x2 being VECTOR of X
for r1, r2 being Real st w1 |-- (W,(Lin {y})) = [x1,(r1 * v)] & w2 |-- (W,(Lin {y})) = [x2,(r2 * v)] holds
(w1 + w2) |-- (W,(Lin {y})) = [(x1 + x2),((r1 + r2) * v)]
A4: X + (Lin {v}) is_the_direct_sum_of W, Lin {y} by A1, A2, A3, Th11;
let w1, w2 be VECTOR of (X + (Lin {v})); ::_thesis: for x1, x2 being VECTOR of X
for r1, r2 being Real st w1 |-- (W,(Lin {y})) = [x1,(r1 * v)] & w2 |-- (W,(Lin {y})) = [x2,(r2 * v)] holds
(w1 + w2) |-- (W,(Lin {y})) = [(x1 + x2),((r1 + r2) * v)]
let x1, x2 be VECTOR of X; ::_thesis: for r1, r2 being Real st w1 |-- (W,(Lin {y})) = [x1,(r1 * v)] & w2 |-- (W,(Lin {y})) = [x2,(r2 * v)] holds
(w1 + w2) |-- (W,(Lin {y})) = [(x1 + x2),((r1 + r2) * v)]
let r1, r2 be Real; ::_thesis: ( w1 |-- (W,(Lin {y})) = [x1,(r1 * v)] & w2 |-- (W,(Lin {y})) = [x2,(r2 * v)] implies (w1 + w2) |-- (W,(Lin {y})) = [(x1 + x2),((r1 + r2) * v)] )
assume that
A5: w1 |-- (W,(Lin {y})) = [x1,(r1 * v)] and
A6: w2 |-- (W,(Lin {y})) = [x2,(r2 * v)] ; ::_thesis: (w1 + w2) |-- (W,(Lin {y})) = [(x1 + x2),((r1 + r2) * v)]
reconsider y1 = x1, y2 = x2 as VECTOR of (X + (Lin {v})) by A2, RLSUB_1:10;
A7: r2 * v = r2 * y by A1, RLSUB_1:14;
then A8: y2 in W by A4, A6, Th4;
 (r1 + r2) * v = (r1 + r2) * y by A1, RLSUB_1:14;
then A9: (r1 + r2) * v in Lin {y} by RLVECT_4:8;
reconsider z1 = x1, z2 = x2 as VECTOR of V by RLSUB_1:10;
A10: y1 + y2 = z1 + z2 by RLSUB_1:13
.= x1 + x2 by RLSUB_1:13 ;
A11: r1 * v = r1 * y by A1, RLSUB_1:14;
then  y1 in W by A4, A5, Th4;
then A12: y1 + y2 in W by A8, RLSUB_1:20;
A13: w2 = y2 + (r2 * y) by A4, A6, A7, Th3;
 w1 = y1 + (r1 * y) by A4, A5, A11, Th3;
then A14: w1 + w2 = ((y1 + (r1 * y)) + y2) + (r2 * y) by A13, RLVECT_1:def_3
.= ((y1 + y2) + (r1 * y)) + (r2 * y) by RLVECT_1:def_3
.= (y1 + y2) + ((r1 * y) + (r2 * y)) by RLVECT_1:def_3
.= (y1 + y2) + ((r1 + r2) * y) by RLVECT_1:def_6 ;
 (r1 + r2) * y = (r1 + r2) * v by A1, RLSUB_1:14;
hence  (w1 + w2) |-- (W,(Lin {y})) = [(x1 + x2),((r1 + r2) * v)] by A4, A12, A9, A14, A10, Th2; ::_thesis: verum
end;

theorem Th17: :: HAHNBAN:17
for V being RealLinearSpace
for v being VECTOR of V
for X being Subspace of V
for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being VECTOR of (X + (Lin {v}))
for x being VECTOR of X
for t, r being Real st w |-- (W,(Lin {y})) = [x,(r * v)] holds
(t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)]
proof
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V
for X being Subspace of V
for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being VECTOR of (X + (Lin {v}))
for x being VECTOR of X
for t, r being Real st w |-- (W,(Lin {y})) = [x,(r * v)] holds
(t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)]
let v be VECTOR of V; ::_thesis: for X being Subspace of V
for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being VECTOR of (X + (Lin {v}))
for x being VECTOR of X
for t, r being Real st w |-- (W,(Lin {y})) = [x,(r * v)] holds
(t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)]
let X be Subspace of V; ::_thesis: for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being VECTOR of (X + (Lin {v}))
for x being VECTOR of X
for t, r being Real st w |-- (W,(Lin {y})) = [x,(r * v)] holds
(t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)]
let y be VECTOR of (X + (Lin {v})); ::_thesis: for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being VECTOR of (X + (Lin {v}))
for x being VECTOR of X
for t, r being Real st w |-- (W,(Lin {y})) = [x,(r * v)] holds
(t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)]
let W be Subspace of X + (Lin {v}); ::_thesis: ( v = y & X = W & not v in X implies for w being VECTOR of (X + (Lin {v}))
for x being VECTOR of X
for t, r being Real st w |-- (W,(Lin {y})) = [x,(r * v)] holds
(t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)] )
assume that
A1: v = y and
A2: X = W and
A3: not v in X ; ::_thesis: for w being VECTOR of (X + (Lin {v}))
for x being VECTOR of X
for t, r being Real st w |-- (W,(Lin {y})) = [x,(r * v)] holds
(t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)]
A4: X + (Lin {v}) is_the_direct_sum_of W, Lin {y} by A1, A2, A3, Th11;
let w be VECTOR of (X + (Lin {v})); ::_thesis: for x being VECTOR of X
for t, r being Real st w |-- (W,(Lin {y})) = [x,(r * v)] holds
(t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)]
let x be VECTOR of X; ::_thesis: for t, r being Real st w |-- (W,(Lin {y})) = [x,(r * v)] holds
(t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)]
let t, r be Real; ::_thesis: ( w |-- (W,(Lin {y})) = [x,(r * v)] implies (t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)] )
assume A5: w |-- (W,(Lin {y})) = [x,(r * v)] ; ::_thesis: (t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)]
reconsider z = x as VECTOR of (X + (Lin {v})) by A2, RLSUB_1:10;
 r * y = r * v by A1, RLSUB_1:14;
then A6: t * w = t * (z + (r * y)) by A4, A5, Th3
.= (t * z) + (t * (r * y)) by RLVECT_1:def_5
.= (t * z) + ((t * r) * y) by RLVECT_1:def_7 ;
reconsider u = x as VECTOR of V by RLSUB_1:10;
A7: (t * r) * y in Lin {y} by RLVECT_4:8;
A8: (t * r) * y = (t * r) * v by A1, RLSUB_1:14;
A9: t * z = t * u by RLSUB_1:14
.= t * x by RLSUB_1:14 ;
then  t * z in W by A2, STRUCT_0:def_5;
hence  (t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)] by A4, A9, A8, A7, A6, Th2; ::_thesis: verum
end;

begin

definition
let V be RLSStruct ;
mode Functional of V is Function of the carrier of V,REAL;
end;

definition
let V be RealLinearSpace;
let IT be Functional of V;
attrIT is subadditive  means :Def1: :: HAHNBAN:def 1
 for x, y being VECTOR of V holds IT . (x + y) <= (IT . x) + (IT . y);
attrIT is additive  means :Def2: :: HAHNBAN:def 2
 for x, y being VECTOR of V holds IT . (x + y) = (IT . x) + (IT . y);
attrIT is homogeneous  means :Def3: :: HAHNBAN:def 3
 for x being VECTOR of V
for r being Real holds IT . (r * x) = r * (IT . x);
attrIT is positively_homogeneous  means :Def4: :: HAHNBAN:def 4
 for x being VECTOR of V
for r being Real st r > 0 holds
IT . (r * x) = r * (IT . x);
attrIT is semi-homogeneous  means :Def5: :: HAHNBAN:def 5
 for x being VECTOR of V
for r being Real st r >= 0 holds
IT . (r * x) = r * (IT . x);
attrIT is absolutely_homogeneous  means :Def6: :: HAHNBAN:def 6
 for x being VECTOR of V
for r being Real holds IT . (r * x) = (abs r) * (IT . x);
attrIT is 0-preserving  means :Def7: :: HAHNBAN:def 7
IT . (0. V) = 0 ;
end;

:: deftheorem Def1 defines subadditive HAHNBAN:def_1_:_
 for V being RealLinearSpace
for IT being Functional of V holds
( IT is subadditive iff for x, y being VECTOR of V holds IT . (x + y) <= (IT . x) + (IT . y) );

:: deftheorem Def2 defines additive HAHNBAN:def_2_:_
 for V being RealLinearSpace
for IT being Functional of V holds
( IT is additive iff for x, y being VECTOR of V holds IT . (x + y) = (IT . x) + (IT . y) );

:: deftheorem Def3 defines homogeneous HAHNBAN:def_3_:_
 for V being RealLinearSpace
for IT being Functional of V holds
( IT is homogeneous iff for x being VECTOR of V
for r being Real holds IT . (r * x) = r * (IT . x) );

:: deftheorem Def4 defines positively_homogeneous HAHNBAN:def_4_:_
 for V being RealLinearSpace
for IT being Functional of V holds
( IT is positively_homogeneous iff for x being VECTOR of V
for r being Real st r > 0 holds
IT . (r * x) = r * (IT . x) );

:: deftheorem Def5 defines semi-homogeneous HAHNBAN:def_5_:_
 for V being RealLinearSpace
for IT being Functional of V holds
( IT is semi-homogeneous iff for x being VECTOR of V
for r being Real st r >= 0 holds
IT . (r * x) = r * (IT . x) );

:: deftheorem Def6 defines absolutely_homogeneous HAHNBAN:def_6_:_
 for V being RealLinearSpace
for IT being Functional of V holds
( IT is absolutely_homogeneous iff for x being VECTOR of V
for r being Real holds IT . (r * x) = (abs r) * (IT . x) );

:: deftheorem Def7 defines 0-preserving HAHNBAN:def_7_:_
 for V being RealLinearSpace
for IT being Functional of V holds
( IT is 0-preserving iff IT . (0. V) = 0 );

registration
let V be RealLinearSpace;
cluster Function-like V18( the carrier of V, REAL ) additive  ->  subadditive for Element of bool [: the carrier of V,REAL:];
coherence
 for b1 being Functional of V st b1 is additive holds
b1 is subadditive
proof
let f be Functional of V; ::_thesis: ( f is additive implies f is subadditive )
assume A1: f is additive ; ::_thesis: f is subadditive
let x, y be VECTOR of V; :: according to HAHNBAN:def_1 ::_thesis: f . (x + y) <= (f . x) + (f . y)
thus  f . (x + y) <= (f . x) + (f . y) by A1, Def2; ::_thesis: verum
end;
cluster Function-like V18( the carrier of V, REAL ) homogeneous  ->  positively_homogeneous for Element of bool [: the carrier of V,REAL:];
coherence
 for b1 being Functional of V st b1 is homogeneous holds
b1 is positively_homogeneous
proof
let f be Functional of V; ::_thesis: ( f is homogeneous implies f is positively_homogeneous )
assume A2: f is homogeneous ; ::_thesis: f is positively_homogeneous
let x be VECTOR of V; :: according to HAHNBAN:def_4 ::_thesis: for r being Real st r > 0 holds
f . (r * x) = r * (f . x)
let r be Real; ::_thesis: ( r > 0 implies f . (r * x) = r * (f . x) )
thus  ( r > 0 implies f . (r * x) = r * (f . x) ) by A2, Def3; ::_thesis: verum
end;
cluster Function-like V18( the carrier of V, REAL ) semi-homogeneous  ->  positively_homogeneous for Element of bool [: the carrier of V,REAL:];
coherence
 for b1 being Functional of V st b1 is semi-homogeneous holds
b1 is positively_homogeneous
proof
let f be Functional of V; ::_thesis: ( f is semi-homogeneous implies f is positively_homogeneous )
assume A3: f is semi-homogeneous ; ::_thesis: f is positively_homogeneous
let x be VECTOR of V; :: according to HAHNBAN:def_4 ::_thesis: for r being Real st r > 0 holds
f . (r * x) = r * (f . x)
let r be Real; ::_thesis: ( r > 0 implies f . (r * x) = r * (f . x) )
assume  r > 0 ; ::_thesis: f . (r * x) = r * (f . x)
hence  f . (r * x) = r * (f . x) by A3, Def5; ::_thesis: verum
end;
cluster Function-like V18( the carrier of V, REAL ) semi-homogeneous  ->  0-preserving for Element of bool [: the carrier of V,REAL:];
coherence
 for b1 being Functional of V st b1 is semi-homogeneous holds
b1 is 0-preserving
proof
let f be Functional of V; ::_thesis: ( f is semi-homogeneous implies f is 0-preserving )
assume A4: f is semi-homogeneous ; ::_thesis: f is 0-preserving
thus f . (0. V) = f . (0 * (0. V)) by RLVECT_1:10
.= 0 * (f . (0. V)) by A4, Def5
.= 0 ; :: according to HAHNBAN:def_7 ::_thesis: verum
end;
cluster Function-like V18( the carrier of V, REAL ) absolutely_homogeneous  ->  semi-homogeneous for Element of bool [: the carrier of V,REAL:];
coherence
 for b1 being Functional of V st b1 is absolutely_homogeneous holds
b1 is semi-homogeneous
proof
let f be Functional of V; ::_thesis: ( f is absolutely_homogeneous implies f is semi-homogeneous )
assume A5: f is absolutely_homogeneous ; ::_thesis: f is semi-homogeneous
let x be VECTOR of V; :: according to HAHNBAN:def_5 ::_thesis: for r being Real st r >= 0 holds
f . (r * x) = r * (f . x)
let r be Real; ::_thesis: ( r >= 0 implies f . (r * x) = r * (f . x) )
assume  r >= 0 ; ::_thesis: f . (r * x) = r * (f . x)
then  abs r = r by ABSVALUE:def_1;
hence  f . (r * x) = r * (f . x) by A5, Def6; ::_thesis: verum
end;
cluster Function-like V18( the carrier of V, REAL ) positively_homogeneous 0-preserving  ->  semi-homogeneous for Element of bool [: the carrier of V,REAL:];
coherence
 for b1 being Functional of V st b1 is 0-preserving & b1 is positively_homogeneous holds
b1 is semi-homogeneous
proof
let f be Functional of V; ::_thesis: ( f is 0-preserving & f is positively_homogeneous implies f is semi-homogeneous )
assume that
A6: f is 0-preserving and
A7: f is positively_homogeneous ; ::_thesis: f is semi-homogeneous
let x be VECTOR of V; :: according to HAHNBAN:def_5 ::_thesis: for r being Real st r >= 0 holds
f . (r * x) = r * (f . x)
let r be Real; ::_thesis: ( r >= 0 implies f . (r * x) = r * (f . x) )
assume A8: r >= 0 ; ::_thesis: f . (r * x) = r * (f . x)
percases ( r = 0 or r > 0 ) by A8;
supposeA9: r = 0 ; ::_thesis: f . (r * x) = r * (f . x)
hence f . (r * x) = f . (0. V) by RLVECT_1:10
.= r * (f . x) by A6, A9, Def7 ;
::_thesis: verum
end;
suppose r > 0 ; ::_thesis: f . (r * x) = r * (f . x)
hence  f . (r * x) = r * (f . x) by A7, Def4; ::_thesis: verum
end;
end;
end;
end;

registration
let V be RealLinearSpace;
cluster Relation-like the carrier of V -defined REAL -valued Function-like non empty total V18( the carrier of V, REAL ) additive homogeneous absolutely_homogeneous for Element of bool [: the carrier of V,REAL:];
existence
 ex b1 being Functional of V st
( b1 is additive & b1 is absolutely_homogeneous & b1 is homogeneous )
proof
reconsider f = the carrier of V --> 0 as Functional of V ;
take  f ; ::_thesis: ( f is additive & f is absolutely_homogeneous & f is homogeneous )
hereby  :: according to HAHNBAN:def_2 ::_thesis: ( f is absolutely_homogeneous & f is homogeneous )
let x, y be VECTOR of V; ::_thesis: f . (x + y) = (f . x) + (f . y)
thus f . (x + y) = 0 + 0 by FUNCOP_1:7
.= (f . x) + 0 by FUNCOP_1:7
.= (f . x) + (f . y) by FUNCOP_1:7 ; ::_thesis: verum
end;
hereby  :: according to HAHNBAN:def_6 ::_thesis: f is homogeneous
let x be VECTOR of V; ::_thesis: for r being Real holds f . (r * x) = (abs r) * (f . x)
let r be Real; ::_thesis: f . (r * x) = (abs r) * (f . x)
thus f . (r * x) = (abs r) * 0 by FUNCOP_1:7
.= (abs r) * (f . x) by FUNCOP_1:7 ; ::_thesis: verum
end;
let x be VECTOR of V; :: according to HAHNBAN:def_3 ::_thesis: for r being Real holds f . (r * x) = r * (f . x)
let r be Real; ::_thesis: f . (r * x) = r * (f . x)
thus f . (r * x) = r * 0 by FUNCOP_1:7
.= r * (f . x) by FUNCOP_1:7 ; ::_thesis: verum
end;
end;

definition
let V be RealLinearSpace;
mode Banach-Functional of V is subadditive positively_homogeneous Functional of V;
mode linear-Functional of V is additive homogeneous Functional of V;
end;

theorem Th18: :: HAHNBAN:18
for V being RealLinearSpace
for L being homogeneous Functional of V
for v being VECTOR of V holds L . (- v) = - (L . v)
proof
let V be RealLinearSpace; ::_thesis: for L being homogeneous Functional of V
for v being VECTOR of V holds L . (- v) = - (L . v)
let L be homogeneous Functional of V; ::_thesis: for v being VECTOR of V holds L . (- v) = - (L . v)
let v be VECTOR of V; ::_thesis: L . (- v) = - (L . v)
thus L . (- v) = L . ((- 1) * v) by RLVECT_1:16
.= (- 1) * (L . v) by Def3
.= - (L . v) ; ::_thesis: verum
end;

theorem Th19: :: HAHNBAN:19
for V being RealLinearSpace
for L being linear-Functional of V
for v1, v2 being VECTOR of V holds L . (v1 - v2) = (L . v1) - (L . v2)
proof
let V be RealLinearSpace; ::_thesis: for L being linear-Functional of V
for v1, v2 being VECTOR of V holds L . (v1 - v2) = (L . v1) - (L . v2)
let L be linear-Functional of V; ::_thesis: for v1, v2 being VECTOR of V holds L . (v1 - v2) = (L . v1) - (L . v2)
let v1, v2 be VECTOR of V; ::_thesis: L . (v1 - v2) = (L . v1) - (L . v2)
thus L . (v1 - v2) = (L . v1) + (L . (- v2)) by Def2
.= (L . v1) + (- (L . v2)) by Th18
.= (L . v1) - (L . v2) ; ::_thesis: verum
end;

theorem Th20: :: HAHNBAN:20
for V being RealLinearSpace
for L being additive Functional of V holds L . (0. V) = 0
proof
let V be RealLinearSpace; ::_thesis: for L being additive Functional of V holds L . (0. V) = 0
let L be additive Functional of V; ::_thesis: L . (0. V) = 0
(L . (0. V)) + 0 = L . ((0. V) + (0. V)) by RLVECT_1:4
.= (L . (0. V)) + (L . (0. V)) by Def2 ;
hence  L . (0. V) = 0 ; ::_thesis: verum
end;

theorem Th21: :: HAHNBAN:21
for V being RealLinearSpace
for X being Subspace of V
for fi being linear-Functional of X
for v being VECTOR of V
for y being VECTOR of (X + (Lin {v})) st v = y & not v in X holds
for r being Real ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & psi . y = r )
proof
let V be RealLinearSpace; ::_thesis: for X being Subspace of V
for fi being linear-Functional of X
for v being VECTOR of V
for y being VECTOR of (X + (Lin {v})) st v = y & not v in X holds
for r being Real ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & psi . y = r )
let X be Subspace of V; ::_thesis: for fi being linear-Functional of X
for v being VECTOR of V
for y being VECTOR of (X + (Lin {v})) st v = y & not v in X holds
for r being Real ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & psi . y = r )
let fi be linear-Functional of X; ::_thesis: for v being VECTOR of V
for y being VECTOR of (X + (Lin {v})) st v = y & not v in X holds
for r being Real ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & psi . y = r )
let v be VECTOR of V; ::_thesis: for y being VECTOR of (X + (Lin {v})) st v = y & not v in X holds
for r being Real ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & psi . y = r )
let y be VECTOR of (X + (Lin {v})); ::_thesis: ( v = y & not v in X implies for r being Real ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & psi . y = r ) )
assume that
A1: v = y and
A2: not v in X ; ::_thesis: for r being Real ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & psi . y = r )
reconsider W1 = X as Subspace of X + (Lin {v}) by RLSUB_2:7;
let r be Real; ::_thesis: ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & psi . y = r )
defpred S1[ VECTOR of (X + (Lin {v})), Real] means  for x being VECTOR of X
for s being Real st ($1 |-- (W1,(Lin {y}))) `1 = x & ($1 |-- (W1,(Lin {y}))) `2 = s * v holds
$2 = (fi . x) + (s * r);
A3: now__::_thesis:_for_e_being_Element_of_(X_+_(Lin_{v}))_ex_u_being_Element_of_REAL_st_S1[e,u]
let e be Element of (X + (Lin {v})); ::_thesis: ex u being Element of REAL st S1[e,u]
consider x being VECTOR of X, s being Real such that
A4: e |-- (W1,(Lin {y})) = [x,(s * v)] by A1, A2, Th15;
take u = (fi . x) + (s * r); ::_thesis: S1[e,u]
thus  S1[e,u] ::_thesis: verum
proof
let x9 be VECTOR of X; ::_thesis: for s being Real st (e |-- (W1,(Lin {y}))) `1 = x9 & (e |-- (W1,(Lin {y}))) `2 = s * v holds
u = (fi . x9) + (s * r)
let t be Real; ::_thesis: ( (e |-- (W1,(Lin {y}))) `1 = x9 & (e |-- (W1,(Lin {y}))) `2 = t * v implies u = (fi . x9) + (t * r) )
assume that
A5: (e |-- (W1,(Lin {y}))) `1 = x9 and
A6: (e |-- (W1,(Lin {y}))) `2 = t * v ; ::_thesis: u = (fi . x9) + (t * r)
 v <> 0. V by A2, RLSUB_1:17;
then  t = s by A4, A6, MCART_1:7, RLVECT_1:37;
hence  u = (fi . x9) + (t * r) by A4, A5, MCART_1:7; ::_thesis: verum
end;
end;
consider f being Function of the carrier of (X + (Lin {v})),REAL such that
A7: for e being VECTOR of (X + (Lin {v})) holds S1[e,f . e] from FUNCT_2:sch_3(A3);
A8: now__::_thesis:_for_a_being_set_st_a_in_dom_fi_holds_
fi_._a_=_f_._a
let a be set ; ::_thesis: ( a in dom fi implies fi . a = f . a )
assume  a in dom fi ; ::_thesis: fi . a = f . a
then reconsider x = a as VECTOR of X by FUNCT_2:def_1;
 the carrier of X c= the carrier of (X + (Lin {v})) by Th1;
then reconsider v1 = x as VECTOR of (X + (Lin {v})) by TARSKI:def_3;
 v1 in X by STRUCT_0:def_5;
then v1 |-- (W1,(Lin {y})) = [v1,(0. V)] by A1, A2, Th13
.= [v1,(0 * v)] by RLVECT_1:10 ;
then A9: ( (v1 |-- (W1,(Lin {y}))) `1 = x & (v1 |-- (W1,(Lin {y}))) `2 = 0 * v ) by MCART_1:7;
thus fi . a = (fi . x) + (0 * r)
.= f . a by A7, A9 ; ::_thesis: verum
end;
reconsider f = f as Functional of (X + (Lin {v})) ;
A10: y |-- (W1,(Lin {y})) = [(0. W1),y] by A1, A2, Th12;
then A11: (y |-- (W1,(Lin {y}))) `1 = 0. X by MCART_1:7;
A12: f is additive
proof
let v1, v2 be VECTOR of (X + (Lin {v})); :: according to HAHNBAN:def_2 ::_thesis: f . (v1 + v2) = (f . v1) + (f . v2)
consider x1 being VECTOR of X, s1 being Real such that
A13: v1 |-- (W1,(Lin {y})) = [x1,(s1 * v)] by A1, A2, Th15;
A14: ( (v1 |-- (W1,(Lin {y}))) `1 = x1 & (v1 |-- (W1,(Lin {y}))) `2 = s1 * v ) by A13, MCART_1:7;
consider x2 being VECTOR of X, s2 being Real such that
A15: v2 |-- (W1,(Lin {y})) = [x2,(s2 * v)] by A1, A2, Th15;
A16: ( (v2 |-- (W1,(Lin {y}))) `1 = x2 & (v2 |-- (W1,(Lin {y}))) `2 = s2 * v ) by A15, MCART_1:7;
 (v1 + v2) |-- (W1,(Lin {y})) = [(x1 + x2),((s1 + s2) * v)] by A1, A2, A13, A15, Th16;
then  ( ((v1 + v2) |-- (W1,(Lin {y}))) `1 = x1 + x2 & ((v1 + v2) |-- (W1,(Lin {y}))) `2 = (s1 + s2) * v ) by MCART_1:7;
hence f . (v1 + v2) = (fi . (x1 + x2)) + ((s1 + s2) * r) by A7
.= ((fi . x1) + (fi . x2)) + ((s1 * r) + (s2 * r)) by Def2
.= ((fi . x1) + (s1 * r)) + ((fi . x2) + (s2 * r))
.= (f . v1) + ((fi . x2) + (s2 * r)) by A7, A14
.= (f . v1) + (f . v2) by A7, A16 ;
::_thesis: verum
end;
 f is homogeneous
proof
let v0 be VECTOR of (X + (Lin {v})); :: according to HAHNBAN:def_3 ::_thesis: for r being Real holds f . (r * v0) = r * (f . v0)
let t be Real; ::_thesis: f . (t * v0) = t * (f . v0)
consider x0 being VECTOR of X, s0 being Real such that
A17: v0 |-- (W1,(Lin {y})) = [x0,(s0 * v)] by A1, A2, Th15;
A18: ( (v0 |-- (W1,(Lin {y}))) `1 = x0 & (v0 |-- (W1,(Lin {y}))) `2 = s0 * v ) by A17, MCART_1:7;
 (t * v0) |-- (W1,(Lin {y})) = [(t * x0),((t * s0) * v)] by A1, A2, A17, Th17;
then  ( ((t * v0) |-- (W1,(Lin {y}))) `1 = t * x0 & ((t * v0) |-- (W1,(Lin {y}))) `2 = (t * s0) * v ) by MCART_1:7;
hence f . (t * v0) = (fi . (t * x0)) + ((t * s0) * r) by A7
.= (t * (fi . x0)) + (t * (s0 * r)) by Def3
.= t * ((fi . x0) + (s0 * r))
.= t * (f . v0) by A7, A18 ;
::_thesis: verum
end;
then reconsider f = f as linear-Functional of (X + (Lin {v})) by A12;
take  f ; ::_thesis: ( f | the carrier of X = fi & f . y = r )
 ( dom fi = the carrier of X & dom f = the carrier of (X + (Lin {v})) ) by FUNCT_2:def_1;
then  dom fi = (dom f) /\ the carrier of X by Th1, XBOOLE_1:28;
hence  f | the carrier of X = fi by A8, FUNCT_1:46; ::_thesis: f . y = r
(y |-- (W1,(Lin {y}))) `2 = y by A10, MCART_1:7
.= 1 * v by A1, RLVECT_1:def_8 ;
hence f . y = (fi . (0. X)) + (1 * r) by A7, A11
.= 0 + (1 * r) by Th20
.= r ;
::_thesis: verum
end;

begin

Lm1:  for V being RealLinearSpace
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 ) )
proof
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 by STRUCT_0:def_5;
 v in Lin {v} by RLVECT_4:9;
then A2: v in the carrier of (Lin {v}) by STRUCT_0:def_5;
 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) by RLVECT_1:4
.= (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_R_eal_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 R_eal; ::_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 set ; :: 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 set ; :: 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 number by A9;
take  b ; :: according to XXREAL_2:def_10 ::_thesis: b is UpperBound of A
let x be ext-real number ; :: 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 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}) by STRUCT_0:def_5;
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})) by STRUCT_0:def_5;
reconsider x1 = x as VECTOR of X by A15, STRUCT_0:def_5;
consider t being Real such that
A18: y29 = t * v by A16, RLVECT_4:8;
percases ( 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, RLVECT_1:4;
then  fi . x1 <= q . u by A3, A14;
hence  psi . y <= q . u by A12, A19, FUNCT_1:49; ::_thesis: verum
end;
supposeA20: 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) by RLVECT_1:17 ;
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})) by STRUCT_0:def_5;
 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;
supposeA28: 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})) by STRUCT_0:def_5;
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, RLVECT_1:17;
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;
end;

Lm2:  for V being RealLinearSpace holds RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is RealLinearSpace
proof
let V be RealLinearSpace; ::_thesis: RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is RealLinearSpace
A1: for v9, w9 being VECTOR of V
for v, w being VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) st v = v9 & w = w9 holds
( v + w = v9 + w9 & ( for r being Real holds r * v = r * v9 ) ) ;
 ( RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is Abelian & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is add-associative & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is right_zeroed & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is right_complementable & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is vector-distributive & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-distributive & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-associative & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-unital )
proof
hereby  :: according to RLVECT_1:def_2 ::_thesis: ( RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is add-associative & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is right_zeroed & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is right_complementable & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is vector-distributive & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-distributive & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-associative & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-unital )
let v, w be VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); ::_thesis: v + w = w + v
reconsider v9 = v, w9 = w as VECTOR of V ;
thus v + w = w9 + v9 by A1
.= w + v ; ::_thesis: verum
end;
hereby  :: according to RLVECT_1:def_3 ::_thesis: ( RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is right_zeroed & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is right_complementable & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is vector-distributive & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-distributive & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-associative & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-unital )
let u, v, w be VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); ::_thesis: (u + v) + w = u + (v + w)
reconsider u9 = u, v9 = v, w9 = w as VECTOR of V ;
thus (u + v) + w = (u9 + v9) + w9
.= u9 + (v9 + w9) by RLVECT_1:def_3
.= u + (v + w) ; ::_thesis: verum
end;
hereby  :: according to RLVECT_1:def_4 ::_thesis: ( RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is right_complementable & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is vector-distributive & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-distributive & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-associative & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-unital )
let v be VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); ::_thesis: v + (0. RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)) = v
reconsider v9 = v as VECTOR of V ;
thus v + (0. RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)) = v9 + (0. V)
.= v by RLVECT_1:4 ; ::_thesis: verum
end;
thus  RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is right_complementable ::_thesis: ( RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is vector-distributive & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-distributive & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-associative & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-unital )
proof
let v be VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable
reconsider v9 = v as VECTOR of V ;
consider w9 being VECTOR of V such that
A2: v9 + w9 = 0. V by ALGSTR_0:def_11;
reconsider w = w9 as VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ;
take  w ; :: according to ALGSTR_0:def_11 ::_thesis: v + w = 0. RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
thus  v + w = 0. RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by A2; ::_thesis: verum
end;
hereby  :: according to RLVECT_1:def_5 ::_thesis: ( RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-distributive & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-associative & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-unital )
let a be real number ; ::_thesis: for v, w being VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds a * (v + w) = (a * v) + (a * w)
let v, w be VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); ::_thesis: a * (v + w) = (a * v) + (a * w)
reconsider v9 = v, w9 = w as VECTOR of V ;
thus a * (v + w) = a * (v9 + w9)
.= (a * v9) + (a * w9) by RLVECT_1:def_5
.= (a * v) + (a * w) ; ::_thesis: verum
end;
hereby  :: according to RLVECT_1:def_6 ::_thesis: ( RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-associative & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-unital )
let a, b be real number ; ::_thesis: for v being VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (a + b) * v = (a * v) + (b * v)
let v be VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); ::_thesis: (a + b) * v = (a * v) + (b * v)
reconsider v9 = v as VECTOR of V ;
thus (a + b) * v = (a + b) * v9
.= (a * v9) + (b * v9) by RLVECT_1:def_6
.= (a * v) + (b * v) ; ::_thesis: verum
end;
hereby  :: according to RLVECT_1:def_7 ::_thesis: RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-unital
let a, b be real number ; ::_thesis: for v being VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (a * b) * v = a * (b * v)
let v be VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); ::_thesis: (a * b) * v = a * (b * v)
reconsider v9 = v as VECTOR of V ;
thus (a * b) * v = (a * b) * v9
.= a * (b * v9) by RLVECT_1:def_7
.= a * (b * v) ; ::_thesis: verum
end;
let v be VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); :: according to RLVECT_1:def_8 ::_thesis: 1 * v = v
reconsider v9 = v as VECTOR of V ;
thus 1 * v = 1 * v9
.= v by RLVECT_1:def_8 ; ::_thesis: verum
end;
hence  RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is RealLinearSpace ; ::_thesis: verum
end;

Lm3:  for V, V9, W9 being RealLinearSpace st V9 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds
for W being Subspace of V st W9 = RLSStruct(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W #) holds
W9 is Subspace of V9
proof
let V be RealLinearSpace; ::_thesis: for V9, W9 being RealLinearSpace st V9 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds
for W being Subspace of V st W9 = RLSStruct(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W #) holds
W9 is Subspace of V9
let V9, W9 be RealLinearSpace; ::_thesis: ( V9 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) implies for W being Subspace of V st W9 = RLSStruct(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W #) holds
W9 is Subspace of V9 )
assume A1: V9 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ; ::_thesis: for W being Subspace of V st W9 = RLSStruct(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W #) holds
W9 is Subspace of V9
let W be Subspace of V; ::_thesis: ( W9 = RLSStruct(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W #) implies W9 is Subspace of V9 )
assume A2: W9 = RLSStruct(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W #) ; ::_thesis: W9 is Subspace of V9
hence  the carrier of W9 c= the carrier of V9 by A1, RLSUB_1:def_2; :: according to RLSUB_1:def_2 ::_thesis: ( 0. W9 = 0. V9 & the addF of W9 = the addF of V9 || the carrier of W9 & the Mult of W9 = the Mult of V9 | [:REAL, the carrier of W9:] )
thus  0. W9 = 0. W by A2
.= 0. V by RLSUB_1:def_2
.= 0. V9 by A1 ; ::_thesis: ( the addF of W9 = the addF of V9 || the carrier of W9 & the Mult of W9 = the Mult of V9 | [:REAL, the carrier of W9:] )
thus  the addF of W9 = the addF of V9 || the carrier of W9 by A1, A2, RLSUB_1:def_2; ::_thesis: the Mult of W9 = the Mult of V9 | [:REAL, the carrier of W9:]
thus  the Mult of W9 = the Mult of V9 | [:REAL, the carrier of W9:] by A1, A2, RLSUB_1:def_2; ::_thesis: verum
end;

Lm4:  for V, V9 being RealLinearSpace st V9 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds
for f being linear-Functional of V9 holds f is linear-Functional of V
proof
let V, V9 be RealLinearSpace; ::_thesis: ( V9 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) implies for f being linear-Functional of V9 holds f is linear-Functional of V )
assume A1: V9 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ; ::_thesis: for f being linear-Functional of V9 holds f is linear-Functional of V
let f be linear-Functional of V9; ::_thesis: f is linear-Functional of V
reconsider f9 = f as Functional of V by A1;
A2: f9 is homogeneous
proof
let x be VECTOR of V; :: according to HAHNBAN:def_3 ::_thesis: for r being Real holds f9 . (r * x) = r * (f9 . x)
let r be Real; ::_thesis: f9 . (r * x) = r * (f9 . x)
reconsider x9 = x as VECTOR of V9 by A1;
thus f9 . (r * x) = f9 . (r * x9) by A1
.= r * (f9 . x) by Def3 ; ::_thesis: verum
end;
 f9 is additive
proof
let x, y be VECTOR of V; :: according to HAHNBAN:def_2 ::_thesis: f9 . (x + y) = (f9 . x) + (f9 . y)
reconsider x9 = x, y9 = y as VECTOR of V9 by A1;
thus f9 . (x + y) = f . (x9 + y9) by A1
.= (f9 . x) + (f9 . y) by Def2 ; ::_thesis: verum
end;
hence  f is linear-Functional of V by A2; ::_thesis: verum
end;

Lm5:  for V, V9 being RealLinearSpace st V9 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds
for f being linear-Functional of V holds f is linear-Functional of V9
proof
let V, V9 be RealLinearSpace; ::_thesis: ( V9 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) implies for f being linear-Functional of V holds f is linear-Functional of V9 )
assume A1: V9 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ; ::_thesis: for f being linear-Functional of V holds f is linear-Functional of V9
let f be linear-Functional of V; ::_thesis: f is linear-Functional of V9
reconsider f9 = f as Functional of V9 by A1;
A2: f9 is homogeneous
proof
let x be VECTOR of V9; :: according to HAHNBAN:def_3 ::_thesis: for r being Real holds f9 . (r * x) = r * (f9 . x)
let r be Real; ::_thesis: f9 . (r * x) = r * (f9 . x)
reconsider x9 = x as VECTOR of V by A1;
thus f9 . (r * x) = f9 . (r * x9) by A1
.= r * (f9 . x) by Def3 ; ::_thesis: verum
end;
 f9 is additive
proof
let x, y be VECTOR of V9; :: according to HAHNBAN:def_2 ::_thesis: f9 . (x + y) = (f9 . x) + (f9 . y)
reconsider x9 = x, y9 = y as VECTOR of V by A1;
thus f9 . (x + y) = f . (x9 + y9) by A1
.= (f9 . x) + (f9 . y) by Def2 ; ::_thesis: verum
end;
hence  f is linear-Functional of V9 by A2; ::_thesis: verum
end;

theorem Th22: :: HAHNBAN:22
for V being RealLinearSpace
for X being Subspace of V
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 V st
( psi | the carrier of X = fi & ( for x being VECTOR of V holds psi . x <= q . x ) )
proof
let V be RealLinearSpace; ::_thesis: for X being Subspace of V
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 V st
( psi | the carrier of X = fi & ( for x being VECTOR of V holds psi . x <= q . x ) )
let X be Subspace of V; ::_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 V st
( psi | the carrier of X = fi & ( for x being VECTOR of V holds psi . x <= q . 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 V st
( psi | the carrier of X = fi & ( for x being VECTOR of V holds psi . x <= q . x ) )
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 V st
( psi | the carrier of X = fi & ( for x being VECTOR of V holds psi . x <= q . x ) ) )
 the carrier of X c= the carrier of V by RLSUB_1:def_2;
then  ( fi in PFuncs ( the carrier of X,REAL) & PFuncs ( the carrier of X,REAL) c= PFuncs ( the carrier of V,REAL) ) by PARTFUN1:45, PARTFUN1:50;
then reconsider fi9 = fi as Element of PFuncs ( the carrier of V,REAL) ;
reconsider RLS = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) as RealLinearSpace by Lm2;
defpred S1[ Element of PFuncs ( the carrier of V,REAL)] means  ex Y being Subspace of V st
( the carrier of X c= the carrier of Y & $1 | the carrier of X = fi & ex f9 being linear-Functional of Y st
( $1 = f9 & ( for y being VECTOR of Y
for v being VECTOR of V st y = v holds
f9 . y <= q . v ) ) );
reconsider A =  {  f where f is Element of PFuncs ( the carrier of V,REAL) : S1[f]  }  as Subset of (PFuncs ( the carrier of V,REAL)) from DOMAIN_1:sch_7();
A1: fi9 | the carrier of X = fi by RELSET_1:19;
assume  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 V st
( psi | the carrier of X = fi & ( for x being VECTOR of V holds psi . x <= q . x ) )
then  fi in A by A1;
then reconsider A = A as non empty Subset of (PFuncs ( the carrier of V,REAL)) ;
defpred S2[ set , set ] means $1 c= $2;
A2: for x, y being Element of A st S2[x,y] & S2[y,x] holds
x = y by XBOOLE_0:def_10;
A3: for x, y, z being Element of A st S2[x,y] & S2[y,z] holds
S2[x,z] by XBOOLE_1:1;
A4: now__::_thesis:_for_B_being_set_st_B_c=_A_&_(_for_x,_y_being_Element_of_A_st_x_in_B_&_y_in_B_&_not_S2[x,y]_holds_
S2[y,x]_)_holds_
ex_u_being_Element_of_A_st_
for_x_being_Element_of_A_st_x_in_B_holds_
S2[x,u]
let B be set ; ::_thesis: ( B c= A & ( for x, y being Element of A st x in B & y in B & not S2[x,y] holds
S2[y,x] ) implies ex u being Element of A st
for x being Element of A st b3 in u holds
S2[b3,x] )
assume that
A5: B c= A and
A6: for x, y being Element of A st x in B & y in B & not S2[x,y] holds
S2[y,x] ; ::_thesis: ex u being Element of A st
for x being Element of A st b3 in u holds
S2[b3,x]
percases ( B = {} or B <> {} ) ;
supposeA7: B = {} ; ::_thesis: ex u being Element of A st
for x being Element of A st b3 in u holds
S2[b3,x]
set u = the Element of A;
take u = the Element of A; ::_thesis: for x being Element of A st x in B holds
S2[x,u]
let x be Element of A; ::_thesis: ( x in B implies S2[x,u] )
assume  x in B ; ::_thesis: S2[x,u]
hence  S2[x,u] by A7; ::_thesis: verum
end;
supposeA8: B <> {} ; ::_thesis: ex u being Element of A st
for x being Element of A st b3 in u holds
S2[b3,x]
A9: B is c=-linear
proof
let x, y be set ; :: according to ORDINAL1:def_8 ::_thesis: ( not x in B or not y in B or x,y are_c=-comparable )
assume  ( x in B & y in B ) ; ::_thesis: x,y are_c=-comparable
hence  ( x c= y or y c= x ) by A5, A6; :: according to XBOOLE_0:def_9 ::_thesis: verum
end;
 B is Subset of (PFuncs ( the carrier of V,REAL)) by A5, XBOOLE_1:1;
then reconsider u = union B as Element of PFuncs ( the carrier of V,REAL) by A9, TREES_2:40;
reconsider E = B as functional non empty set by A5, A8;
set t = the Element of B;
set K =  {  (dom g) where g is Element of E : verum  }  ;
A10: dom u = union  {  (dom g) where g is Element of E : verum  }  by FUNCT_1:110;
A11: now__::_thesis:_for_t_being_set_st_t_in_A_holds_
ex_Y_being_Subspace_of_V_ex_f_being_linear-Functional_of_Y_st_
(_t_=_f_&_the_carrier_of_X_c=_the_carrier_of_Y_&_f_|_the_carrier_of_X_=_fi_&_(_for_y_being_VECTOR_of_Y
for_v_being_VECTOR_of_V_st_y_=_v_holds_
f_._y_<=_q_._v_)_)
let t be set ; ::_thesis: ( t in A implies ex Y being Subspace of V ex f being linear-Functional of Y st
( t = f & the carrier of X c= the carrier of Y & f | the carrier of X = fi & ( for y being VECTOR of Y
for v being VECTOR of V st y = v holds
f . y <= q . v ) ) )
assume  t in A ; ::_thesis: ex Y being Subspace of V ex f being linear-Functional of Y st
( t = f & the carrier of X c= the carrier of Y & f | the carrier of X = fi & ( for y being VECTOR of Y
for v being VECTOR of V st y = v holds
f . y <= q . v ) )
then consider f being Element of PFuncs ( the carrier of V,REAL) such that
A12: t = f and
A13: ex Y being Subspace of V st
( the carrier of X c= the carrier of Y & f | the carrier of X = fi & ex f9 being linear-Functional of Y st
( f = f9 & ( for y being VECTOR of Y
for v being VECTOR of V st y = v holds
f9 . y <= q . v ) ) ) ;
consider Y being Subspace of V such that
A14: the carrier of X c= the carrier of Y and
A15: f | the carrier of X = fi and
A16: ex f9 being linear-Functional of Y st
( f = f9 & ( for y being VECTOR of Y
for v being VECTOR of V st y = v holds
f9 . y <= q . v ) ) by A13;
take Y = Y; ::_thesis: ex f being linear-Functional of Y st
( t = f & the carrier of X c= the carrier of Y & f | the carrier of X = fi & ( for y being VECTOR of Y
for v being VECTOR of V st y = v holds
f . y <= q . v ) )
consider f9 being linear-Functional of Y such that
A17: f = f9 and
A18: for y being VECTOR of Y
for v being VECTOR of V st y = v holds
f9 . y <= q . v by A16;
reconsider f = f9 as linear-Functional of Y ;
take f = f; ::_thesis: ( t = f & the carrier of X c= the carrier of Y & f | the carrier of X = fi & ( for y being VECTOR of Y
for v being VECTOR of V st y = v holds
f . y <= q . v ) )
thus  t = f by A12, A17; ::_thesis: ( the carrier of X c= the carrier of Y & f | the carrier of X = fi & ( for y being VECTOR of Y
for v being VECTOR of V st y = v holds
f . y <= q . v ) )
thus  the carrier of X c= the carrier of Y by A14; ::_thesis: ( f | the carrier of X = fi & ( for y being VECTOR of Y
for v being VECTOR of V st y = v holds
f . y <= q . v ) )
thus  f | the carrier of X = fi by A15, A17; ::_thesis: for y being VECTOR of Y
for v being VECTOR of V st y = v holds
f . y <= q . v
thus  for y being VECTOR of Y
for v being VECTOR of V st y = v holds
f . y <= q . v by A18; ::_thesis: verum
end;
A19: now__::_thesis:_for_x_being_set_st_x_in__{__(dom_g)_where_g_is_Element_of_E_:_verum__}__holds_
x_c=_the_carrier_of_V
let x be set ; ::_thesis: ( x in  {  (dom g) where g is Element of E : verum  }  implies x c= the carrier of V )
assume  x in  {  (dom g) where g is Element of E : verum  }  ; ::_thesis: x c= the carrier of V
then consider g being Element of E such that
A20: dom g = x ;
 g in A by A5, TARSKI:def_3;
then consider Y being Subspace of V, f9 being linear-Functional of Y such that
A21: g = f9 and
 the carrier of X c= the carrier of Y and
 f9 | the carrier of X = fi and
 for y being VECTOR of Y
for v being VECTOR of V st y = v holds
f9 . y <= q . v by A11;
 dom g = the carrier of Y by A21, FUNCT_2:def_1;
hence  x c= the carrier of V by A20, RLSUB_1:def_2; ::_thesis: verum
end;
 the Element of B in A by A5, A8, TARSKI:def_3;
then  ex Y being Subspace of V ex f9 being linear-Functional of Y st
( the Element of B = f9 & the carrier of X c= the carrier of Y & f9 | the carrier of X = fi & ( for y being VECTOR of Y
for v being VECTOR of V st y = v holds
f9 . y <= q . v ) ) by A11;
then  u <> {} by A8, XBOOLE_1:3, ZFMISC_1:74;
then reconsider D = dom u as non empty Subset of V by A10, A19, ZFMISC_1:76;
 D is linearly-closed
proof
hereby  :: according to RLSUB_1:def_1 ::_thesis: for b1 being Element of REAL
for b2 being Element of the carrier of V holds
( not b2 in D or b1 * b2 in D )
let v, u be Element of V; ::_thesis: ( v in D & u in D implies v + u in D )
assume that
A22: v in D and
A23: u in D ; ::_thesis: v + u in D
consider D1 being set  such that
A24: v in D1 and
A25: D1 in  {  (dom g) where g is Element of E : verum  }  by A10, A22, TARSKI:def_4;
consider g1 being Element of E such that
A26: D1 = dom g1 by A25;
consider D2 being set  such that
A27: u in D2 and
A28: D2 in  {  (dom g) where g is Element of E : verum  }  by A10, A23, TARSKI:def_4;
consider g2 being Element of E such that
A29: D2 = dom g2 by A28;
 ( g1 in A & g2 in A ) by A5, TARSKI:def_3;
then  ( g1 c= g2 or g2 c= g1 ) by A6;
then consider g being Element of E such that
A30: g1 c= g and
A31: g2 c= g ;
 g in A by A5, TARSKI:def_3;
then consider Y being Subspace of V, f9 being linear-Functional of Y such that
A32: g = f9 and
 the carrier of X c= the carrier of Y and
 f9 | the carrier of X = fi and
 for y being VECTOR of Y
for v being VECTOR of V st y = v holds
f9 . y <= q . v by A11;
A33: dom g = the carrier of Y by A32, FUNCT_2:def_1;
 D2 c= dom g by A29, A31, RELAT_1:11;
then A34: u in Y by A27, A33, STRUCT_0:def_5;
 D1 c= dom g by A26, A30, RELAT_1:11;
then  v in Y by A24, A33, STRUCT_0:def_5;
then  v + u in Y by A34, RLSUB_1:20;
then A35: v + u in dom g by A33, STRUCT_0:def_5;
 dom g in  {  (dom g) where g is Element of E : verum  }  ;
hence  v + u in D by A10, A35, TARSKI:def_4; ::_thesis: verum
end;
let a be Real; ::_thesis: for b1 being Element of the carrier of V holds
( not b1 in D or a * b1 in D )
let v be Element of V; ::_thesis: ( not v in D or a * v in D )
assume  v in D ; ::_thesis: a * v in D
then consider D1 being set  such that
A36: v in D1 and
A37: D1 in  {  (dom g) where g is Element of E : verum  }  by A10, TARSKI:def_4;
consider g being Element of E such that
A38: D1 = dom g by A37;
 g in A by A5, TARSKI:def_3;
then consider Y being Subspace of V, f9 being linear-Functional of Y such that
A39: g = f9 and
 the carrier of X c= the carrier of Y and
 f9 | the carrier of X = fi and
 for y being VECTOR of Y
for v being VECTOR of V st y = v holds
f9 . y <= q . v by A11;
A40: dom g = the carrier of Y by A39, FUNCT_2:def_1;
then  v in Y by A36, A38, STRUCT_0:def_5;
then  a * v in Y by RLSUB_1:21;
then A41: a * v in dom g by A40, STRUCT_0:def_5;
 dom g in  {  (dom g) where g is Element of E : verum  }  ;
hence  a * v in D by A10, A41, TARSKI:def_4; ::_thesis: verum
end;
then consider Y being strict Subspace of V such that
A42: the carrier of Y = dom u by RLSUB_1:35;
set t = the Element of dom u;
consider XX being set  such that
 the Element of dom u in XX and
A43: XX in  {  (dom g) where g is Element of E : verum  }  by A10, A42, TARSKI:def_4;
 ex f being Function st
( u = f & dom f c= the carrier of V & rng f c= REAL ) by PARTFUN1:def_3;
then reconsider f9 = u as Function of the carrier of Y,REAL by A42, FUNCT_2:def_1, RELSET_1:4;
reconsider f9 = f9 as Functional of Y ;
consider gg being Element of E such that
A44: XX = dom gg by A43;
A45: f9 is additive
proof
let x, y be VECTOR of Y; :: according to HAHNBAN:def_2 ::_thesis: f9 . (x + y) = (f9 . x) + (f9 . y)
consider XXx being set  such that
A46: x in XXx and
A47: XXx in  {  (dom g) where g is Element of E : verum  }  by A10, A42, TARSKI:def_4;
consider ggx being Element of E such that
A48: XXx = dom ggx by A47;
consider XXy being set  such that
A49: y in XXy and
A50: XXy in  {  (dom g) where g is Element of E : verum  }  by A10, A42, TARSKI:def_4;
consider ggy being Element of E such that
A51: XXy = dom ggy by A50;
 ( ggx in A & ggy in A ) by A5, TARSKI:def_3;
then  ( ggx c= ggy or ggy c= ggx ) by A6;
then consider gg being Element of E such that
A52: ( gg = ggx or gg = ggy ) and
A53: ( ggx c= gg & ggy c= gg ) ;
 gg in A by A5, TARSKI:def_3;
then consider YY being Subspace of V, ff being linear-Functional of YY such that
A54: gg = ff and
 the carrier of X c= the carrier of YY and
 ff | the carrier of X = fi and
 for y being VECTOR of YY
for v being VECTOR of V st y = v holds
ff . y <= q . v by A11;
 ( dom ggx c= dom gg & dom ggy c= dom gg ) by A53, RELAT_1:11;
then reconsider x9 = x, y9 = y as VECTOR of YY by A46, A48, A49, A51, A54, FUNCT_2:def_1;
A55: ff c= f9 by A54, ZFMISC_1:74;
A56: dom ff = the carrier of YY by FUNCT_2:def_1;
then  YY is Subspace of Y by A10, A42, A47, A48, A50, A51, A52, A54, RLSUB_1:28, ZFMISC_1:74;
then  x + y = x9 + y9 by RLSUB_1:13;
hence f9 . (x + y) = ff . (x9 + y9) by A56, A55, GRFUNC_1:2
.= (ff . x9) + (ff . y9) by Def2
.= (f9 . x) + (ff . y9) by A56, A55, GRFUNC_1:2
.= (f9 . x) + (f9 . y) by A56, A55, GRFUNC_1:2 ;
::_thesis: verum
end;
 f9 is homogeneous
proof
let x be VECTOR of Y; :: according to HAHNBAN:def_3 ::_thesis: for r being Real holds f9 . (r * x) = r * (f9 . x)
let r be Real; ::_thesis: f9 . (r * x) = r * (f9 . x)
consider XX being set  such that
A57: x in XX and
A58: XX in  {  (dom g) where g is Element of E : verum  }  by A10, A42, TARSKI:def_4;
consider gg being Element of E such that
A59: XX = dom gg by A58;
 gg in A by A5, TARSKI:def_3;
then consider YY being Subspace of V, ff being linear-Functional of YY such that
A60: gg = ff and
 the carrier of X c= the carrier of YY and
 ff | the carrier of X = fi and
 for y being VECTOR of YY
for v being VECTOR of V st y = v holds
ff . y <= q . v by A11;
reconsider x9 = x as VECTOR of YY by A57, A59, A60, FUNCT_2:def_1;
A61: ff c= f9 by A60, ZFMISC_1:74;
A62: dom ff = the carrier of YY by FUNCT_2:def_1;
then  YY is Subspace of Y by A10, A42, A58, A59, A60, RLSUB_1:28, ZFMISC_1:74;
then  r * x = r * x9 by RLSUB_1:14;
hence f9 . (r * x) = ff . (r * x9) by A62, A61, GRFUNC_1:2
.= r * (ff . x9) by Def3
.= r * (f9 . x) by A62, A61, GRFUNC_1:2 ;
::_thesis: verum
end;
then reconsider f9 = f9 as linear-Functional of Y by A45;
A63: now__::_thesis:_for_y_being_VECTOR_of_Y
for_v_being_VECTOR_of_V_st_y_=_v_holds_
f9_._y_<=_q_._v
let y be VECTOR of Y; ::_thesis: for v being VECTOR of V st y = v holds
f9 . y <= q . v
let v be VECTOR of V; ::_thesis: ( y = v implies f9 . y <= q . v )
assume A64: y = v ; ::_thesis: f9 . y <= q . v
consider XX being set  such that
A65: y in XX and
A66: XX in  {  (dom g) where g is Element of E : verum  }  by A10, A42, TARSKI:def_4;
consider gg being Element of E such that
A67: XX = dom gg by A66;
 gg in A by A5, TARSKI:def_3;
then consider YY being Subspace of V, ff being linear-Functional of YY such that
A68: gg = ff and
 the carrier of X c= the carrier of YY and
 ff | the carrier of X = fi and
A69: for y being VECTOR of YY
for v being VECTOR of V st y = v holds
ff . y <= q . v by A11;
reconsider y9 = y as VECTOR of YY by A65, A67, A68, FUNCT_2:def_1;
A70: ( dom ff = the carrier of YY & ff c= f9 ) by A68, FUNCT_2:def_1, ZFMISC_1:74;
 ff . y9 <= q . v by A64, A69;
hence  f9 . y <= q . v by A70, GRFUNC_1:2; ::_thesis: verum
end;
 gg in A by A5, TARSKI:def_3;
then consider YY being Subspace of V, ff being linear-Functional of YY such that
A71: gg = ff and
A72: the carrier of X c= the carrier of YY and
A73: ff | the carrier of X = fi and
 for y being VECTOR of YY
for v being VECTOR of V st y = v holds
ff . y <= q . v by A11;
 the carrier of X c= dom ff by A72, FUNCT_2:def_1;
then A74: u | the carrier of X = fi by A71, A73, GRFUNC_1:27, ZFMISC_1:74;
A75: XX c= dom u by A10, A43, ZFMISC_1:74;
 XX = the carrier of YY by A44, A71, FUNCT_2:def_1;
then  the carrier of X c= the carrier of Y by A42, A72, A75, XBOOLE_1:1;
then  u in A by A74, A63;
then reconsider u = u as Element of A ;
take u = u; ::_thesis: for x being Element of A st x in B holds
S2[x,u]
let x be Element of A; ::_thesis: ( x in B implies S2[x,u] )
assume  x in B ; ::_thesis: S2[x,u]
hence  S2[x,u] by ZFMISC_1:74; ::_thesis: verum
end;
end;
end;
A76: for x being Element of A holds S2[x,x] ;
consider psi being Element of A such that
A77: for chi being Element of A st psi <> chi holds
not S2[psi,chi] from ORDERS_1:sch_1(A76, A2, A3, A4);
 psi in A ;
then consider f being Element of PFuncs ( the carrier of V,REAL) such that
A78: f = psi and
A79: ex Y being Subspace of V st
( the carrier of X c= the carrier of Y & f | the carrier of X = fi & ex f9 being linear-Functional of Y st
( f = f9 & ( for y being VECTOR of Y
for v being VECTOR of V st y = v holds
f9 . y <= q . v ) ) ) ;
consider Y being Subspace of V such that
A80: the carrier of X c= the carrier of Y and
A81: f | the carrier of X = fi and
A82: ex f9 being linear-Functional of Y st
( f = f9 & ( for y being VECTOR of Y
for v being VECTOR of V st y = v holds
f9 . y <= q . v ) ) by A79;
reconsider RLSY = RLSStruct(# the carrier of Y, the ZeroF of Y, the addF of Y, the Mult of Y #) as RealLinearSpace by Lm2;
consider f9 being linear-Functional of Y such that
A83: f = f9 and
A84: for y being VECTOR of Y
for v being VECTOR of V st y = v holds
f9 . y <= q . v by A82;
A85: RLSY is Subspace of RLS by Lm3;
A86: now__::_thesis:_not_RLSStruct(#_the_carrier_of_Y,_the_ZeroF_of_Y,_the_addF_of_Y,_the_Mult_of_Y_#)_<>_RLSStruct(#_the_carrier_of_V,_the_ZeroF_of_V,_the_addF_of_V,_the_Mult_of_V_#)
assume  RLSStruct(# the carrier of Y, the ZeroF of Y, the addF of Y, the Mult of Y #) <> RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ; ::_thesis: contradiction
then A87: the carrier of Y <> the carrier of V by A85, RLSUB_1:32;
 the carrier of Y c= the carrier of V by RLSUB_1:def_2;
then  the carrier of Y c< the carrier of V by A87, XBOOLE_0:def_8;
then consider v being set  such that
A88: v in the carrier of V and
A89: not v in the carrier of Y by XBOOLE_0:6;
reconsider v = v as VECTOR of V by A88;
consider phi being linear-Functional of (Y + (Lin {v})) such that
A90: phi | the carrier of Y = f9 and
A91: for x being VECTOR of (Y + (Lin {v}))
for v being VECTOR of V st x = v holds
phi . x <= q . v by A84, A89, Lm1;
A92: rng phi c= REAL by RELAT_1:def_19;
 the carrier of Y c= the carrier of (Y + (Lin {v})) by Th1;
then A93: the carrier of X c= the carrier of (Y + (Lin {v})) by A80, XBOOLE_1:1;
A94: dom phi = the carrier of (Y + (Lin {v})) by FUNCT_2:def_1;
then  dom phi c= the carrier of V by RLSUB_1:def_2;
then reconsider phi = phi as Element of PFuncs ( the carrier of V,REAL) by A92, PARTFUN1:def_3;
 the carrier of Y /\ the carrier of X = the carrier of X by A80, XBOOLE_1:28;
then  phi | the carrier of X = fi by A81, A83, A90, RELAT_1:71;
then A95: phi in A by A91, A93;
 v in Lin {v} by RLVECT_4:9;
then A96: v in the carrier of (Lin {v}) by STRUCT_0:def_5;
reconsider phi = phi as Element of A by A95;
 the carrier of (Lin {v}) c= the carrier of ((Lin {v}) + Y) by Th1;
then  ( dom f9 = the carrier of Y & v in the carrier of ((Lin {v}) + Y) ) by A96, FUNCT_2:def_1;
then  phi <> psi by A78, A83, A89, A94, RLSUB_2:5;
hence  contradiction by A77, A78, A83, A90, RELAT_1:59; ::_thesis: verum
end;
reconsider ggh = f9 as linear-Functional of RLSY by Lm5;
 f = ggh by A83;
then reconsider psi = psi as linear-Functional of V by A78, A86, Lm4;
take  psi ; ::_thesis: ( psi | the carrier of X = fi & ( for x being VECTOR of V holds psi . x <= q . x ) )
thus  psi | the carrier of X = fi by A78, A81; ::_thesis: for x being VECTOR of V holds psi . x <= q . x
let x be VECTOR of V; ::_thesis: psi . x <= q . x
thus  psi . x <= q . x by A78, A82, A86; ::_thesis: verum
end;

theorem Th23: :: HAHNBAN:23
for V being RealNormSpace holds the normF of V is subadditive absolutely_homogeneous Functional of V
proof
let V be RealNormSpace; ::_thesis: the normF of V is subadditive absolutely_homogeneous Functional of V
reconsider N = the normF of V as Functional of V ;
A1: N is subadditive
proof
let x, y be VECTOR of V; :: according to HAHNBAN:def_1 ::_thesis: N . (x + y) <= (N . x) + (N . y)
A2: N . (x + y) = ||.(x + y).|| by NORMSP_0:def_1;
 ( N . x = ||.x.|| & N . y = ||.y.|| ) by NORMSP_0:def_1;
hence  N . (x + y) <= (N . x) + (N . y) by A2, NORMSP_1:def_1; ::_thesis: verum
end;
 N is absolutely_homogeneous
proof
let x be VECTOR of V; :: according to HAHNBAN:def_6 ::_thesis: for r being Real holds N . (r * x) = (abs r) * (N . x)
let r be Real; ::_thesis: N . (r * x) = (abs r) * (N . x)
thus N . (r * x) = ||.(r * x).|| by NORMSP_0:def_1
.= (abs r) * ||.x.|| by NORMSP_1:def_1
.= (abs r) * (N . x) by NORMSP_0:def_1 ; ::_thesis: verum
end;
hence  the normF of V is subadditive absolutely_homogeneous Functional of V by A1; ::_thesis: verum
end;

theorem :: HAHNBAN:24
for V being RealNormSpace
for X being Subspace 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 <= ||.v.|| ) holds
ex psi being linear-Functional of V st
( psi | the carrier of X = fi & ( for x being VECTOR of V holds psi . x <= ||.x.|| ) )
proof
let V be RealNormSpace; ::_thesis: for X being Subspace 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 <= ||.v.|| ) holds
ex psi being linear-Functional of V st
( psi | the carrier of X = fi & ( for x being VECTOR of V holds psi . x <= ||.x.|| ) )
let X be Subspace 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 <= ||.v.|| ) holds
ex psi being linear-Functional of V st
( psi | the carrier of X = fi & ( for x being VECTOR of V holds psi . x <= ||.x.|| ) )
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 <= ||.v.|| ) implies ex psi being linear-Functional of V st
( psi | the carrier of X = fi & ( for x being VECTOR of V holds psi . x <= ||.x.|| ) ) )
assume A1: for x being VECTOR of X
for v being VECTOR of V st x = v holds
fi . x <= ||.v.|| ; ::_thesis: ex psi being linear-Functional of V st
( psi | the carrier of X = fi & ( for x being VECTOR of V holds psi . x <= ||.x.|| ) )
reconsider q = the normF of V as Banach-Functional of V by Th23;
now__::_thesis:_for_x_being_VECTOR_of_X
for_v_being_VECTOR_of_V_st_x_=_v_holds_
fi_._x_<=_q_._v
let x be VECTOR of X; ::_thesis: for v being VECTOR of V st x = v holds
fi . x <= q . v
let v be VECTOR of V; ::_thesis: ( x = v implies fi . x <= q . v )
assume A2: x = v ; ::_thesis: fi . x <= q . v
 q . v = ||.v.|| by NORMSP_0:def_1;
hence  fi . x <= q . v by A1, A2; ::_thesis: verum
end;
then consider psi being linear-Functional of V such that
A3: psi | the carrier of X = fi and
A4: for x being VECTOR of V holds psi . x <= q . x by Th22;
take  psi ; ::_thesis: ( psi | the carrier of X = fi & ( for x being VECTOR of V holds psi . x <= ||.x.|| ) )
thus  psi | the carrier of X = fi by A3; ::_thesis: for x being VECTOR of V holds psi . x <= ||.x.||
let x be VECTOR of V; ::_thesis: psi . x <= ||.x.||
 q . x = ||.x.|| by NORMSP_0:def_1;
hence  psi . x <= ||.x.|| by A4; ::_thesis: verum
end;