let X be set ; :: thesis: for A being Subset of X holds ((0,1) --> (1,0)) * (chi ((A `),X)) = chi (A,X)
let A be Subset of X; :: thesis: ((0,1) --> (1,0)) * (chi ((A `),X)) = chi (A,X)
thus ((0,1) --> (1,0)) * (chi ((A `),X)) = chi (((A `) `),X) by Th8
.= chi (A,X) ; :: thesis: verum