let n be Element of NAT ; :: thesis: for W being non empty set
for f1 being PartFunc of W,(REAL-NS n)
for g1 being PartFunc of W,(REAL n) st f1 = g1 holds
||.f1.|| = |.g1.|
let W be non empty set ; :: thesis: for f1 being PartFunc of W,(REAL-NS n)
for g1 being PartFunc of W,(REAL n) st f1 = g1 holds
||.f1.|| = |.g1.|
let f1 be PartFunc of W,(REAL-NS n); :: thesis: for g1 being PartFunc of W,(REAL n) st f1 = g1 holds
||.f1.|| = |.g1.|
let g1 be PartFunc of W,(REAL n); :: thesis: ( f1 = g1 implies ||.f1.|| = |.g1.| )
assume A1: f1 = g1 ; :: thesis: ||.f1.|| = |.g1.|
dom ||.f1.|| = dom f1 by NORMSP_0:def 3;
then A2: dom ||.f1.|| = dom |.g1.| by A1, Def2;

now :: thesis: for x being Element of W st x in dom ||.f1.|| holds
||.f1.|| . x = |.g1.| . x

let x be Element of W; :: thesis: ( x in dom ||.f1.|| implies ||.f1.|| . x = |.g1.| . x )
assume A3: x in dom ||.f1.|| ; :: thesis: ||.f1.|| . x = |.g1.| . x
A4: f1 /. x = g1 /. x by A1, REAL_NS1:def 4;
set y1 = g1 /. x;
A5: ||.(f1 /. x).|| = |.(g1 /. x).| by A4, REAL_NS1:1;
A6: ||.f1.|| . x = ||.(f1 /. x).|| by A3, NORMSP_0:def 3;
|.g1.| /. x = |.(g1 /. x).| by A2, A3, Def2;
hence ||.f1.|| . x = |.g1.| . x by A2, A3, A5, A6, PARTFUN1:def 6; :: thesis: verum

end;

hence ||.f1.|| = |.g1.| by A2, PARTFUN1:5; :: thesis: verum