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;
A2: mi (A \/ B) c= (mi A) \/ B by Th12;

now

let a be set ; :: thesis: ( a in mi ((mi A) \/ B) implies a in mi (A \/ B) )
assume A3: a in mi ((mi A) \/ B) ; :: thesis: a in mi (A \/ B)
then A4: a in (mi A) \/ B by Th6;
reconsider a' = a as finite set by A3, Lm1;

now

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

now

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

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

then consider c being set such that
A7: c c= b and
A8: c in mi A by Th10;
A9: c in (mi A) \/ B by A8, XBOOLE_0:def 3;
c c= a by A6, A7, XBOOLE_1:1;
then c = a by A3, A9, Th6;
hence b = a by A6, A7, XBOOLE_0:def 10; :: 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 A3, A6, Th6; :: thesis: verum

end;

end;

end;

hence b = a ; :: thesis: verum

end;

then a' in mi (A \/ B) by A1, A4, Th7;
hence a in mi (A \/ B) ; :: thesis: verum

end;

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

now

let a be set ; :: thesis: ( a in mi (A \/ B) implies a in mi ((mi A) \/ B) )
assume A10: a in mi (A \/ B) ; :: thesis: a in mi ((mi A) \/ B)
then reconsider a' = 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, A10, Th6;
then a' in mi ((mi A) \/ B) by A2, A10, Th7;
hence a in mi ((mi A) \/ B) ; :: thesis: verum

end;

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