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;

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

hence
||.f1.|| = |.g1.|
by A2, PARTFUN1:5; :: thesis: verum||.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;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