begin
scheme
SSubsetUniq{
F1()
-> 1-sorted ,
P1[
set ] } :
for
A1,
A2 being
Subset of
F1() st ( for
x being
set holds
(
x in A1 iff
P1[
x] ) ) & ( for
x being
set holds
(
x in A2 iff
P1[
x] ) ) holds
A1 = A2
Lm1:
for A, x being set holds [:A,{x}:] is Function
Lm2:
0 = 2 * 0
;
Lm3:
1 = 0 + 1
;
begin
definition
let n,
k be
Element of
NAT ;
existence
ex b1 being Element of PFuncs (NAT,{k}) st
for x being set holds
( x in b1 iff ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) )
uniqueness
for b1, b2 being Element of PFuncs (NAT,{k}) st ( for x being set holds
( x in b1 iff ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) ) ) & ( for x being set holds
( x in b2 iff ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) ) ) holds
b1 = b2
end;
Lm4:
for n being Element of NAT holds (2 * n) + 1 <= (2 * (n + 1)) + 1
Lm5:
for n, n9 being Element of NAT holds not PFCrt ((n + 1),n9) c= PFCrt (n,n9)
Lm6:
for n, k being Element of NAT holds PFCrt (n,k) c= PFCrt ((n + 1),k)
Lm7:
for n, m, k being Element of NAT st n < k holds
PFCrt (n,m) c= PFArt (k,m)
definition
let n,
k be
Element of
NAT ;
existence
ex b1 being Element of Fin (PFuncs (NAT,{k})) st
for x being set holds
( x in b1 iff ( ex m being non empty Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) )
uniqueness
for b1, b2 being Element of Fin (PFuncs (NAT,{k})) st ( for x being set holds
( x in b1 iff ( ex m being non empty Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) ) ) & ( for x being set holds
( x in b2 iff ( ex m being non empty Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) ) ) holds
b1 = b2
end;
Lm8:
for n, k being Element of NAT
for x being set st x in PFBrt (n,k) holds
x is finite
begin
Lm9:
for a being non empty set st a <> {{}} & {} in a holds
ex b being set st
( b in a & b <> {} )
Lm10:
for m being Element of NAT holds not SubstPoset (NAT,{m}) is complete