let X be non empty set ; :: thesis: for A being set
for r being Real holds r (#) (chi (A,X)) = chi (r,A,X)
let A be set ; :: thesis: for r being Real holds r (#) (chi (A,X)) = chi (r,A,X)
let r be Real; :: thesis: r (#) (chi (A,X)) = chi (r,A,X)
for x being Element of X holds (r (#) (chi (A,X))) . x = (chi (r,A,X)) . x

proof

let x be Element of X; :: thesis: (r (#) (chi (A,X))) . x = (chi (r,A,X)) . x
x in X ;
then x in dom (r (#) (chi (A,X))) by FUNCT_2:def 1;
then A2: (r (#) (chi (A,X))) . x = r * ((chi (A,X)) . x) by MESFUNC1:def 6;

per cases ( x in A or not x in A ) ;

suppose x in A ; :: thesis: (r (#) (chi (A,X))) . x = (chi (r,A,X)) . x

then ( (chi (A,X)) . x = 1 & (chi (r,A,X)) . x = r ) by Def1, FUNCT_3:def 3;
hence (r (#) (chi (A,X))) . x = (chi (r,A,X)) . x by A2, XXREAL_3:81; :: thesis: verum

end;

suppose not x in A ; :: thesis: (r (#) (chi (A,X))) . x = (chi (r,A,X)) . x

then ( (chi (A,X)) . x = 0 & (chi (r,A,X)) . x = 0 ) by Def1, FUNCT_3:def 3;
hence (r (#) (chi (A,X))) . x = (chi (r,A,X)) . x by A2; :: thesis: verum

end;

end;

end;

hence r (#) (chi (A,X)) = chi (r,A,X) by FUNCT_2:def 8; :: thesis: verum