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 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 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 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 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 m
now :: thesis: card () = Product m
per cases ( n = 0 or n <> 0 ) ;
suppose A5: n = 0 ; :: thesis: card () = Product m
A6: m = <*(m . 1)*> by ;
A7: X = <*(X . 1)*> by ;
n + 1 in Seg (n + 1) by FINSEQ_1:4;
then A8: 1 in dom X by ;
thus card () = card (X . 1) by Th16, A7, A8
.= m . 1 by A8, A4
.= Product m by ; :: thesis: verum
end;
suppose A9: n <> 0 ; :: thesis: card () = Product m
set X1 = X | n;
reconsider m1 = m | n as FinSequence of NAT ;
A10: len m1 = n by ;
A11: len (X | n) = n by ;
A12: dom (X | n) = Seg (len (X | n)) by FINSEQ_1:def 3
.= Seg n by ;
A13: dom m1 = Seg (len m1) by FINSEQ_1:def 3
.= Seg n by ;
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 ;
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
.= m . i by
.= m1 . i by ; :: thesis: verum
end;
then A17: card (product X1) = Product m1 by A3, A10, A11;
A18: n < len X by ;
A19: X is FinSequence of rng X by FINSEQ_1:def 4;
A20: X = X | (n + 1) by
.= X1 ^ <*(X . (len X))*> by ;
A21: n < len m by ;
A22: m = m | (n + 1) by
.= m1 ^ <*(m . (len m))*> by ;
len X in Seg (len X) by ;
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 ;
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 ;
then A27: card [:(product X1),(X . (len X)):] = card (product (X1 ^ <*(X . (len X))*>)) by ;
A28: card () = card (product <*(product X1),(X . (len X))*>) by ;
A29: ( product X1 is finite set & X . (len X) is finite set ) by ;
card (product <*(product X1),(X . (len X))*>) = card [:(product X1),(X . (len X)):] by
.= (Product m1) * (m . (len m)) by ;
hence card () = Product m by ; :: thesis: verum
end;
end;
end;
hence card () = 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 m ; :: thesis: verum