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)
(A `) ` = A ;
hence ((0,1) --> (1,0)) * (chi ((A `),X)) = chi (A,X) by Th7; :: thesis: verum