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 is bounded & f = g holds
g is bounded
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 is bounded & f = g holds
g is bounded
let f be PartFunc of REAL,(REAL n); :: thesis: for g being Function of A,(REAL n) st f is bounded & f = g holds
g is bounded
let g be Function of A,(REAL n); :: thesis: ( f is bounded & f = g implies g is bounded )
assume A1: ( f is bounded & f = g ) ; :: thesis: g is bounded
let i be Element of NAT ; :: according to INTEGR15:def 12 :: thesis: ( not i in Seg n or (proj (i,n)) * g is bounded )
thus ( not i in Seg n or (proj (i,n)) * g is bounded ) by A1, INTEGR15:def 15; :: thesis: verum