let NORM1, NORM2 be Function of (REAL n),REAL; :: thesis: ( ( for x being Element of REAL n holds NORM1 . x = Sum (abs x) ) & ( for x being Element of REAL n holds NORM2 . x = Sum (abs x) ) implies NORM1 = NORM2 )
assume that
A3: for x being Element of REAL n holds NORM1 . x = Sum (abs x) and
A4: for x being Element of REAL n holds NORM2 . x = Sum (abs 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
thus NORM1 . x = Sum (abs x) by A3
.= NORM2 . x by A4 ; :: thesis: verum

end;

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