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;
A2: mi (A ^ B) c= (mi A) ^ B by Th17;

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;
A5: a is finite by A3, Lm1;

now

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
A6: c c= b and
A7: c in (mi A) ^ B by Lm3;
assume A8: b c= a ; :: thesis: b = a
then c c= a by A6, XBOOLE_1:1;
then c = a by A3, A7, Th6;
hence b = a by A6, A8, XBOOLE_0:def 10; :: thesis: verum

end;

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

end;

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