let X be RealNormSpace; :: thesis: ( not X is trivial implies ex DuX being SubRealNormSpace of DualSp (DualSp X) ex L being Lipschitzian LinearOperator of X,DuX st
( L is bijective & DuX = Im (BidualFunc X) & ( for x being Point of X holds L . x = BiDual x ) & ( for x being Point of X holds ||.x.|| = ||.(L . x).|| ) ) )
assume A0: not X is trivial ; :: thesis: ex DuX being SubRealNormSpace of DualSp (DualSp X) ex L being Lipschitzian LinearOperator of X,DuX st
( L is bijective & DuX = Im (BidualFunc X) & ( for x being Point of X holds L . x = BiDual x ) & ( for x being Point of X holds ||.x.|| = ||.(L . x).|| ) )
set F = BidualFunc X;
set V1 = rng (BidualFunc X);
D0: rng (BidualFunc X) is linearly-closed by NORMSP_3:35;
rng (BidualFunc X) <> {}

proof

assume rng (BidualFunc X) = {} ; :: thesis: contradiction
then dom (BidualFunc X) = {} by RELAT_1:42;
hence contradiction by FUNCT_2:def 1; :: thesis: verum

end;

then the carrier of (Lin (rng (BidualFunc X))) = rng (BidualFunc X) by NORMSP_3:31, D0;
then C4: the carrier of (Im (BidualFunc X)) = rng (BidualFunc X) ;
then reconsider L = BidualFunc X as Function of X,(Im (BidualFunc X)) by FUNCT_2:6;
A3: ( BidualFunc X is additive & BidualFunc X is homogeneous ) ;
B0: L is additive

proof

let x, y be Point of X; :: according to VECTSP_1:def 19 :: thesis: L . (x + y) = (L . x) + (L . y)
L . (x + y) = ((BidualFunc X) . x) + ((BidualFunc X) . y) by A3;
hence L . (x + y) = (L . x) + (L . y) by NORMSP_3:28; :: thesis: verum

end;

L is homogeneous

proof

let x be Point of X; :: according to LOPBAN_1:def 5 :: thesis: for b₁ being object holds L . (b₁ * x) = b₁ * (L . x)
let r be Real; :: thesis: L . (r * x) = r * (L . x)
L . (r * x) = r * ((BidualFunc X) . x) by LOPBAN_1:def 5;
hence L . (r * x) = r * (L . x) by NORMSP_3:28; :: thesis: verum

end;

then reconsider L = L as LinearOperator of X,(Im (BidualFunc X)) by B0;
P5: for x being Point of X holds ||.x.|| = ||.(L . x).||

proof

let x be Point of X; :: thesis: ||.x.|| = ||.(L . x).||
||.x.|| = ||.((BidualFunc X) . x).|| by A0, LMNORM;
hence ||.x.|| = ||.(L . x).|| by NORMSP_3:28; :: thesis: verum

end;

then for x being Point of X holds ||.(L . x).|| <= 1 * ||.x.|| ;
then reconsider L = L as Lipschitzian LinearOperator of X,(Im (BidualFunc X)) by LOPBAN_1:def 8;
take Im (BidualFunc X) ; :: thesis: ex L being Lipschitzian LinearOperator of X,(Im (BidualFunc X)) st
( L is bijective & Im (BidualFunc X) = Im (BidualFunc X) & ( for x being Point of X holds L . x = BiDual x ) & ( for x being Point of X holds ||.x.|| = ||.(L . x).|| ) )
take L ; :: thesis: ( L is bijective & Im (BidualFunc X) = Im (BidualFunc X) & ( for x being Point of X holds L . x = BiDual x ) & ( for x being Point of X holds ||.x.|| = ||.(L . x).|| ) )
( L is one-to-one & L is onto ) by C4;
hence ( L is bijective & Im (BidualFunc X) = Im (BidualFunc X) & ( for x being Point of X holds L . x = BiDual x ) & ( for x being Point of X holds ||.x.|| = ||.(L . x).|| ) ) by Def2, P5; :: thesis: verum