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
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 A1: a in mi (A \/ B) ; :: thesis: a in (mi A) \/ B
then reconsider a9 = a as finite set by Lm1;
A2: a in A \/ B by A1, Th6;
now :: thesis: a in (mi A) \/ B
per cases ( a in A or a in B ) by A2, XBOOLE_0:def 3;
suppose A3: a in A ; :: thesis: a in (mi A) \/ B
now :: thesis: for b being finite set st b in A & b c= a holds
b = a
let b be finite set ; :: thesis: ( b in A & b c= a implies b = a )
assume b in A ; :: thesis: ( b c= a implies b = a )
then b in A \/ B by XBOOLE_0:def 3;
hence ( b c= a implies b = a ) by A1, Th6; :: thesis: verum
end;
then a9 in mi A by A3, Th7;
hence a in (mi A) \/ B by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
hence a in (mi A) \/ B ; :: thesis: verum
end;
hence mi (A \/ B) c= (mi A) \/ B ; :: thesis: verum