defpred S_{1}[ 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_{1}[ 0 ]
;

A2: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[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

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

A2: for n being Nat st S

S

proof

for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A3: S_{1}[n]
; :: thesis: S_{1}[n + 1]

_{1}[n + 1]
; :: thesis: verum

end;assume A3: S

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

hence
Sfor 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

end;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 mend;

hence
card (product X) = Product m
; :: thesis: verumper cases
( n = 0 or n <> 0 )
;

end;

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;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

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

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 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;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

proof

then reconsider X1 = X | n as non-empty non empty FinSequence by A9;
assume
not X | n is non-empty
; :: thesis: contradiction

then A14: {} in rng (X | n) by RELAT_1:def 9;

rng (X | n) c= rng X by RELAT_1:70;

hence contradiction by A14; :: thesis: verum

end;then A14: {} in rng (X | n) by RELAT_1:def 9;

rng (X | n) c= rng X by RELAT_1:70;

hence contradiction by A14; :: thesis: verum

now :: thesis: for i being Element of NAT st i in dom X1 holds

card (X1 . i) = m1 . i

then A17:
card (product X1) = Product m1
by A3, A10, A11;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;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

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

then
product (X1 ^ <*(X . (len X))*>) <> {}
by CARD_3:26;
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 {} 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

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

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