defpred S1[ Nat] means for m being FinSequence of NAT
for X being non-empty non empty FinSequence st len m = $1 & len m = len X & ( for i being Element of NAT st i in dom X holds
card (X . i) = m . i ) holds
card (product X) = Product m;
A1:
S1[ 0 ]
;
A2:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A3:
S1[
n]
;
S1[n + 1]
now for m being FinSequence of NAT
for X being non-empty non empty FinSequence st len m = n + 1 & len m = len X & ( for i being Element of NAT st i in dom X holds
card (X . i) = m . i ) holds
card (product X) = Product mlet m be
FinSequence of
NAT ;
for X being non-empty non empty FinSequence st len m = n + 1 & len m = len X & ( for i being Element of NAT st i in dom X holds
card (X . i) = m . i ) holds
card (product X) = Product mlet X be
non-empty non
empty FinSequence;
( len m = n + 1 & len m = len X & ( for i being Element of NAT st i in dom X holds
card (X . i) = m . i ) implies card (product X) = Product m )assume A4:
(
len m = n + 1 &
len m = len X & ( for
i being
Element of
NAT st
i in dom X holds
card (X . i) = m . i ) )
;
card (product X) = Product mnow card (product X) = Product mper cases
( n = 0 or n <> 0 )
;
suppose A5:
n = 0
;
card (product X) = Product mA6:
m = <*(m . 1)*>
by A5, FINSEQ_1:40, A4;
A7:
X = <*(X . 1)*>
by A5, FINSEQ_1:40, A4;
n + 1
in Seg (n + 1)
by FINSEQ_1:4;
then A8:
1
in dom X
by A5, FINSEQ_1:def 3, A4;
thus card (product X) =
card (X . 1)
by Th16, A7, A8
.=
m . 1
by A8, A4
.=
Product m
by A6, RVSUM_1:95
;
verum end; suppose A9:
n <> 0
;
card (product X) = Product mset X1 =
X | n;
reconsider m1 =
m | n as
FinSequence of
NAT ;
A10:
len m1 = n
by NAT_1:11, A4, FINSEQ_1:59;
A11:
len (X | n) = n
by NAT_1:11, A4, FINSEQ_1:59;
A12:
dom (X | n) =
Seg (len (X | n))
by FINSEQ_1:def 3
.=
Seg n
by NAT_1:11, A4, FINSEQ_1:59
;
A13:
dom m1 =
Seg (len m1)
by FINSEQ_1:def 3
.=
Seg n
by NAT_1:11, A4, FINSEQ_1:59
;
X | n is
non-empty
then reconsider X1 =
X | n as
non-empty non
empty FinSequence by A9;
then A17:
card (product X1) = Product m1
by A3, A10, A11;
A18:
n < len X
by NAT_1:19, A4;
A19:
X is
FinSequence of
rng X
by FINSEQ_1:def 4;
A20:
X =
X | (n + 1)
by FINSEQ_1:58, A4
.=
X1 ^ <*(X . (len X))*>
by A18, FINSEQ_5:83, A4
;
A21:
n < len m
by NAT_1:19, A4;
A22:
m =
m | (n + 1)
by FINSEQ_1:58, A4
.=
m1 ^ <*(m . (len m))*>
by A21, FINSEQ_5:83, A4
;
len X in Seg (len X)
by A4, FINSEQ_1:4;
then A23:
len X in dom X
by FINSEQ_1:def 3;
then A24:
card (X . (len X)) = m . (len m)
by A4;
consider I being
Function of
[:(product X1),(X . (len X)):],
(product (X1 ^ <*(X . (len X))*>)) such that A25:
(
I is
one-to-one &
I is
onto & ( for
x,
y being
set st
x in product X1 &
y in X . (len X) holds
ex
x1,
y1 being
FinSequence st
(
x = x1 &
<*y*> = y1 &
I . (
x,
y)
= x1 ^ y1 ) ) )
by A23, Th17;
not
{} in rng (X1 ^ <*(X . (len X))*>)
then
product (X1 ^ <*(X . (len X))*>) <> {}
by CARD_3:26;
then A26:
dom I = [:(product X1),(X . (len X)):]
by FUNCT_2:def 1;
rng I = product (X1 ^ <*(X . (len X))*>)
by A25, FUNCT_2:def 3;
then A27:
card [:(product X1),(X . (len X)):] = card (product (X1 ^ <*(X . (len X))*>))
by CARD_1:5, A25, A26, WELLORD2:def 4;
A28:
card (product X) = card (product <*(product X1),(X . (len X))*>)
by CARD_1:5, A20, A27, TOPGEN_5:8;
A29:
(
product X1 is
finite set &
X . (len X) is
finite set )
by A24, A17;
card (product <*(product X1),(X . (len X))*>) =
card [:(product X1),(X . (len X)):]
by CARD_1:5, TOPGEN_5:8
.=
(Product m1) * (m . (len m))
by A24, A17, A29, CARD_2:46
;
hence
card (product X) = Product m
by RVSUM_1:96, A22, A28;
verum end; end; end; hence
card (product X) = Product m
;
verum end;
hence
S1[
n + 1]
;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A2);
hence
for m being FinSequence of NAT
for X being non-empty non empty FinSequence st len m = len X & ( for i being Element of NAT st i in dom X holds
card (X . i) = m . i ) holds
card (product X) = Product m
; verum