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