let f be PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st f = g holds
||.f.|| = |.g.|
let g be PartFunc of [:[:REAL,REAL:],REAL:],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 A3, FUNCT_1:2; :: thesis: verum