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:
A2: dom |.f.| = dom f by NFCONT_4:def 2
.= dom |.g.| by ;
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
.= |.(f /. x).| by
.= |.g.| /. x by
.= |.g.| . x by ; :: thesis: verum
end;
hence |.f.| = |.g.| by ; :: thesis: verum