let A be set ; :: thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi ((mi B) ^ C) = mi (B ^ C)
let B, C be Element of Fin (DISJOINT_PAIRS A); :: thesis: mi ((mi B) ^ C) = mi (B ^ C)
A1: (mi B) ^ C c= B ^ C by Th40, Th46;

now :: thesis: for a being Element of DISJOINT_PAIRS A st a in mi ((mi B) ^ C) holds
a in mi (B ^ C)

let a be Element of DISJOINT_PAIRS A; :: thesis: ( a in mi ((mi B) ^ C) implies a in mi (B ^ C) )
assume A2: a in mi ((mi B) ^ C) ; :: thesis: a in mi (B ^ C)

A3: now :: thesis: for b being Element of DISJOINT_PAIRS A st b in B ^ C & b c= a holds
b = a

let b be Element of DISJOINT_PAIRS A; :: thesis: ( b in B ^ C & b c= a implies b = a )
assume b in B ^ C ; :: thesis: ( b c= a implies b = a )
then consider c being Element of DISJOINT_PAIRS A such that
A4: c c= b and
A5: c in (mi B) ^ C by Lm6;
assume A6: b c= a ; :: thesis: b = a
then c c= a by A4, Th2;
then c = a by A2, A5, Th36;
hence b = a by A4, A6, Th1; :: thesis: verum

end;

a in (mi B) ^ C by A2, Th36;
hence a in mi (B ^ C) by A1, A3, Th39; :: thesis: verum

end;

hence mi ((mi B) ^ C) c= mi (B ^ C) by Lm5; :: according to XBOOLE_0:def 10 :: thesis: mi (B ^ C) c= mi ((mi B) ^ C)
A7: mi (B ^ C) c= (mi B) ^ C by Th47;

now :: thesis: for a being Element of DISJOINT_PAIRS A st a in mi (B ^ C) holds
a in mi ((mi B) ^ C)

let a be Element of DISJOINT_PAIRS A; :: thesis: ( a in mi (B ^ C) implies a in mi ((mi B) ^ C) )
assume A8: a in mi (B ^ C) ; :: thesis: a in mi ((mi B) ^ C)
then for b being Element of DISJOINT_PAIRS A st b in (mi B) ^ C & b c= a holds
b = a by A1, Th36;
hence a in mi ((mi B) ^ C) by A7, A8, Th39; :: thesis: verum

end;

hence mi (B ^ C) c= mi ((mi B) ^ C) by Lm5; :: thesis: verum