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, Th14;

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)

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 b in A ^ B ; :: thesis: ( b c= a implies b = a )
then consider c being finite set such that
A4: c c= b and
A5: c in (mi A) ^ B by Lm2;
assume A6: b c= a ; :: thesis: b = a
then c c= a by A4;
then c = a by A2, A5, Th6;
hence b = a by A4, A6; :: thesis: verum

end;

( a in (mi A) ^ B & a is finite ) by A2, Lm1, Th6;
hence a in mi (A ^ B) by A1, A3, Th7; :: 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)
A7: mi (A ^ B) c= (mi A) ^ B by Th17;

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 A8: a in mi (A ^ B) ; :: thesis: a in mi ((mi A) ^ B)
then ( a is finite & ( for b being finite set st b in (mi A) ^ B & b c= a holds
b = a ) ) by A1, Lm1, Th6;
hence a in mi ((mi A) ^ B) by A7, A8, Th7; :: thesis: verum

end;

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