let R1, R2 be FinSequence of NAT ; ( R1,R2 are_fiberwise_equipotent implies Product R1 = Product R2 )
defpred S1[ Nat] means for f, g being FinSequence of NAT st f,g are_fiberwise_equipotent & len f = $1 holds
Product f = Product g;
A1:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A2:
S1[
n]
;
S1[n + 1]
let f,
g be
FinSequence of
NAT ;
( f,g are_fiberwise_equipotent & len f = n + 1 implies Product f = Product g )
assume that A3:
f,
g are_fiberwise_equipotent
and A4:
len f = n + 1
;
Product f = Product g
reconsider a =
f . (n + 1) as
Element of
NAT ;
A5:
rng f = rng g
by A3, CLASSES1:83;
set fn =
f | n;
A6:
f = (f | n) ^ <*a*>
by A4, RFINSEQ:20;
0 + 1
<= n + 1
by NAT_1:13;
then
n + 1
in dom f
by A4, FINSEQ_3:27;
then
a in rng g
by A5, FUNCT_1:def 5;
then consider m being
Nat such that A7:
m in dom g
and A8:
g . m = a
by FINSEQ_2:11;
reconsider m =
m as
Element of
NAT by ORDINAL1:def 13;
set gg =
g /^ m;
set gm =
g | m;
m <= len g
by A7, FINSEQ_3:27;
then A9:
len (g | m) = m
by FINSEQ_1:80;
A10:
1
<= m
by A7, FINSEQ_3:27;
then
max 0 ,
(m - 1) = m - 1
by FINSEQ_2:4;
then reconsider m1 =
m - 1 as
Element of
NAT by FINSEQ_2:5;
A11:
m = m1 + 1
;
then
m1 <= m
by NAT_1:11;
then A12:
Seg m1 c= Seg m
by FINSEQ_1:7;
m in Seg m
by A10, FINSEQ_1:3;
then
(g | m) . m = a
by A7, A8, RFINSEQ:19;
then A13:
g | m = ((g | m) | m1) ^ <*a*>
by A9, A11, RFINSEQ:20;
A14:
g = (g | m) ^ (g /^ m)
by RFINSEQ:21;
A15:
(g | m) | m1 =
(g | m) | (Seg m1)
by FINSEQ_1:def 15
.=
(g | (Seg m)) | (Seg m1)
by FINSEQ_1:def 15
.=
g | ((Seg m) /\ (Seg m1))
by RELAT_1:100
.=
g | (Seg m1)
by A12, XBOOLE_1:28
.=
g | m1
by FINSEQ_1:def 15
;
now let x be
set ;
card (Coim (f | n),x) = card (Coim ((g | m1) ^ (g /^ m)),x)
card (Coim f,x) = card (Coim g,x)
by A3, CLASSES1:def 9;
then (card ((f | n) " {x})) + (card (<*a*> " {x})) =
card ((((g | m1) ^ <*a*>) ^ (g /^ m)) " {x})
by A14, A13, A15, A6, FINSEQ_3:63
.=
(card (((g | m1) ^ <*a*>) " {x})) + (card ((g /^ m) " {x}))
by FINSEQ_3:63
.=
((card ((g | m1) " {x})) + (card (<*a*> " {x}))) + (card ((g /^ m) " {x}))
by FINSEQ_3:63
.=
((card ((g | m1) " {x})) + (card ((g /^ m) " {x}))) + (card (<*a*> " {x}))
.=
(card (((g | m1) ^ (g /^ m)) " {x})) + (card (<*a*> " {x}))
by FINSEQ_3:63
;
hence
card (Coim (f | n),x) = card (Coim ((g | m1) ^ (g /^ m)),x)
;
verum end;
then A16:
f | n,
(g | m1) ^ (g /^ m) are_fiberwise_equipotent
by CLASSES1:def 9;
len (f | n) = n
by A4, FINSEQ_1:80, NAT_1:11;
then
Product (f | n) = Product ((g | m1) ^ (g /^ m))
by A2, A16;
hence Product f =
(Product ((g | m1) ^ (g /^ m))) * (Product <*a*>)
by A6, RVSUM_1:127
.=
((Product (g | m1)) * (Product (g /^ m))) * (Product <*a*>)
by RVSUM_1:127
.=
((Product (g | m1)) * (Product <*a*>)) * (Product (g /^ m))
.=
(Product (g | m)) * (Product (g /^ m))
by A13, A15, RVSUM_1:127
.=
Product g
by A14, RVSUM_1:127
;
verum
end;
assume A17:
R1,R2 are_fiberwise_equipotent
; Product R1 = Product R2
A18:
len R1 = len R1
;
A19:
S1[ 0 ]
for n being Nat holds S1[n]
from NAT_1:sch 2(A19, A1);
hence
Product R1 = Product R2
by A17, A18; verum