let R1, R2 be complex-valued FinSequence; :: thesis: ( R1,R2 are_fiberwise_equipotent implies Product R1 = Product R2 )
( rng R1 c= COMPLEX & rng R2 c= COMPLEX ) by VALUED_0:def 1;
then A0: ( R1 is FinSequence of COMPLEX & R2 is FinSequence of COMPLEX ) by FINSEQ_1:def 4;
defpred S₁[ Nat] means for f, g being FinSequence of COMPLEX st f,g are_fiberwise_equipotent & len f = $1 holds
Product f = Product g;
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
let f, g be FinSequence of COMPLEX ; :: thesis: ( 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 ; :: thesis: Product f = Product g
set a = f . (n + 1);
A5: rng f = rng g by A3, CLASSES1:75;
set fn = f | n;
A6: f = (f | n) ^ <*(f . (n + 1))*> by A4, RFINSEQ:7;
0 + 1 <= n + 1 by NAT_1:13;
then n + 1 in dom f by A4, FINSEQ_3:25;
then f . (n + 1) in rng g by A5, FUNCT_1:def 3;
then consider m being Nat such that
A7: m in dom g and
A8: g . m = f . (n + 1) by FINSEQ_2:10;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
set gg = g /^ m;
set gm = g | m;
m <= len g by A7, FINSEQ_3:25;
then A9: len (g | m) = m by FINSEQ_1:59;
A10: 1 <= m by A7, FINSEQ_3:25;
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:5;
m in Seg m by A10, FINSEQ_1:1;
then (g | m) . m = f . (n + 1) by A7, A8, RFINSEQ:6;
then A13: g | m = ((g | m) | m1) ^ <*(f . (n + 1))*> by A9, A11, RFINSEQ:7;
A14: g = (g | m) ^ (g /^ m) by RFINSEQ:8;
A15: (g | m) | m1 = (g | m) | (Seg m1) by FINSEQ_1:def 16
.= (g | (Seg m)) | (Seg m1) by FINSEQ_1:def 16
.= g | ((Seg m) /\ (Seg m1)) by RELAT_1:71
.= g | (Seg m1) by A12, XBOOLE_1:28
.= g | m1 by FINSEQ_1:def 16 ;

now :: thesis: for x being object holds card (Coim ((f | n),x)) = card (Coim (((g | m1) ^ (g /^ m)),x))

let x be object ; :: thesis: card (Coim ((f | n),x)) = card (Coim (((g | m1) ^ (g /^ m)),x))
card (Coim (f,x)) = card (Coim (g,x)) by A3, CLASSES1:def 10;
then (card ((f | n) " {x})) + (card (<*(f . (n + 1))*> " {x})) = card ((((g | m1) ^ <*(f . (n + 1))*>) ^ (g /^ m)) " {x}) by A14, A13, A15, A6, FINSEQ_3:57
.= (card (((g | m1) ^ <*(f . (n + 1))*>) " {x})) + (card ((g /^ m) " {x})) by FINSEQ_3:57
.= ((card ((g | m1) " {x})) + (card (<*(f . (n + 1))*> " {x}))) + (card ((g /^ m) " {x})) by FINSEQ_3:57
.= ((card ((g | m1) " {x})) + (card ((g /^ m) " {x}))) + (card (<*(f . (n + 1))*> " {x}))
.= (card (((g | m1) ^ (g /^ m)) " {x})) + (card (<*(f . (n + 1))*> " {x})) by FINSEQ_3:57 ;
hence card (Coim ((f | n),x)) = card (Coim (((g | m1) ^ (g /^ m)),x)) ; :: thesis: verum

end;

then A16: f | n,(g | m1) ^ (g /^ m) are_fiberwise_equipotent by CLASSES1:def 10;
len (f | n) = n by A4, FINSEQ_1:59, NAT_1:11;
then Product (f | n) = Product ((g | m1) ^ (g /^ m)) by A2, A16;
hence Product f = (Product ((g | m1) ^ (g /^ m))) * (Product <*(f . (n + 1))*>) by A6, RVSUM_1:97
.= ((Product (g | m1)) * (Product (g /^ m))) * (Product <*(f . (n + 1))*>) by RVSUM_1:97
.= ((Product (g | m1)) * (Product <*(f . (n + 1))*>)) * (Product (g /^ m))
.= (Product (g | m)) * (Product (g /^ m)) by A13, A15, RVSUM_1:97
.= Product g by A14, RVSUM_1:97 ;
:: thesis: verum

end;

assume A17: R1,R2 are_fiberwise_equipotent ; :: thesis: Product R1 = Product R2
A18: len R1 = len R1 ;
A19: S₁[ 0 ]

proof

let f, g be FinSequence of COMPLEX ; :: thesis: ( f,g are_fiberwise_equipotent & len f = 0 implies Product f = Product g )
assume ( f,g are_fiberwise_equipotent & len f = 0 ) ; :: thesis: Product f = Product g
then A20: ( len g = 0 & f = <*> NAT ) by RFINSEQ:3;
then g = <*> NAT ;
hence Product f = Product g by A20; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A19, A1);
hence Product R1 = Product R2 by A0, A17, A18; :: thesis: verum