defpred S1[ set ] means ( \$1 is empty or P1[\$1] );
A3: for x, B being set st x in F2() & B c= F2() & S1[B] holds
S1[B \/ {x}]
proof
let x, B be set ; :: thesis: ( x in F2() & B c= F2() & S1[B] implies S1[B \/ {x}] )
assume that
A4: x in F2() and
A5: B c= F2() and
A6: S1[B] ; :: thesis: S1[B \/ {x}]
A7: F2() c= Permutations F1() by FINSUB_1:def 5;
then reconsider x = x as Element of Permutations F1() by A4;
A8: B c= Permutations F1() by ;
per cases ( x in B or ( not B is empty & not x in B ) or B is empty ) ;
suppose A9: x in B ; :: thesis: S1[B \/ {x}]
then reconsider B = B as non empty Element of Fin (Permutations F1()) by ;
{x} c= B by ;
hence S1[B \/ {x}] by ; :: thesis: verum
end;
suppose A10: ( not B is empty & not x in B ) ; :: thesis: S1[B \/ {x}]
then reconsider B = B as non empty Element of Fin (Permutations F1()) by ;
P1[B \/ {x}] by A2, A4, A5, A6, A10;
hence S1[B \/ {x}] ; :: thesis: verum
end;
end;
end;
A11: S1[ {} ] ;
A12: F2() is finite ;
S1[F2()] from FINSET_1:sch 2(A12, A11, A3);
hence P1[F2()] ; :: thesis: verum