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