let A be set ; :: thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi (B ^ (mi C)) = mi (B ^ C)
let B, C be Element of Fin (DISJOINT_PAIRS A); :: thesis: mi (B ^ (mi C)) = mi (B ^ C)
( B ^ (mi C) = (mi C) ^ B & B ^ C = C ^ B ) by Th48;
hence mi (B ^ (mi C)) = mi (B ^ C) by Th50; :: thesis: verum