let n be non zero Nat; :: thesis: for D being n -element FinSequence
for J being closed_interval Subset of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & f is_continuous_on [:(CarProduct D),J:] & f = g holds
for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2 being Point of (CarProduct ((Seg n) --> RNS_Real))
for y1, y2 being Real st [x1,y1] in [:(CarProduct D),J:] & [x2,y2] in [:(CarProduct D),J:] & ||.(x2 - x1).|| < r & |.(y2 - y1).| < r holds
|.((|.g.| . [x2,y2]) - (|.g.| . [x1,y1])).| < e ) )
let D be n -element FinSequence; :: thesis: for J being closed_interval Subset of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & f is_continuous_on [:(CarProduct D),J:] & f = g holds
for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2 being Point of (CarProduct ((Seg n) --> RNS_Real))
for y1, y2 being Real st [x1,y1] in [:(CarProduct D),J:] & [x2,y2] in [:(CarProduct D),J:] & ||.(x2 - x1).|| < r & |.(y2 - y1).| < r holds
|.((|.g.| . [x2,y2]) - (|.g.| . [x1,y1])).| < e ) )
let J be closed_interval Subset of REAL; :: thesis: for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & f is_continuous_on [:(CarProduct D),J:] & f = g holds
for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2 being Point of (CarProduct ((Seg n) --> RNS_Real))
for y1, y2 being Real st [x1,y1] in [:(CarProduct D),J:] & [x2,y2] in [:(CarProduct D),J:] & ||.(x2 - x1).|| < r & |.(y2 - y1).| < r holds
|.((|.g.| . [x2,y2]) - (|.g.| . [x1,y1])).| < e ) )
let f be PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & f is_continuous_on [:(CarProduct D),J:] & f = g holds
for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2 being Point of (CarProduct ((Seg n) --> RNS_Real))
for y1, y2 being Real st [x1,y1] in [:(CarProduct D),J:] & [x2,y2] in [:(CarProduct D),J:] & ||.(x2 - x1).|| < r & |.(y2 - y1).| < r holds
|.((|.g.| . [x2,y2]) - (|.g.| . [x1,y1])).| < e ) )
let g be PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL; :: thesis: ( ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & f is_continuous_on [:(CarProduct D),J:] & f = g implies for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2 being Point of (CarProduct ((Seg n) --> RNS_Real))
for y1, y2 being Real st [x1,y1] in [:(CarProduct D),J:] & [x2,y2] in [:(CarProduct D),J:] & ||.(x2 - x1).|| < r & |.(y2 - y1).| < r holds
|.((|.g.| . [x2,y2]) - (|.g.| . [x1,y1])).| < e ) ) )
assume that
A1: for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL and
A2: f is_continuous_on [:(CarProduct D),J:] and
A3: f = g ; :: thesis: for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2 being Point of (CarProduct ((Seg n) --> RNS_Real))
for y1, y2 being Real st [x1,y1] in [:(CarProduct D),J:] & [x2,y2] in [:(CarProduct D),J:] & ||.(x2 - x1).|| < r & |.(y2 - y1).| < r holds
|.((|.g.| . [x2,y2]) - (|.g.| . [x1,y1])).| < e ) )
||.f.|| = |.g.| by A3, Th38;
hence for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2 being Point of (CarProduct ((Seg n) --> RNS_Real))
for y1, y2 being Real st [x1,y1] in [:(CarProduct D),J:] & [x2,y2] in [:(CarProduct D),J:] & ||.(x2 - x1).|| < r & |.(y2 - y1).| < r holds
|.((|.g.| . [x2,y2]) - (|.g.| . [x1,y1])).| < e ) ) by A1, A2, MESFUN16:22, Th37; :: thesis: verum