let V, C be set ; :: thesis: for A, B being Element of Fin (PFuncs (V,C)) holds mi (A ^ (mi B)) = mi (A ^ B)
let A, B be Element of Fin (PFuncs (V,C)); :: thesis: mi (A ^ (mi B)) = mi (A ^ B)
( A ^ (mi B) = (mi B) ^ A & A ^ B = B ^ A ) by Th3;
hence mi (A ^ (mi B)) = mi (A ^ B) by Th19; :: thesis: verum