defpred S₁[ set ] means ( $1 is empty or P₁[$1] );
A3: for x, B being set st x in F₂() & B c= F₂() & S₁[B] holds
S₁[B \/ {x}]

proof

let x, B be set ; :: thesis: ( x in F₂() & B c= F₂() & S₁[B] implies S₁[B \/ {x}] )
assume that
A4: x in F₂() and
A5: B c= F₂() and
A6: S₁[B] ; :: thesis: S₁[B \/ {x}]
A7: F₂() c= Permutations F₁() by FINSUB_1:def 5;
then reconsider x = x as Element of Permutations F₁() by A4;
A8: B c= Permutations F₁() by A5, A7, XBOOLE_1:1;

per cases ( x in B or ( not B is empty & not x in B ) or B is empty ) ;

suppose A9: x in B ; :: thesis: S₁[B \/ {x}]

then reconsider B = B as non empty Element of Fin (Permutations F₁()) by A5, A8, FINSUB_1:def 5;
{x} c= B by A9, ZFMISC_1:31;
hence S₁[B \/ {x}] by A6, XBOOLE_1:12; :: thesis: verum

end;

suppose A10: ( not B is empty & not x in B ) ; :: thesis: S₁[B \/ {x}]

then reconsider B = B as non empty Element of Fin (Permutations F₁()) by A5, A8, FINSUB_1:def 5;
P₁[B \/ {x}] by A2, A4, A5, A6, A10;
hence S₁[B \/ {x}] ; :: thesis: verum

end;

suppose B is empty ; :: thesis: S₁[B \/ {x}]

then P₁[B \/ {x}] by A1, A4;
hence S₁[B \/ {x}] ; :: thesis: verum

end;

end;

end;

A11: S₁[ {} ] ;
A12: F₂() is finite ;
S₁[F₂()] from FINSET_1:sch 2(A12, A11, A3);
hence P₁[F₂()] ; :: thesis: verum