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 :: thesis: for a being set st a in mi (A ^ B) holds
a in (mi A) ^ B

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

end;

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