let NORM1, NORM2 be Function of (REAL n),REAL; :: thesis: ( ( for x being Element of REAL n holds
( NORM1 . x in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= NORM1 . x ) ) ) & ( for x being Element of REAL n holds
( NORM2 . x in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= NORM2 . x ) ) ) implies NORM1 = NORM2 )
assume that
A5: for x being Element of REAL n holds
( NORM1 . x in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= NORM1 . x ) ) and
A6: for x being Element of REAL n holds
( NORM2 . x in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= NORM2 . x ) ) ; :: thesis: NORM1 = NORM2
for x being Element of REAL n holds NORM1 . x = NORM2 . x

proof

let x be Element of REAL n; :: thesis: NORM1 . x = NORM2 . x
A7: ( NORM1 . x in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= NORM1 . x ) ) by A5;
( NORM2 . x in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= NORM2 . x ) ) by A6;
then consider i being object such that
A8: ( i in dom (abs x) & NORM2 . x = (abs x) . i ) by FUNCT_1:def 3;
A9: dom (abs x) = dom x by VALUED_1:def 11;
reconsider i = i as Nat by A8;
A10: NORM2 . x <= NORM1 . x by A5, A8, A9;
consider j being object such that
A11: ( j in dom (abs x) & NORM1 . x = (abs x) . j ) by A7, FUNCT_1:def 3;
NORM1 . x <= NORM2 . x by A6, A9, A11;
hence NORM1 . x = NORM2 . x by XXREAL_0:1, A10; :: thesis: verum

end;

hence NORM1 = NORM2 by FUNCT_2:63; :: thesis: verum