let NORM1, NORM2 be Function of (BoundedLinearFunctionals X),REAL; :: thesis: ( ( for x being object st x in BoundedLinearFunctionals X holds

NORM1 . x = upper_bound (PreNorms (Bound2Lipschitz (x,X))) ) & ( for x being object st x in BoundedLinearFunctionals X holds

NORM2 . x = upper_bound (PreNorms (Bound2Lipschitz (x,X))) ) implies NORM1 = NORM2 )

assume that

A2: for x being object st x in BoundedLinearFunctionals X holds

NORM1 . x = upper_bound (PreNorms (Bound2Lipschitz (x,X))) and

A3: for x being object st x in BoundedLinearFunctionals X holds

NORM2 . x = upper_bound (PreNorms (Bound2Lipschitz (x,X))) ; :: thesis: NORM1 = NORM2

for z being object st z in BoundedLinearFunctionals X holds

NORM1 . z = NORM2 . z

NORM1 . x = upper_bound (PreNorms (Bound2Lipschitz (x,X))) ) & ( for x being object st x in BoundedLinearFunctionals X holds

NORM2 . x = upper_bound (PreNorms (Bound2Lipschitz (x,X))) ) implies NORM1 = NORM2 )

assume that

A2: for x being object st x in BoundedLinearFunctionals X holds

NORM1 . x = upper_bound (PreNorms (Bound2Lipschitz (x,X))) and

A3: for x being object st x in BoundedLinearFunctionals X holds

NORM2 . x = upper_bound (PreNorms (Bound2Lipschitz (x,X))) ; :: thesis: NORM1 = NORM2

for z being object st z in BoundedLinearFunctionals X holds

NORM1 . z = NORM2 . z

proof

hence
NORM1 = NORM2
; :: thesis: verum
let z be object ; :: thesis: ( z in BoundedLinearFunctionals X implies NORM1 . z = NORM2 . z )

assume A5: z in BoundedLinearFunctionals X ; :: thesis: NORM1 . z = NORM2 . z

NORM1 . z = upper_bound (PreNorms (Bound2Lipschitz (z,X))) by A2, A5;

hence NORM1 . z = NORM2 . z by A3, A5; :: thesis: verum

end;assume A5: z in BoundedLinearFunctionals X ; :: thesis: NORM1 . z = NORM2 . z

NORM1 . z = upper_bound (PreNorms (Bound2Lipschitz (z,X))) by A2, A5;

hence NORM1 . z = NORM2 . z by A3, A5; :: thesis: verum