let V, C be set ; :: thesis: for A, B being Element of Fin (PFuncs (V,C)) holds mi ((mi A) \/ B) = mi (A \/ B)
let A, B be Element of Fin (PFuncs (V,C)); :: thesis: mi ((mi A) \/ B) = mi (A \/ B)
A1: (mi A) \/ B c= A \/ B by Th8, XBOOLE_1:9;

now :: thesis: for a being set st a in mi ((mi A) \/ B) holds
a in mi (A \/ B)

let a be set ; :: thesis: ( a in mi ((mi A) \/ B) implies a in mi (A \/ B) )
assume A2: a in mi ((mi A) \/ B) ; :: thesis: a in mi (A \/ B)
then reconsider a9 = a as finite set by Lm1;

A3: now :: thesis: for b being finite set st b in A \/ B & b c= a holds
b = a

let b be finite set ; :: thesis: ( b in A \/ B & b c= a implies b = a )
assume that
A4: b in A \/ B and
A5: b c= a ; :: thesis: b = a

now :: thesis: b = a

per cases ( b in A or b in B ) by A4, XBOOLE_0:def 3;

suppose b in A ; :: thesis: b = a

then consider c being set such that
A6: c c= b and
A7: c in mi A by Th10;
( c in (mi A) \/ B & c c= a ) by A5, A6, A7, XBOOLE_0:def 3;
then c = a by A2, Th6;
hence b = a by A5, A6; :: thesis: verum

end;

suppose b in B ; :: thesis: b = a

then b in (mi A) \/ B by XBOOLE_0:def 3;
hence b = a by A2, A5, Th6; :: thesis: verum

end;

end;

end;

hence b = a ; :: thesis: verum

end;

a in (mi A) \/ B by A2, Th6;
then a9 in mi (A \/ B) by A1, A3, Th7;
hence a in mi (A \/ B) ; :: thesis: verum

end;

hence mi ((mi A) \/ B) c= mi (A \/ B) ; :: according to XBOOLE_0:def 10 :: thesis: mi (A \/ B) c= mi ((mi A) \/ B)
A8: mi (A \/ B) c= (mi A) \/ B by Th12;

now :: thesis: for a being set st a in mi (A \/ B) holds
a in mi ((mi A) \/ B)

let a be set ; :: thesis: ( a in mi (A \/ B) implies a in mi ((mi A) \/ B) )
assume A9: a in mi (A \/ B) ; :: thesis: a in mi ((mi A) \/ B)
then reconsider a9 = a as finite set by Lm1;
for b being finite set st b in (mi A) \/ B & b c= a holds
b = a by A1, A9, Th6;
then a9 in mi ((mi A) \/ B) by A8, A9, Th7;
hence a in mi ((mi A) \/ B) ; :: thesis: verum

end;

hence mi (A \/ B) c= mi ((mi A) \/ B) ; :: thesis: verum