let I be non empty closed_interval Subset of REAL; :: thesis: for r being Real
for jauge being positive-yielding Function of I,REAL st jauge = r (#) (chi (I,I)) holds
0 < r
let r be Real; :: thesis: for jauge being positive-yielding Function of I,REAL st jauge = r (#) (chi (I,I)) holds
0 < r
let jauge be positive-yielding Function of I,REAL; :: thesis: ( jauge = r (#) (chi (I,I)) implies 0 < r )
assume A1: jauge = r (#) (chi (I,I)) ; :: thesis: 0 < r
assume A2: r <= 0 ; :: thesis: contradiction
set x = the Element of I;
the Element of I in I ;
then A3: ( the Element of I in dom (chi (I,I)) & the Element of I in dom jauge ) by PARTFUN1:def 2;
then jauge . the Element of I = r * ((chi (I,I)) . the Element of I) by A1, VALUED_1:def 5
.= r * 1 by FUNCT_3:def 3
.= r ;
then ( jauge . the Element of I <= 0 & jauge . the Element of I in rng jauge ) by A2, A3, FUNCT_1:3;
hence contradiction by PARTFUN3:def 1; :: thesis: verum