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 AS: <>* f = g ; :: thesis: |.f.| = |.g.|
A1: dom |.g.| = dom g by NFCONT_4:def 2
.= dom f by AS, LMXTh0 ;
then A2: 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 A3: x in dom |.g.| ; :: thesis: |.g.| . x = |.f.| . x
then A6: g /. x = <*(f /. x)*> by AS, A1, XTh30;
thus |.g.| . x = |.g.| /. x by A3, PARTFUN1:def 6
.= |.(g /. x).| by A3, NFCONT_4:def 2
.= |.(f /. x).| by A6, XTh30D
.= |.(f . x).| by A1, A3, PARTFUN1:def 6
.= |.f.| . x by VALUED_1:18 ; :: thesis: verum

end;

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