let n be Element of NAT ; :: thesis: for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,(REAL n)
for g being Function of A,(REAL n) st f = g holds
|.f.| = |.g.|
let A be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of REAL,(REAL n)
for g being Function of A,(REAL n) st f = g holds
|.f.| = |.g.|
let f be PartFunc of REAL,(REAL n); :: thesis: for g being Function of A,(REAL n) st f = g holds
|.f.| = |.g.|
let g be Function of A,(REAL n); :: thesis: ( f = g implies |.f.| = |.g.| )
assume A1: f = g ; :: thesis: |.f.| = |.g.|
A2: dom |.f.| = dom f by NFCONT_4:def 2
.= dom |.g.| by A1, NFCONT_4:def 2 ;

now :: thesis: for x being object st x in dom |.f.| holds
|.f.| . x = |.g.| . x

let x be object ; :: thesis: ( x in dom |.f.| implies |.f.| . x = |.g.| . x )
assume A3: x in dom |.f.| ; :: thesis: |.f.| . x = |.g.| . x
thus |.f.| . x = |.f.| /. x by A3, PARTFUN1:def 6
.= |.(f /. x).| by A3, NFCONT_4:def 2
.= |.g.| /. x by A1, A2, A3, NFCONT_4:def 2
.= |.g.| . x by A2, A3, PARTFUN1:def 6 ; :: thesis: verum

end;

hence |.f.| = |.g.| by A2, FUNCT_1:2; :: thesis: verum