defpred S₁[ non zero Nat] means for X being non-empty $1 -element FinSequence ex F being Function of (CarProduct X),(product X) st
( F is one-to-one & F is onto );
A1: S₁[1]

proof

let X be non-empty 1 -element FinSequence; :: thesis: ex F being Function of (CarProduct X),(product X) st
( F is one-to-one & F is onto )
set P = ProdFinSeq X;
A2: ( (ProdFinSeq X) . 1 = X . 1 & ( for i being Nat st 1 <= i & i < 1 holds
(ProdFinSeq X) . (i + 1) = [:((ProdFinSeq X) . i),(X . (i + 1)):] ) & CarProduct X = (ProdFinSeq X) . 1 ) by Def3;
dom X = Seg (len X) by FINSEQ_1:def 3;
then A3: dom X = Seg 1 by CARD_1:def 7;
then 1 in dom X ;
then consider I being Function of (X . 1),(product X) such that
A4: ( I is one-to-one & I is onto & ( for x being object st x in X . 1 holds
I . x = <*x*> ) ) by A3, FINSEQ_1:2, PRVECT_3:2;
reconsider I = I as Function of (CarProduct X),(product X) by A2;
take I ; :: thesis: ( I is one-to-one & I is onto )
thus ( I is one-to-one & I is onto ) by A4; :: thesis: verum

end;

A5: for n being non zero Nat st S₁[n] holds
S₁[n + 1]

proof

let n be non zero Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A6: S₁[n] ; :: thesis: S₁[n + 1]
let X be non-empty n + 1 -element FinSequence; :: thesis: ex F being Function of (CarProduct X),(product X) st
( F is one-to-one & F is onto )
A7: len X = n + 1 by CARD_1:def 7;
A8: CarProduct X = [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):] by Th6;
set X1 = SubFin (X,n);
consider F1 being Function of (CarProduct (SubFin (X,n))),(product (SubFin (X,n))) such that
A9: ( F1 is one-to-one & F1 is onto ) by A6;
n + 1 in Seg (n + 1) by FINSEQ_1:4;
then A10: n + 1 in dom X by A7, FINSEQ_1:def 3;
reconsider Y = <*(X . (n + 1))*> as non empty FinSequence ;
A11: ( len Y = 1 & rng Y = {(X . (n + 1))} ) by FINSEQ_1:39;
then not {} in rng Y by A10;
then reconsider Y = Y as non-empty non empty FinSequence by RELAT_1:def 9;
A12: dom Y = Seg (len Y) by FINSEQ_1:def 3;
Y . 1 = X . (n + 1) ;
then consider J being Function of (X . (n + 1)),(product Y) such that
A13: ( J is one-to-one & J is onto & ( for x being object st x in X . (n + 1) holds
J . x = <*x*> ) ) by A10, A11, A12, FINSEQ_1:2, PRVECT_3:2;
n < n + 1 by NAT_1:13;
then A14: SubFin (X,n) = X | n by Def5;
then A15: (SubFin (X,n)) ^ Y = X by FINSEQ_3:55, A7;
A16: ElmFin (X,(n + 1)) = X . (n + 1) by Def1;
consider I being Function of [:(product (SubFin (X,n))),(product Y):],(product ((SubFin (X,n)) ^ Y)) such that
A17: ( I is one-to-one & I is onto & ( for x, y being FinSequence st x in product (SubFin (X,n)) & y in product Y holds
I . (x,y) = x ^ y ) ) by PRVECT_3:6;
reconsider I = I as Function of [:(product (SubFin (X,n))),(product Y):],(product X) by FINSEQ_3:55, A7, A14;
deffunc H₁( object , object ) -> object = [(F1 . $1),(J . $2)];
A18: for x, y being object st x in CarProduct (SubFin (X,n)) & y in X . (n + 1) holds
H₁(x,y) in [:(product (SubFin (X,n))),(product Y):]

proof

let x, y be object ; :: thesis: ( x in CarProduct (SubFin (X,n)) & y in X . (n + 1) implies H₁(x,y) in [:(product (SubFin (X,n))),(product Y):] )
assume ( x in CarProduct (SubFin (X,n)) & y in X . (n + 1) ) ; :: thesis: H₁(x,y) in [:(product (SubFin (X,n))),(product Y):]
then ( F1 . x in product (SubFin (X,n)) & J . y in product Y ) by FUNCT_2:5;
hence H₁(x,y) in [:(product (SubFin (X,n))),(product Y):] by ZFMISC_1:87; :: thesis: verum

