let X be non empty set ; :: thesis: for f being finite-support Function of X,NAT holds card (NatMinor f) = multnat $$ (support f),(addnat [:] f,1)
defpred S1[ Element of Fin X] means for f being Function of X,NAT st ( for x being Element of X st not x in $1 holds
f . x = 0 ) holds
card (NatMinor f) = multnat $$ $1,(addnat [:] f,1);
A1:
S1[ {}. X]
A5:
for B being Element of Fin X
for b being Element of X st S1[B] & not b in B holds
S1[B \/ {.b.}]
proof
let B be
Element of
Fin X;
:: thesis: for b being Element of X st S1[B] & not b in B holds
S1[B \/ {.b.}]let b be
Element of
X;
:: thesis: ( S1[B] & not b in B implies S1[B \/ {.b.}] )
assume A6:
(
S1[
B] & not
b in B )
;
:: thesis: S1[B \/ {.b.}]
let f be
Function of
X,
NAT ;
:: thesis: ( ( for x being Element of X st not x in B \/ {.b.} holds
f . x = 0 ) implies card (NatMinor f) = multnat $$ (B \/ {.b.}),(addnat [:] f,1) )
assume A7:
for
x being
Element of
X st not
x in B \/ {b} holds
f . x = 0
;
:: thesis: card (NatMinor f) = multnat $$ (B \/ {.b.}),(addnat [:] f,1)
dom (addnat [:] f,1) = X
by FUNCT_2:def 1;
then A8:
(addnat [:] f,1) . b =
addnat . (f . b),1
by FUNCOP_1:35
.=
(f . b) + 1
by BINOP_2:def 23
;
set g =
f +* b,
0 ;
A9:
dom f = X
by FUNCT_2:def 1;
for
x being
Element of
X st not
x in B holds
(f +* b,0 ) . x = 0
then A13:
card (NatMinor (f +* b,0 )) = multnat $$ B,
(addnat [:] (f +* b,0 ),1)
by A6;
then reconsider ng =
NatMinor (f +* b,0 ) as
functional non
empty finite set ;
set cng =
card ng;
(f +* b,0 ) | B = f | B
by A6, FUNCT_7:94;
then
(addnat [:] (f +* b,0 ),1) | B = (addnat [:] f,1) | B
by FUNCOP_1:36;
then A14:
multnat $$ B,
(addnat [:] (f +* b,0 ),1) = multnat $$ B,
(addnat [:] f,1)
by SETWOP_2:9;
A15:
f . b < (f . b) + 1
by XREAL_1:31;
reconsider fb1 =
(f . b) + 1 as non
empty Element of
NAT ;
[:ng,((f . b) + 1):],
NatMinor f are_equipotent
proof
deffunc H1(
Element of
ng,
Element of
fb1)
-> set = $1
+* b,$2;
A16:
for
p being
Element of
ng for
l being
Element of
fb1 holds
H1(
p,
l)
in NatMinor f
consider r being
Function of
[:ng,fb1:],
(NatMinor f) such that A24:
for
p being
Element of
ng for
l being
Element of
fb1 holds
r . p,
l = H1(
p,
l)
from FUNCT_7:sch 1(A16);
take
r
;
:: according to WELLORD2:def 4 :: thesis: ( r is one-to-one & dom r = [:ng,((f . b) + 1):] & rng r = NatMinor f )
thus
r is
one-to-one
:: thesis: ( dom r = [:ng,((f . b) + 1):] & rng r = NatMinor f )proof
let x1,
x2 be
set ;
:: according to FUNCT_1:def 8 :: thesis: ( not x1 in dom r or not x2 in dom r or not r . x1 = r . x2 or x1 = x2 )
assume A25:
(
x1 in dom r &
x2 in dom r &
r . x1 = r . x2 )
;
:: thesis: x1 = x2
then consider p1,
l1 being
set such that A26:
x1 = [p1,l1]
by RELAT_1:def 1;
A27:
(
p1 in ng &
l1 in fb1 )
by A25, A26, ZFMISC_1:106;
consider p2,
l2 being
set such that A28:
x2 = [p2,l2]
by A25, RELAT_1:def 1;
A29:
(
p2 in ng &
l2 in fb1 )
by A25, A28, ZFMISC_1:106;
reconsider p1 =
p1 as
Element of
NatMinor (f +* b,0 ) by A25, A26, ZFMISC_1:106;
reconsider p2 =
p2 as
Element of
NatMinor (f +* b,0 ) by A25, A28, ZFMISC_1:106;
A30:
p1 +* b,
l1 =
r . p1,
l1
by A24, A27
.=
r . p2,
l2
by A25, A26, A28
.=
p2 +* b,
l2
by A24, A29
;
A31:
dom p1 = X
by FUNCT_2:169;
A32:
dom p2 = X
by FUNCT_2:169;
then reconsider p1' =
p1,
p2' =
p2 as
natural-valued ManySortedSet of
by A31, PARTFUN1:def 4, RELAT_1:def 18;
l1 =
(p1 +* b,l1) . b
by A31, FUNCT_7:33
.=
l2
by A30, A32, FUNCT_7:33
;
hence
x1 = x2
by A26, A28, A33, PBOOLE:3;
:: thesis: verum
end;
thus A39:
dom r = [:ng,((f . b) + 1):]
by FUNCT_2:def 1;
:: thesis: rng r = NatMinor f
thus
rng r c= NatMinor f
;
:: according to XBOOLE_0:def 10 :: thesis: NatMinor f c= rng r
thus
NatMinor f c= rng r
:: thesis: verumproof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in NatMinor f or x in rng r )
assume
x in NatMinor f
;
:: thesis: x in rng r
then reconsider e =
x as
Element of
NatMinor f ;
A40:
dom e = X
by FUNCT_2:169;
then A41:
e is
ManySortedSet of
by PARTFUN1:def 4, RELAT_1:def 18;
dom (e +* b,0 ) = X
by A40, FUNCT_7:32;
then reconsider eb0 =
e +* b,
0 as
natural-valued ManySortedSet of
by PARTFUN1:def 4, RELAT_1:def 18;
then reconsider eb0 =
eb0 as
Element of
NatMinor (f +* b,0 ) by Def17;
e . b <= f . b
by A41, Def17;
then
e . b < fb1
by A15, XXREAL_0:2;
then A45:
e . b in fb1
by NAT_1:45;
then A46:
[eb0,(e . b)] in dom r
by A39, ZFMISC_1:106;
e =
e +* b,
(e . b)
by FUNCT_7:37
.=
eb0 +* b,
(e . b)
by FUNCT_7:36
;
then
e = r . eb0,
(e . b)
by A24, A45;
hence
x in rng r
by A46, FUNCT_1:def 5;
:: thesis: verum
end;
end;
hence card (NatMinor f) =
card [:ng,((f . b) + 1):]
by CARD_1:21
.=
(card ng) * (card ((f . b) + 1))
by CARD_2:65
.=
(card ng) * ((f . b) + 1)
by CARD_1:def 5
.=
multnat . (multnat $$ B,(addnat [:] f,1)),
((f . b) + 1)
by A13, A14, BINOP_2:def 24
.=
multnat $$ (B \/ {.b.}),
(addnat [:] f,1)
by A6, A8, SETWOP_2:4
;
:: thesis: verum
end;
A47:
for B being Element of Fin X holds S1[B]
from SETWISEO:sch 2(A1, A5);
let f be finite-support Function of X,NAT ; :: thesis: card (NatMinor f) = multnat $$ (support f),(addnat [:] f,1)
for x being Element of X st not x in support f holds
f . x = 0
by Def7;
hence
card (NatMinor f) = multnat $$ (support f),(addnat [:] f,1)
by A47; :: thesis: verum