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 ;

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

hence
BoundedLinearFunctionalsNorm X = BoundedLinearFunctionalsNorm (RUSp2RNSp X)
by A1; :: thesis: verum(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;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