defpred S_{1}[ set ] means ( $1 is empty or P_{1}[$1] );

A3: for x, B being set st x in F_{2}() & B c= F_{2}() & S_{1}[B] holds

S_{1}[B \/ {x}]
_{1}[ {} ]
;

A12: F_{2}() is finite
;

S_{1}[F_{2}()]
from FINSET_1:sch 2(A12, A11, A3);

hence P_{1}[F_{2}()]
; :: thesis: verum

A3: for x, B being set st x in F

S

proof

A11:
S
let x, B be set ; :: thesis: ( x in F_{2}() & B c= F_{2}() & S_{1}[B] implies S_{1}[B \/ {x}] )

assume that

A4: x in F_{2}()
and

A5: B c= F_{2}()
and

A6: S_{1}[B]
; :: thesis: S_{1}[B \/ {x}]

A7: F_{2}() c= Permutations F_{1}()
by FINSUB_1:def 5;

then reconsider x = x as Element of Permutations F_{1}() by A4;

A8: B c= Permutations F_{1}()
by A5, A7, XBOOLE_1:1;

end;assume that

A4: x in F

A5: B c= F

A6: S

A7: F

then reconsider x = x as Element of Permutations F

A8: B c= Permutations F

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

end;

suppose A9:
x in B
; :: thesis: S_{1}[B \/ {x}]

then reconsider B = B as non empty Element of Fin (Permutations F_{1}()) by A8, FINSUB_1:def 5;

{x} c= B by A9, ZFMISC_1:31;

hence S_{1}[B \/ {x}]
by A6, XBOOLE_1:12; :: thesis: verum

end;{x} c= B by A9, ZFMISC_1:31;

hence S

A12: F

S

hence P