defpred S₁[ 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: S₁[ 0 ] ;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]

now :: thesis: 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 m

let m be FinSequence of NAT ; :: thesis: 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 m
let X be non-empty non empty FinSequence; :: thesis: ( 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 ) ) ; :: thesis: card (product X) = Product m

now :: thesis: card (product X) = Product m

per cases ( n = 0 or n <> 0 ) ;

suppose A5: n = 0 ; :: thesis: card (product X) = Product m

A6: 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 ; :: thesis: verum

end;

suppose A9: n <> 0 ; :: thesis: card (product X) = Product m

set 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 ;
reconsider X1 = X | n as non-empty non empty FinSequence by A9;

now :: thesis: for i being Element of NAT st i in dom X1 holds
card (X1 . i) = m1 . i

let i be Element of NAT ; :: thesis: ( i in dom X1 implies card (X1 . i) = m1 . i )
assume A15: i in dom X1 ; :: thesis: card (X1 . i) = m1 . i
Seg n c= Seg (n + 1) by NAT_1:11, FINSEQ_1:5;
then i in Seg (len X) by A4, A12, A15;
then A16: i in dom X by FINSEQ_1:def 3;
thus card (X1 . i) = card (X . i) by FUNCT_1:47, A15
.= m . i by A4, A16
.= m1 . i by FUNCT_1:47, A15, A13, A12 ; :: thesis: verum

end;

then A17: card (product X1) = Product m1 by A3, A10, A11;
A18: n < len X by NAT_1:19, A4;
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))*>)

proof

assume {} in rng (X1 ^ <*(X . (len X))*>) ; :: thesis: contradiction
then {} in (rng X1) \/ (rng <*(X . (len X))*>) by FINSEQ_1:31;
then ( {} in rng X1 or {} in rng <*(X . (len X))*> ) by XBOOLE_0:def 3;
then ( not X1 is non-empty or {} in {(X . (len X))} ) by FINSEQ_1:39;
hence contradiction by TARSKI:def 1, A23; :: thesis: verum

end;

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; :: thesis: verum

end;

end;

end;

hence card (product X) = Product m ; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[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 ; :: thesis: verum