let NORM1, NORM2 be Function of X,REAL; :: thesis: ( ( for x being Element of X ex y being Element of (RLSp2RVSp X) ex z being Element of REAL (dim X) st
( x = y & z = y |-- b & NORM1 . x = (sum_norm (dim X)) . z ) ) & ( for x being Element of X ex y being Element of (RLSp2RVSp X) ex z being Element of REAL (dim X) st
( x = y & z = y |-- b & NORM2 . x = (sum_norm (dim X)) . z ) ) implies NORM1 = NORM2 )
assume that
A3: for x being Element of X ex y being Element of (RLSp2RVSp X) ex z being Element of REAL (dim X) st
( x = y & z = y |-- b & NORM1 . x = (sum_norm (dim X)) . z ) and
A4: for x being Element of X ex y being Element of (RLSp2RVSp X) ex z being Element of REAL (dim X) st
( x = y & z = y |-- b & NORM2 . x = (sum_norm (dim X)) . z ) ; :: thesis: NORM1 = NORM2
for x being Element of X holds NORM1 . x = NORM2 . x
proof
let x be Element of X; :: thesis: NORM1 . x = NORM2 . x
A5: ex y being Element of (RLSp2RVSp X) ex z being Element of REAL (dim X) st
( y = x & z = y |-- b & NORM1 . x = (sum_norm (dim X)) . z ) by A3;
ex y being Element of (RLSp2RVSp X) ex z being Element of REAL (dim X) st
( y = x & z = y |-- b & NORM2 . x = (sum_norm (dim X)) . z ) by A4;
hence NORM1 . x = NORM2 . x by A5; :: thesis: verum
end;
hence NORM1 = NORM2 by FUNCT_2:63; :: thesis: verum