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 ;

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

hence
|.f.| = |.g.|
by A2, FUNCT_1:2; :: thesis: verum|.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;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