defpred S1[ set ] means P1[F2() \/ $1];
set D = F1() \ F2();
A4: F1() \ F2() is finite by A1;
A5: for x, E being set st x in F1() \ F2() & E c= F1() \ F2() & S1[E] holds
S1[E \/ {x}]
proof
let x, E be set ; :: thesis: ( x in F1() \ F2() & E c= F1() \ F2() & S1[E] implies S1[E \/ {x}] )
assume that
A6: x in F1() \ F2() and
A7: E c= F1() \ F2() and
A8: S1[E] ; :: thesis: S1[E \/ {x}]
set C = F2() \/ E;
F2() \/ E c= F2() \/ (F1() \ F2()) by A7, XBOOLE_1:9;
then F2() \/ E c= F1() by XBOOLE_1:45;
then P1[(F2() \/ E) \/ {x}] by A3, A6, A8, XBOOLE_1:7;
hence S1[E \/ {x}] by XBOOLE_1:4; :: thesis: verum
end;
A10: S1[ {} ] by A2;
S1[F1() \ F2()] from FINSET_1:sch 2(A4, A10, A5);
 hence P1[F1()] by XBOOLE_1:45; :: thesis: verum