begin
begin
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 ) )
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
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
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
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