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 S₁[ 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);
let f be finite-support Function of X,NAT ; :: thesis: card (NatMinor f) = multnat $$ (support f),(addnat [:] f,1)
A1: for x being Element of X st not x in support f holds
f . x = 0 by Def7;
A2: for B being Element of Fin X
for b being Element of X st S₁[B] & not b in B holds
S₁[B \/ {.b.}]

proof

let B be Element of Fin X; :: thesis: for b being Element of X st S₁[B] & not b in B holds
S₁[B \/ {.b.}]
let b be Element of X; :: thesis: ( S₁[B] & not b in B implies S₁[B \/ {.b.}] )
assume that
A3: S₁[B] and
A4: not b in B ; :: thesis: S₁[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 A5: 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)
set g = f +* b,0 ;
(f +* b,0 ) | B = f | B by A4, FUNCT_7:94;
then (addnat [:] (f +* b,0 ),1) | B = (addnat [:] f,1) | B by FUNCOP_1:36;
then A6: multnat $$ B,(addnat [:] (f +* b,0 ),1) = multnat $$ B,(addnat [:] f,1) by SETWOP_2:9;
A7: 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

proof

let x be Element of X; :: thesis: ( not x in B implies (f +* b,0 ) . x = 0 )
assume A8: not x in B ; :: thesis: (f +* b,0 ) . x = 0

per cases ( x = b or x <> b ) ;

suppose x = b ; :: thesis: (f +* b,0 ) . x = 0

hence (f +* b,0 ) . x = 0 by A7, FUNCT_7:33; :: thesis: verum

end;

suppose A9: x <> b ; :: thesis: (f +* b,0 ) . x = 0

A10: now

assume x in B \/ {b} ; :: thesis: contradiction
then ( x in B or x in {b} ) by XBOOLE_0:def 3;
hence contradiction by A8, A9, TARSKI:def 1; :: thesis: verum

end;

thus (f +* b,0 ) . x = f . x by A9, FUNCT_7:34
.= 0 by A5, A10 ; :: thesis: verum

end;

end;

end;

then A11: card (NatMinor (f +* b,0 )) = multnat $$ B,(addnat [:] (f +* b,0 ),1) by A3;
then reconsider ng = NatMinor (f +* b,0 ) as functional non empty finite set ;
reconsider fb1 = (f . b) + 1 as non empty Element of NAT ;
dom (addnat [:] f,1) = X by FUNCT_2:def 1;
then A12: (addnat [:] f,1) . b = addnat . (f . b),1 by FUNCOP_1:35
.= (f . b) + 1 by BINOP_2:def 23 ;
set cng = card ng;
A13: f . b < (f . b) + 1 by XREAL_1:31;
[:ng,((f . b) + 1):], NatMinor f are_equipotent

proof

deffunc H₁( Element of ng, Element of fb1) -> set = $1 +* b,$2;
A14: for p being Element of ng
for l being Element of fb1 holds H₁(p,l) in NatMinor f

proof

let p be Element of ng; :: thesis: for l being Element of fb1 holds H₁(p,l) in NatMinor f
let l be Element of fb1; :: thesis: H₁(p,l) in NatMinor f
reconsider q = p as Element of NatMinor (f +* b,0 ) ;
( fb1 c= NAT & l in fb1 ) ;
then reconsider k = l as Element of NAT ;
p in NatMinor (f +* b,0 ) ;
then A15: dom p = X by FUNCT_2:169;
then dom (p +* b,l) = X by FUNCT_7:32;
then reconsider pbl = q +* b,k as natural-valued ManySortedSet of X by PARTFUN1:def 4, RELAT_1:def 18;
for x being set st x in X holds
pbl . x <= f . x

proof

let x be set ; :: thesis: ( x in X implies pbl . x <= f . x )
assume A16: x in X ; :: thesis: pbl . x <= f . x

per cases ( x = b or x <> b ) ;

suppose A17: x = b ; :: thesis: pbl . x <= f . x

A18: k < fb1 by NAT_1:45;
pbl . x = k by A15, A17, FUNCT_7:33;
hence pbl . x <= f . x by A17, A18, NAT_1:13; :: thesis: verum

end;

suppose A19: x <> b ; :: thesis: pbl . x <= f . x

q is ManySortedSet of X by A15, PARTFUN1:def 4, RELAT_1:def 18;
then A20: q . x <= (f +* b,0 ) . x by A16, Def17;
pbl . x = q . x by A19, FUNCT_7:34;
hence pbl . x <= f . x by A19, A20, FUNCT_7:34; :: thesis: verum

end;

end;

end;

hence H₁(p,l) in NatMinor f by Def17; :: thesis: verum

end;

consider r being Function of [:ng,fb1:],(NatMinor f) such that
A21: for p being Element of ng
for l being Element of fb1 holds r . p,l = H₁(p,l) from FUNCT_7:sch 1(A14);
take r ; :: according to WELLORD2:def 4 :: thesis: ( r is one-to-one & proj1 r = [:ng,((f . b) + 1):] & proj2 r = NatMinor f )
thus r is one-to-one :: thesis: ( proj1 r = [:ng,((f . b) + 1):] & proj2 r = NatMinor f )

proof

