let X be RealUnitarySpace; :: thesis: BoundedLinearFunctionalsNorm X = BoundedLinearFunctionalsNorm (RUSp2RNSp X)
set Y = RUSp2RNSp X;
set f = BoundedLinearFunctionalsNorm X;
set g = BoundedLinearFunctionalsNorm (RUSp2RNSp X);
A1: dom (BoundedLinearFunctionalsNorm X) = BoundedLinearFunctionals X by FUNCT_2:def 1
.= BoundedLinearFunctionals (RUSp2RNSp X) by LM6
.= dom (BoundedLinearFunctionalsNorm (RUSp2RNSp X)) by FUNCT_2:def 1 ;

now :: thesis: for x being object st x in dom (BoundedLinearFunctionalsNorm X) holds
(BoundedLinearFunctionalsNorm X) . x = (BoundedLinearFunctionalsNorm (RUSp2RNSp X)) . x

let x be object ; :: thesis: ( x in dom (BoundedLinearFunctionalsNorm X) implies (BoundedLinearFunctionalsNorm X) . x = (BoundedLinearFunctionalsNorm (RUSp2RNSp X)) . x )
assume B11: x in dom (BoundedLinearFunctionalsNorm X) ; :: thesis: (BoundedLinearFunctionalsNorm X) . x = (BoundedLinearFunctionalsNorm (RUSp2RNSp X)) . x
then B1: x in BoundedLinearFunctionals X ;
B2: (BoundedLinearFunctionalsNorm X) . x = upper_bound (PreNorms (Bound2Lipschitz (x,X))) by B11, Def14;
B31: x in BoundedLinearFunctionals (RUSp2RNSp X) by B1, LM6;
Bound2Lipschitz (x,X) = Bound2Lipschitz (x,(RUSp2RNSp X)) by LM6;
then upper_bound (PreNorms (Bound2Lipschitz (x,X))) = upper_bound (PreNorms (Bound2Lipschitz (x,(RUSp2RNSp X)))) by LM8;
hence (BoundedLinearFunctionalsNorm X) . x = (BoundedLinearFunctionalsNorm (RUSp2RNSp X)) . x by B2, B31, DUALSP01:def 14; :: thesis: verum

end;

hence BoundedLinearFunctionalsNorm X = BoundedLinearFunctionalsNorm (RUSp2RNSp X) by A1; :: thesis: verum