let X be set ; :: thesis: for S being RealNormSpace
for f being PartFunc of S,RNS_Real
for g being PartFunc of X,REAL st f = g holds
||.f.|| = |.g.|
let S be RealNormSpace; :: thesis: for f being PartFunc of S,RNS_Real
for g being PartFunc of X,REAL st f = g holds
||.f.|| = |.g.|
let f be PartFunc of S,RNS_Real; :: thesis: for g being PartFunc of X,REAL st f = g holds
||.f.|| = |.g.|
let g be PartFunc of X,REAL; :: thesis: ( f = g implies ||.f.|| = |.g.| )
assume A1: f = g ; :: thesis: ||.f.|| = |.g.|
A2: dom ||.f.|| = dom f by NORMSP_0:def 3;
then A3: dom ||.f.|| = dom |.g.| by A1, VALUED_1:def 11;
for x being object st x in dom ||.f.|| holds
||.f.|| . x = |.g.| . x

proof

let x be object ; :: thesis: ( x in dom ||.f.|| implies ||.f.|| . x = |.g.| . x )
assume A4: x in dom ||.f.|| ; :: thesis: ||.f.|| . x = |.g.| . x
then A5: ||.f.|| . x = ||.(f /. x).|| by NORMSP_0:def 3;
f /. x = f . x by A4, A2, PARTFUN1:def 6;
then ||.(f /. x).|| = |.(g . x).| by A1, EUCLID:def 2;
hence ||.f.|| . x = |.g.| . x by A3, A4, A5, VALUED_1:def 11; :: thesis: verum

end;

hence ||.f.|| = |.g.| by A2, A1, VALUED_1:def 11; :: thesis: verum