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; :: thesis: ( S1[n] implies S1[n + 1] )
assume A3: S1[n] ; :: thesis: S1[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 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 ;
X | n is non-empty then 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;
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))*>)
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 S1[n + 1] ; :: thesis: 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 ; :: thesis: verum