let V, C be set ; 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)); 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 ; ( a in A ^ B implies ex b being finite set st
( b c= a & b in (mi A) ^ B ) )
assume
a in A ^ B
; 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
; ( e c= a & e in (mi A) ^ B )
thus
e c= a
by A1, A5, XBOOLE_1:9; e in (mi A) ^ B
thus
e in (mi A) ^ B
by A3, A6, A8; verum