defpred S1[ object ] means ( ex m being non zero Element of NAT st
( m <= n & $1 = PFArt (m,k) ) or $1 = PFCrt (n,k) );
consider X being set such that
A1: for x being object holds
( x in X iff ( x in PFuncs (NAT,{k}) & S1[x] ) ) from XBOOLE_0:sch 1();
 A2: X c= bool [:(Seg ((2 * n) + 1)),{k}:]
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in bool [:(Seg ((2 * n) + 1)),{k}:] )
reconsider xx = x as set by TARSKI:1;
assume A3: x in X ; :: thesis: x in bool [:(Seg ((2 * n) + 1)),{k}:]
per cases ( ex m being non zero Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) by A1, A3;
suppose A4: ex m being non zero Element of NAT st
( m <= n & x = PFArt (m,k) ) ; :: thesis: x in bool [:(Seg ((2 * n) + 1)),{k}:]
A5: 2 * n <= (2 * n) + 1 by NAT_1:11;
consider m being non zero Element of NAT such that
A6: m <= n and
A7: x = PFArt (m,k) by A4;
2 * m <= 2 * n by A6, NAT_1:4;
then A8: 2 * m <= (2 * n) + 1 by A5, XXREAL_0:2;
xx c= [:(Seg ((2 * n) + 1)),{k}:]
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in xx or t in [:(Seg ((2 * n) + 1)),{k}:] )
assume A9: t in xx ; :: thesis: t in [:(Seg ((2 * n) + 1)),{k}:]
per cases ( ex m1 being odd Element of NAT st
( m1 <= 2 * m & [m1,k] = t ) or [(2 * m),k] = t ) by A7, A9, Def2;
suppose ex m1 being odd Element of NAT st
( m1 <= 2 * m & [m1,k] = t ) ; :: thesis: t in [:(Seg ((2 * n) + 1)),{k}:]
then consider m1 being odd Element of NAT such that
A10: m1 <= 2 * m and
A11: [m1,k] = t ;
A12: 1 <= m1 by ABIAN:12;
m1 <= (2 * n) + 1 by A8, A10, XXREAL_0:2;
then m1 in Seg ((2 * n) + 1) by A12, FINSEQ_1:1;
hence t in [:(Seg ((2 * n) + 1)),{k}:] by A11, ZFMISC_1:106; :: thesis: verum
end;
suppose A13: [(2 * m),k] = t ; :: thesis: t in [:(Seg ((2 * n) + 1)),{k}:]
1 <= 2 * m by NAT_1:14;
then 2 * m in Seg ((2 * n) + 1) by A8, FINSEQ_1:1;
hence t in [:(Seg ((2 * n) + 1)),{k}:] by A13, ZFMISC_1:106; :: thesis: verum
end;
end;
end;
hence x in bool [:(Seg ((2 * n) + 1)),{k}:] ; :: thesis: verum
end;
suppose A14: x = PFCrt (n,k) ; :: thesis: x in bool [:(Seg ((2 * n) + 1)),{k}:]
xx c= [:(Seg ((2 * n) + 1)),{k}:]
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in xx or t in [:(Seg ((2 * n) + 1)),{k}:] )
assume t in xx ; :: thesis: t in [:(Seg ((2 * n) + 1)),{k}:]
then consider m being odd Element of NAT such that
A15: m <= (2 * n) + 1 and
A16: [m,k] = t by A14, Def3;
1 <= m by ABIAN:12;
then m in Seg ((2 * n) + 1) by A15, FINSEQ_1:1;
hence t in [:(Seg ((2 * n) + 1)),{k}:] by A16, ZFMISC_1:106; :: thesis: verum
end;
hence x in bool [:(Seg ((2 * n) + 1)),{k}:] ; :: thesis: verum
end;
end;
end;
X c= PFuncs (NAT,{k}) by A1;
then reconsider X = X as Element of Fin (PFuncs (NAT,{k})) by A2, FINSUB_1:def 5;
take X ; :: thesis: for x being object holds
( x in X iff ( ex m being non zero Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) )
let x be object ; :: thesis: ( x in X iff ( ex m being non zero Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) )
thus ( not x in X or ex m being non zero Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) by A1; :: thesis: ( ( ex m being non zero Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) implies x in X )
assume ( ex m being non zero Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) ; :: thesis: x in X
hence x in X by A1; :: thesis: verum