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

now

let a be set ; :: thesis: ( a in mi (A ^ B) implies a in (mi A) ^ B )
assume A2: a in mi (A ^ B) ; :: thesis: a in (mi A) ^ B
then A3: a in A ^ B by Th6;
a is finite by A2, Lm1;
then consider b being finite set such that
A4: b c= a and
A5: b in (mi A) ^ B by A3, Lm3;
thus a in (mi A) ^ B by A1, A2, A4, A5, Th6; :: thesis: verum

end;

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