let V, C be set ; :: thesis: for A being Element of Fin (PFuncs (V,C)) holds mi (A ^ A) = mi A
let A be Element of Fin (PFuncs (V,C)); :: thesis: mi (A ^ A) = mi A
thus mi (A ^ A) = mi ((A ^ A) \/ A) by Th23, XBOOLE_1:12
.= mi A by Lm4 ; :: thesis: verum