let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in proj1 r or not x2 in proj1 r or not r . x1 = r . x2 or x1 = x2 )
assume that
A22: x1 in dom r and
A23: x2 in dom r and
A24: r . x1 = r . x2 ; :: thesis: x1 = x2
consider p2, l2 being set such that
A25: x2 = [p2,l2] by A23, RELAT_1:def 1;
reconsider p2 = p2 as Element of NatMinor (f +* b,0 ) by A23, A25, ZFMISC_1:106;
A26: dom p2 = X by FUNCT_2:169;
A27: l2 in fb1 by A23, A25, ZFMISC_1:106;
consider p1, l1 being set such that
A28: x1 = [p1,l1] by A22, RELAT_1:def 1;
reconsider p1 = p1 as Element of NatMinor (f +* b,0 ) by A22, A28, ZFMISC_1:106;
A29: dom p1 = X by FUNCT_2:169;
then reconsider p19 = p1, p29 = p2 as natural-valued ManySortedSet of X by A26, PARTFUN1:def 4, RELAT_1:def 18;
l1 in fb1 by A22, A28, ZFMISC_1:106;
then A30: p1 +* b,l1 = r . p1,l1 by A21
.= r . p2,l2 by A24, A28, A25
.= p2 +* b,l2 by A21, A27 ;

A31: now

let x be set ; :: thesis: ( x in X implies p19 . b₁ = p29 . b₁ )
assume x in X ; :: thesis: p19 . b₁ = p29 . b₁

per cases ( x = b or x <> b ) ;

suppose A32: x = b ; :: thesis: p19 . b₁ = p29 . b₁

A33: (f +* b,0 ) . b = 0 by A7, FUNCT_7:33;
hence p19 . x = 0 by A32, Def17
.= p29 . x by A32, A33, Def17 ;
:: thesis: verum

end;

suppose A34: x <> b ; :: thesis: p19 . b₁ = p29 . b₁

hence p19 . x = (p1 +* b,l1) . x by FUNCT_7:34
.= p29 . x by A30, A34, FUNCT_7:34 ;
:: thesis: verum

end;

end;

end;

l1 = (p1 +* b,l1) . b by A29, FUNCT_7:33
.= l2 by A30, A26, FUNCT_7:33 ;
hence x1 = x2 by A28, A25, A31, PBOOLE:3; :: thesis: verum

end;

thus A35: dom r = [:ng,((f . b) + 1):] by FUNCT_2:def 1; :: thesis: proj2 r = NatMinor f
thus rng r c= NatMinor f ; :: according to XBOOLE_0:def 10 :: thesis: NatMinor f c= proj2 r
thus NatMinor f c= rng r :: thesis: verum

proof

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 ;
A36: dom e = X by FUNCT_2:169;
then dom (e +* b,0 ) = X by FUNCT_7:32;
then reconsider eb0 = e +* b,0 as natural-valued ManySortedSet of X by PARTFUN1:def 4, RELAT_1:def 18;
A37: e is ManySortedSet of X by A36, PARTFUN1:def 4, RELAT_1:def 18;

now

let x be set ; :: thesis: ( x in X implies eb0 . b₁ <= (f +* b,0 ) . b₁ )
assume A38: x in X ; :: thesis: eb0 . b₁ <= (f +* b,0 ) . b₁

per cases ( x = b or x <> b ) ;

suppose x = b ; :: thesis: eb0 . b₁ <= (f +* b,0 ) . b₁

hence eb0 . x <= (f +* b,0 ) . x by A36, FUNCT_7:33; :: thesis: verum

end;

suppose A39: x <> b ; :: thesis: eb0 . b₁ <= (f +* b,0 ) . b₁

then A40: eb0 . x = e . x by FUNCT_7:34;
e . x <= f . x by A37, A38, Def17;
hence eb0 . x <= (f +* b,0 ) . x by A39, A40, FUNCT_7:34; :: thesis: verum

end;

end;

end;

then reconsider eb0 = eb0 as Element of NatMinor (f +* b,0 ) by Def17;
e . b <= f . b by A37, Def17;
then e . b < fb1 by A13, XXREAL_0:2;
then A41: e . b in fb1 by NAT_1:45;
then A42: [eb0,(e . b)] in dom r by A35, 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 A21, A41;
hence x in rng r by A42, 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 A11, A6, BINOP_2:def 24
.= multnat $$ (B \/ {.b.}),(addnat [:] f,1) by A4, A12, SETWOP_2:4 ;
:: thesis: verum

end;

A43: S₁[ {}. X]

proof

let f be Function of X,NAT ; :: thesis: ( ( for x being Element of X st not x in {}. X holds
f . x = 0 ) implies card (NatMinor f) = multnat $$ ({}. X),(addnat [:] f,1) )
assume A44: for x being Element of X st not x in {}. X holds
f . x = 0 ; :: thesis: card (NatMinor f) = multnat $$ ({}. X),(addnat [:] f,1)

now

let x be set ; :: thesis: ( ( x in NatMinor f implies x = f ) & ( x = f implies x in NatMinor f ) )

hereby :: thesis: ( x = f implies x in NatMinor f )

assume A45: x in NatMinor f ; :: thesis: x = f
then reconsider x9 = x as Function of X,NAT by FUNCT_2:121;

now

let c be Element of X; :: thesis: x9 . c = f . c
f . c = 0 by A44;
hence x9 . c = f . c by A45, Def17; :: thesis: verum

end;

hence x = f by FUNCT_2:113; :: thesis: verum
reconsider x99 = x9 as natural-valued ManySortedSet of X ;

end;

thus ( x = f implies x in NatMinor f ) by Th65; :: thesis: verum

end;

then NatMinor f = {f} by TARSKI:def 1;
hence card (NatMinor f) = 1 by CARD_1:50
.= multnat $$ ({}. X),(addnat [:] f,1) by BINOP_2:10, SETWISEO:40 ;
:: thesis: verum

end;

for B being Element of Fin X holds S₁[B] from SETWISEO:sch 2(A43, A2);
hence card (NatMinor f) = multnat $$ (support f),(addnat [:] f,1) by A1; :: thesis: verum