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)))
reconsider g = f +* (b,0) as Function of X,NAT ;
g | B = f | B by A4, FUNCT_7:92;
then (addnat [:] (g,1)) | B = (addnat [:] (f,1)) | B by FUNCOP_1:28;
then A6: multnat $$ (B,(addnat [:] (g,1))) = multnat $$ (B,(addnat [:] (f,1))) by SETWOP_2:7;
A7: dom f = X by FUNCT_2:def 1;
for x being Element of X st not x in B holds
g . x = 0

proof

let x be Element of X; :: thesis: ( not x in B implies g . x = 0 )
assume A8: not x in B ; :: thesis: g . x = 0

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

suppose x = b ; :: thesis: g . x = 0

hence g . x = 0 by A7, FUNCT_7:31; :: thesis: verum

end;

suppose A9: x <> b ; :: thesis: g . x = 0

A10: now :: thesis: not x in B \/ {b}

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 g . x = f . x by A9, FUNCT_7:32
.= 0 by A5, A10 ; :: thesis: verum

end;

end;

end;

then A11: card (NatMinor g) = multnat $$ (B,(addnat [:] (g,1))) by A3;
then reconsider ng = NatMinor g as functional non empty finite set ;
reconsider fb1 = (f . b) + 1 as non zero Nat ;
dom (addnat [:] (f,1)) = X by FUNCT_2:def 1;
then A12: (addnat [:] (f,1)) . b = addnat . ((f . b),1) by FUNCOP_1:27
.= (f . b) + 1 by BINOP_2:def 23 ;
set cng = card ng;
A13: f . b < (f . b) + 1 by XREAL_1:29;
[: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 g ;
( fb1 c= NAT & l in fb1 ) ;
then reconsider k = l as Element of NAT ;
p in NatMinor g ;
then A15: dom p = X by FUNCT_2:92;
then dom (p +* (b,l)) = X by FUNCT_7:30;
then reconsider pbl = q +* (b,k) as natural-valued ManySortedSet of X by PARTFUN1:def 2, 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

k in Segm fb1 ;
then A18: k < fb1 by NAT_1:44;
pbl . x = k by A15, A17, FUNCT_7:31;
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 2, RELAT_1:def 18;
then A20: q . x <= g . x by A16, Def14;
pbl . x = q . x by A19, FUNCT_7:32;
hence pbl . x <= f . x by A19, A20, FUNCT_7:32; :: thesis: verum

end;

end;

end;

hence H₁(p,l) in NatMinor f by Def14; :: 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 & 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 object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom r or not x2 in dom 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 object such that
A25: x2 = [p2,l2] by A23, RELAT_1:def 1;
reconsider p2 = p2 as Element of NatMinor g by A23, A25, ZFMISC_1:87;
A26: dom p2 = X by FUNCT_2:92;
A27: l2 in fb1 by A23, A25, ZFMISC_1:87;
consider p1, l1 being object such that
A28: x1 = [p1,l1] by A22, RELAT_1:def 1;
reconsider p1 = p1 as Element of NatMinor g by A22, A28, ZFMISC_1:87;
A29: dom p1 = X by FUNCT_2:92;
then reconsider p19 = p1, p29 = p2 as natural-valued ManySortedSet of X by A26, PARTFUN1:def 2, RELAT_1:def 18;
l1 in fb1 by A22, A28, ZFMISC_1:87;
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 :: thesis: for x being object st x in X holds
p19 . x = p29 . x

let x be object ; :: 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: g . b = 0 by A7, FUNCT_7:31;
hence p19 . x = 0 by A32, Def14
.= p29 . x by A32, A33, Def14 ;
:: thesis: verum

end;

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

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

end;

end;

end;

l1 = (p1 +* (b,l1)) . b by A29, FUNCT_7:31
.= l2 by A30, A26, FUNCT_7:31 ;
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: 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: verum

proof

let x be object ; :: 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:92;
then dom (e +* (b,0)) = X by FUNCT_7:30;
then reconsider eb0 = e +* (b,0) as natural-valued ManySortedSet of X by PARTFUN1:def 2, RELAT_1:def 18;
A37: e is ManySortedSet of X by A36, PARTFUN1:def 2, RELAT_1:def 18;

now :: thesis: for x being set st x in X holds
eb0 . x <= g . x

let x be set ; :: thesis: ( x in X implies eb0 . b₁ <= g . b₁ )
assume A38: x in X ; :: thesis: eb0 . b₁ <= g . b₁

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

suppose x = b ; :: thesis: eb0 . b₁ <= g . b₁

hence eb0 . x <= g . x by A36, FUNCT_7:31; :: thesis: verum

end;

suppose A39: x <> b ; :: thesis: eb0 . b₁ <= g . b₁

then A40: eb0 . x = e . x by FUNCT_7:32;
e . x <= f . x by A37, A38, Def14;
hence eb0 . x <= g . x by A39, A40, FUNCT_7:32; :: thesis: verum

end;

end;

end;

then reconsider eb0 = eb0 as Element of NatMinor g by Def14;
e . b <= f . b by A37, Def14;
then e . b < fb1 by A13, XXREAL_0:2;
then A41: e . b in Segm fb1 by NAT_1:44;
then A42: [eb0,(e . b)] in dom r by A35, ZFMISC_1:87;
e = e +* (b,(e . b)) by FUNCT_7:35
.= eb0 +* (b,(e . b)) by FUNCT_7:34 ;
then e = r . (eb0,(e . b)) by A21, A41;
hence x in rng r by A42, FUNCT_1:def 3; :: thesis: verum

end;

end;

hence card (NatMinor f) = card [:ng,((f . b) + 1):] by CARD_1:5
.= (card ng) * (card ((f . b) + 1)) by CARD_2:46
.= (card ng) * ((f . b) + 1)
.= 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:2 ;
:: 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 :: thesis: for x being object holds
( ( x in NatMinor f implies x = f ) & ( x = f implies x in NatMinor f ) )

let x be object ; :: 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:66;

now :: thesis: for c being Element of X holds x9 . c = f . c

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

end;

hence x = f by FUNCT_2:63; :: thesis: verum

end;

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

end;

then NatMinor f = {f} by TARSKI:def 1;
hence card (NatMinor f) = 1 by CARD_1:30
.= multnat $$ (({}. X),(addnat [:] (f,1))) by BINOP_2:10, SETWISEO:31 ;
:: 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