defpred S1[ Nat] means for X being finite set st card X = $1 & X <> {} holds
ex x being object st
( x in X & ( for y being object st y in X holds
P1[x,y] ) );
A4: S1[ 0 ] ;
A5: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A6: for X being finite set st card X = n & X <> {} holds
ex x being object st
( x in X & ( for y being object st y in X holds
P1[x,y] ) ) ; :: thesis: S1[n + 1]
let X be finite set ; :: thesis: ( card X = n + 1 & X <> {} implies ex x being object st
( x in X & ( for y being object st y in X holds
P1[x,y] ) ) )
assume that
A7: card X = n + 1 and
A8: X <> {} ; :: thesis: ex x being object st
( x in X & ( for y being object st y in X holds
P1[x,y] ) )
set x = the Element of X;
A9: now :: thesis: ( X \ { the Element of X} = {} implies ex x being object st
( x in X & ( for y being object st y in X holds
P1[x,y] ) ) )
assume X \ { the Element of X} = {} ; :: thesis: ex x being object st
( x in X & ( for y being object st y in X holds
P1[x,y] ) )
then A10: X c= { the Element of X} by XBOOLE_1:37;
thus ex x being object st
( x in X & ( for y being object st y in X holds
P1[x,y] ) ) :: thesis: verum
proof
take the Element of X ; :: thesis: ( the Element of X in X & ( for y being object st y in X holds
P1[ the Element of X,y] ) )
thus the Element of X in X by A8; :: thesis: for y being object st y in X holds
P1[ the Element of X,y]
let y be object ; :: thesis: ( y in X implies P1[ the Element of X,y] )
assume y in X ; :: thesis: P1[ the Element of X,y]
then y = the Element of X by A10, TARSKI:def 1;
hence P1[ the Element of X,y] by A2; :: thesis: verum
end;
end;
now :: thesis: ( X \ { the Element of X} <> {} implies ex x being object st
( x in X & ( for y being object st y in X holds
P1[x,y] ) ) )
assume A11: X \ { the Element of X} <> {} ; :: thesis: ex x being object st
( x in X & ( for y being object st y in X holds
P1[x,y] ) )
{ the Element of X} c= X by A8, ZFMISC_1:31;
then A12: card (X \ { the Element of X}) = (n + 1) - (card { the Element of X}) by A7, Th43;
card { the Element of X} = 1 by CARD_1:30;
then consider y being object such that
A13: y in X \ { the Element of X} and
A14: for z being object st z in X \ { the Element of X} holds
P1[y,z] by A6, A11, A12;
A15: ( P1[ the Element of X,y] or P1[y, the Element of X] ) by A2;
A16: P1[ the Element of X, the Element of X] by A2;
P1[y,y] by A2;
then consider z being object such that
A17: ( z = the Element of X or z = y ) and
A18: P1[z, the Element of X] and
A19: P1[z,y] by A15, A16;
thus ex x being object st
( x in X & ( for y being object st y in X holds
P1[x,y] ) ) :: thesis: verum
proof
take z ; :: thesis: ( z in X & ( for y being object st y in X holds
P1[z,y] ) )
thus z in X by A13, A17; :: thesis: for y being object st y in X holds
P1[z,y]
let u be object ; :: thesis: ( u in X implies P1[z,u] )
A20: ( u in { the Element of X} or not u in { the Element of X} ) ;
assume u in X ; :: thesis: P1[z,u]
then ( u = the Element of X or u in X \ { the Element of X} ) by A20, TARSKI:def 1, XBOOLE_0:def 5;
then ( P1[z,u] or P1[y,u] ) by A14, A18;
hence P1[z,u] by A3, A19; :: thesis: verum
end;
end;
hence ex x being object st
( x in X & ( for y being object st y in X holds
P1[x,y] ) ) by A9; :: thesis: verum
end;
A21: for n being Nat holds S1[n] from NAT_1:sch 2(A4, A5);
 card F1() = card F1() ;
hence ex x being object st
( x in F1() & ( for y being object st y in F1() holds
P1[x,y] ) ) by A1, A21; :: thesis: verum