end;

consider K being Function of [:(CarProduct (SubFin (X,n))),(X . (n + 1)):],[:(product (SubFin (X,n))),(product Y):] such that
A19: for x, y being object st x in CarProduct (SubFin (X,n)) & y in X . (n + 1) holds
K . (x,y) = H₁(x,y) from BINOP_1:sch 2(A18);
A20: dom K = [:(CarProduct (SubFin (X,n))),(X . (n + 1)):] by FUNCT_2:def 1;

now :: thesis: for z1, z2 being object st z1 in dom K & z2 in dom K & K . z1 = K . z2 holds
z1 = z2

let z1, z2 be object ; :: thesis: ( z1 in dom K & z2 in dom K & K . z1 = K . z2 implies z1 = z2 )
assume A21: ( z1 in dom K & z2 in dom K & K . z1 = K . z2 ) ; :: thesis: z1 = z2
then consider x1, y1 being object such that
A22: ( x1 in CarProduct (SubFin (X,n)) & y1 in X . (n + 1) & z1 = [x1,y1] ) by ZFMISC_1:def 2;
consider x2, y2 being object such that
A23: ( x2 in CarProduct (SubFin (X,n)) & y2 in X . (n + 1) & z2 = [x2,y2] ) by A21, ZFMISC_1:def 2;
[(F1 . x1),(J . y1)] = K . (x1,y1) by A19, A22;
then [(F1 . x1),(J . y1)] = K . (x2,y2) by A21, A22, A23;
then [(F1 . x1),(J . y1)] = [(F1 . x2),(J . y2)] by A19, A23;
then A24: ( F1 . x1 = F1 . x2 & J . y1 = J . y2 ) by XTUPLE_0:1;
A25: ( x1 in dom F1 & x2 in dom F1 ) by A22, A23, FUNCT_2:def 1;
( y1 in dom J & y2 in dom J ) by A22, A23, FUNCT_2:def 1;
then y1 = y2 by A13, A24;
hence z1 = z2 by A9, A25, A24, A22, A23; :: thesis: verum

end;

then A26: K is one-to-one ;

now :: thesis: for z being object st z in [:(product (SubFin (X,n))),(product Y):] holds
z in rng K

let z be object ; :: thesis: ( z in [:(product (SubFin (X,n))),(product Y):] implies z in rng K )
assume z in [:(product (SubFin (X,n))),(product Y):] ; :: thesis: z in rng K
then consider x, y being object such that
A27: ( x in product (SubFin (X,n)) & y in product Y & z = [x,y] ) by ZFMISC_1:def 2;
A28: ( x in rng F1 & y in rng J ) by A13, A9, A27, FUNCT_2:def 3;
then consider s being object such that
A29: ( s in dom F1 & x = F1 . s ) by FUNCT_1:def 3;
consider t being object such that
A30: ( t in dom J & y = J . t ) by A28, FUNCT_1:def 3;
A31: [s,t] in dom K by A20, A29, A30, ZFMISC_1:87;
K . (s,t) = H₁(s,t) by A19, A29, A30;
hence z in rng K by A27, A29, A30, A31, FUNCT_1:3; :: thesis: verum

end;

then rng K = [:(product (SubFin (X,n))),(product Y):] ;
then A32: K is onto by FUNCT_2:def 3;
reconsider F = I * K as Function of [:(CarProduct (SubFin (X,n))),(X . (n + 1)):],(product X) ;
reconsider F = F as Function of (CarProduct X),(product X) by A8, A16;
take F ; :: thesis: ( F is one-to-one & F is onto )
thus ( F is one-to-one & F is onto ) by A15, A17, A26, A32, FUNCT_2:27; :: thesis: verum

end;

A33: for n being non zero Nat holds S₁[n] from NAT_1:sch 10(A1, A5);
let m be non zero Nat; :: thesis: for X being non-empty m -element FinSequence ex F being Function of (CarProduct X),(product X) st
( F is one-to-one & F is onto )
let X be non-empty m -element FinSequence; :: thesis: ex F being Function of (CarProduct X),(product X) st
( F is one-to-one & F is onto )
thus ex F being Function of (CarProduct X),(product X) st
( F is one-to-one & F is onto ) by A33; :: thesis: verum