let X be non empty set ; :: thesis: for A being set
for r being Real holds
( rng (chi (r,A,X)) c= {0,r} & chi (r,A,X) is V121() & chi (r,A,X) is V120() )
let A be set ; :: thesis: for r being Real holds
( rng (chi (r,A,X)) c= {0,r} & chi (r,A,X) is V121() & chi (r,A,X) is V120() )
let r be Real; :: thesis: ( rng (chi (r,A,X)) c= {0,r} & chi (r,A,X) is V121() & chi (r,A,X) is V120() )
now :: thesis: for y being object st y in rng (chi (r,A,X)) holds
y in {0,r}
let y be object ; :: thesis: ( y in rng (chi (r,A,X)) implies b1 in {0,r} )
assume y in rng (chi (r,A,X)) ; :: thesis: b1 in {0,r}
then consider x being object such that
A1: ( x in dom (chi (r,A,X)) & y = (chi (r,A,X)) . x ) by FUNCT_1:def 3;
per cases ( x in A or not x in A ) ;
suppose x in A ; :: thesis: b1 in {0,r}
then (chi (r,A,X)) . x = r by A1, Def1;
hence y in {0,r} by A1, TARSKI:def 2; :: thesis: verum
end;
suppose not x in A ; :: thesis: b1 in {0,r}
then (chi (r,A,X)) . x = 0 by A1, Def1;
hence y in {0,r} by A1, TARSKI:def 2; :: thesis: verum
end;
end;
end;
hence rng (chi (r,A,X)) c= {0,r} ; :: thesis: ( chi (r,A,X) is V121() & chi (r,A,X) is V120() )
( chi (A,X) is V121() & chi (A,X) is V120() ) by Th3;
then ( r (#) (chi (A,X)) is V121() & r (#) (chi (A,X)) is V120() ) ;
hence ( chi (r,A,X) is V121() & chi (r,A,X) is V120() ) by Th1; :: thesis: verum