let r be Real; :: thesis: for X being set
for g being PartFunc of X,REAL holds less_dom (g,r) = g " ].-infty,r.[
let X be set ; :: thesis: for g being PartFunc of X,REAL holds less_dom (g,r) = g " ].-infty,r.[
let g be PartFunc of X,REAL; :: thesis: less_dom (g,r) = g " ].-infty,r.[
for z being object holds
( z in less_dom (g,r) iff z in g " ].-infty,r.[ )

proof

let z be object ; :: thesis: ( z in less_dom (g,r) iff z in g " ].-infty,r.[ )

hereby :: thesis: ( z in g " ].-infty,r.[ implies z in less_dom (g,r) )

assume A1: z in less_dom (g,r) ; :: thesis: z in g " ].-infty,r.[
then A2: ( z in dom g & g . z < r ) by MESFUNC1:def 11;
( -infty < g . z & g . z < r ) by A1, XREAL_0:def 1, XXREAL_0:12, MESFUNC1:def 11;
then g . z in ].-infty,r.[ ;
hence z in g " ].-infty,r.[ by A2, FUNCT_1:def 7; :: thesis: verum

end;

assume z in g " ].-infty,r.[ ; :: thesis: z in less_dom (g,r)
then A3: ( z in dom g & g . z in ].-infty,r.[ ) by FUNCT_1:def 7;
then ex t being Real st
( t = g . z & -infty < t & t < r ) ;
hence z in less_dom (g,r) by A3, MESFUNC1:def 11; :: thesis: verum

end;

hence less_dom (g,r) = g " ].-infty,r.[ by TARSKI:2; :: thesis: verum