let i be Element of NAT ; :: thesis: for f being PartFunc of (REAL i),REAL
for g being PartFunc of (REAL i),(REAL 1) st <>* f = g holds
|.f.| = |.g.|
let f be PartFunc of (REAL i),REAL; :: thesis: for g being PartFunc of (REAL i),(REAL 1) st <>* f = g holds
|.f.| = |.g.|
let g be PartFunc of (REAL i),(REAL 1); :: thesis: ( <>* f = g implies |.f.| = |.g.| )
assume A1: <>* f = g ; :: thesis: |.f.| = |.g.|
A2: dom |.g.| = dom g by NFCONT_4:def 2
.= dom f by A1, Th3 ;
then A3: dom |.g.| = dom |.f.| by VALUED_1:def 11;

now :: thesis: for x being Element of REAL i st x in dom |.g.| holds
|.g.| . x = |.f.| . x

let x be Element of REAL i; :: thesis: ( x in dom |.g.| implies |.g.| . x = |.f.| . x )
assume A4: x in dom |.g.| ; :: thesis: |.g.| . x = |.f.| . x
then A5: g /. x = <*(f /. x)*> by A1, A2, Th6;
thus |.g.| . x = |.g.| /. x by A4, PARTFUN1:def 6
.= |.(g /. x).| by A4, NFCONT_4:def 2
.= |.(f /. x).| by A5, Lm1
.= |.(f . x).| by A2, A4, PARTFUN1:def 6
.= |.f.| . x by VALUED_1:18 ; :: thesis: verum

end;

hence |.f.| = |.g.| by A3, PARTFUN1:5; :: thesis: verum