let V, C be set ; :: thesis: for K, L being Element of Fin (PFuncs (V,C)) holds mi ((K ^ L) \/ L) = mi L
let K, L be Element of Fin (PFuncs (V,C)); :: thesis: mi ((K ^ L) \/ L) = mi L

now :: thesis: for a being set st a in mi ((K ^ L) \/ L) holds
a in mi L

let a be set ; :: thesis: ( a in mi ((K ^ L) \/ L) implies a in mi L )
assume A1: a in mi ((K ^ L) \/ L) ; :: thesis: a in mi L
then a in (K ^ L) \/ L by Th6;
then A2: ( a in K ^ L or a in L ) by XBOOLE_0:def 3;

A3: now :: thesis: for b being finite set st b in L & b c= a holds
b = a

let b be finite set ; :: thesis: ( b in L & b c= a implies b = a )
assume b in L ; :: thesis: ( b c= a implies b = a )
then b in (K ^ L) \/ L by XBOOLE_0:def 3;
hence ( b c= a implies b = a ) by A1, Th6; :: thesis: verum

end;

A4: now :: thesis: ( a in K ^ L implies a in L )

assume a in K ^ L ; :: thesis: a in L
then consider b being set such that
A5: b in L and
A6: b c= a by Lm3;
b in (K ^ L) \/ L by A5, XBOOLE_0:def 3;
hence a in L by A1, A5, A6, Th6; :: thesis: verum

end;

a is finite by A1, Lm1;
hence a in mi L by A2, A4, A3, Th7; :: thesis: verum

end;

hence mi ((K ^ L) \/ L) c= mi L ; :: according to XBOOLE_0:def 10 :: thesis: mi L c= mi ((K ^ L) \/ L)

now :: thesis: for a being set st a in mi L holds
a in mi ((K ^ L) \/ L)

let a be set ; :: thesis: ( a in mi L implies a in mi ((K ^ L) \/ L) )
assume A7: a in mi L ; :: thesis: a in mi ((K ^ L) \/ L)
then A8: a in L by Th6;
then A9: a in (K ^ L) \/ L by XBOOLE_0:def 3;

A10: now :: thesis: for b being finite set st b in (K ^ L) \/ L & b c= a holds
b = a

let b be finite set ; :: thesis: ( b in (K ^ L) \/ L & b c= a implies b = a )
assume b in (K ^ L) \/ L ; :: thesis: ( b c= a implies b = a )
then A11: ( b in K ^ L or b in L ) by XBOOLE_0:def 3;
assume A12: b c= a ; :: thesis: b = a

now :: thesis: ( b in K ^ L implies b in L )

assume b in K ^ L ; :: thesis: b in L
then consider c being set such that
A13: c in L and
A14: c c= b by Lm3;
c c= a by A12, A14;
then c = a by A7, A13, Th6;
hence b in L by A8, A12, A14, XBOOLE_0:def 10; :: thesis: verum

end;

hence b = a by A7, A11, A12, Th6; :: thesis: verum

end;

a is finite by A7, Lm1;
hence a in mi ((K ^ L) \/ L) by A9, A10, Th7; :: thesis: verum

end;

hence mi L c= mi ((K ^ L) \/ L) ; :: thesis: verum