let V, C be set ; :: thesis: for A, B being Element of Fin (PFuncs (V,C))
for a being finite set st a in A ^ B holds
ex b being finite set st
( b c= a & b in (mi A) ^ B )
let A, B be Element of Fin (PFuncs (V,C)); :: thesis: for a being finite set st a in A ^ B holds
ex b being finite set st
( b c= a & b in (mi A) ^ B )
let a be finite set ; :: thesis: ( a in A ^ B implies ex b being finite set st
( b c= a & b in (mi A) ^ B ) )
assume a in A ^ B ; :: thesis: ex b being finite set st
( b c= a & b in (mi A) ^ B )
then consider b, c being Element of PFuncs (V,C) such that
A1: a = b \/ c and
A2: b in A and
A3: c in B and
A4: b tolerates c ;
b is finite by A1, FINSET_1:1, XBOOLE_1:7;
then consider d being set such that
A5: d c= b and
A6: d in mi A by A2, Th10;
A7: mi A c= PFuncs (V,C) by FINSUB_1:def 5;
then reconsider d9 = d, c9 = c as Element of PFuncs (V,C) by A6;
reconsider d1 = d, b1 = b, c1 = c as PartFunc of V,C by A6, A7, PARTFUN1:46;
d1 c= b1 by A5;
then A8: d9 tolerates c9 by A4, PARTFUN1:58;
then d9 \/ c9 = d9 +* c9 by FUNCT_4:30;
then reconsider e = d1 \/ c1 as Element of PFuncs (V,C) by PARTFUN1:45;
reconsider e = e as finite set by A1, A5, FINSET_1:1, XBOOLE_1:9;
take e ; :: thesis: ( e c= a & e in (mi A) ^ B )
thus e c= a by A1, A5, XBOOLE_1:9; :: thesis: e in (mi A) ^ B
thus e in (mi A) ^ B by A3, A6, A8; :: thesis: verum