A1: m = len X by CARD_1:def 7;
SubFin (X,1) = X | 1 by NAT_1:14, MEASUR13:def 5;
then A2: dom (SubFin (X,1)) = {1} by FINSEQ_1:def 3, FINSEQ_1:2;
(SubFin (X,1)) . 1 = CarProduct (SubFin (X,1)) by MEASUR13:def 3;
then consider id1 being Function of (CarProduct (SubFin (X,1))),(product (SubFin (X,1))) such that
A3: ( id1 is one-to-one & id1 is onto & ( for x being object st x in CarProduct (SubFin (X,1)) holds
id1 . x = <*x*> ) ) by A2, PRVECT_3:2;
defpred S₁[ Nat, set , set ] means ( ex i being non zero Nat ex Fi being Function of (CarProduct (SubFin (X,i))),(product (SubFin (X,i))) st
( i = $1 & Fi = $2 & Fi is bijective ) implies ex i being non zero Nat ex Fi being Function of (CarProduct (SubFin (X,i))),(product (SubFin (X,i))) ex IK being Function of [:(CarProduct (SubFin (X,i))),(ElmFin (X,(i + 1))):],(product (SubFin (X,(i + 1)))) st
( i = $1 & Fi = $2 & IK = $3 & Fi is bijective & IK is bijective & ( for x, y being object st x in CarProduct (SubFin (X,i)) & y in ElmFin (X,(i + 1)) holds
ex s being FinSequence st
( Fi . x = s & IK . (x,y) = s ^ <*y*> ) ) ) );
A4: for n being Nat st 1 <= n & n < m holds
for x being set ex y being set st S₁[n,x,y]

let n be Nat; :: thesis:
assume A5: ( 1 <= n & n < m ) ; :: thesis:
let x be set ; :: thesis:

assume ex k being non zero Nat ex Fk being Function of (CarProduct (SubFin (X,k))),(product (SubFin (X,k))) st
( k = n & Fk = x & Fk is bijective ) ; :: thesis:
then consider k being non zero Nat, Fk being Function of (CarProduct (SubFin (X,k))),(product (SubFin (X,k))) such that
A6: ( k = n & Fk = x & Fk is bijective ) ;
set Xk = SubFin (X,k);
A7: ( Fk is one-to-one & Fk is onto ) by A6;
A8: k + 1 <= m by A5, A6, NAT_1:13;
set Xk1 = SubFin (X,(k + 1));
k <= k + 1 by NAT_1:11;
then A9: SubFin ((SubFin (X,(k + 1))),k) = SubFin (X,k) by A8, MEASUR13:7;
len (SubFin (X,(k + 1))) = k + 1 by CARD_1:def 7;
then k + 1 in Seg (len (SubFin (X,(k + 1)))) by FINSEQ_1:4;
then A11: k + 1 in dom (SubFin (X,(k + 1))) by FINSEQ_1:def 3;
reconsider Y = <*((SubFin (X,(k + 1))) . (k + 1))*> as non empty FinSequence ;
A12: ( len Y = 1 & rng Y = {((SubFin (X,(k + 1))) . (k + 1))} ) by FINSEQ_1:39;
then not {} in rng Y by A11;
then reconsider Y = Y as non-empty non empty FinSequence by RELAT_1:def 9;
A13: dom Y = {1} by A12, FINSEQ_1:2, FINSEQ_1:def 3;
Y . 1 = ElmFin ((SubFin (X,(k + 1))),(k + 1)) by MEASUR13:def 1;
then Y . 1 = ElmFin (X,(k + 1)) by A8, MEASUR13:8;
then consider J being Function of (ElmFin (X,(k + 1))),(product Y) such that
A14: ( J is one-to-one & J is onto & ( for x being object st x in ElmFin (X,(k + 1)) holds
J . x = <*x*> ) ) by A13, PRVECT_3:2;
SubFin (X,k) = (SubFin (X,(k + 1))) | k by A9, NAT_1:11, MEASUR13:def 5;
then A15: SubFin (X,(k + 1)) = (SubFin (X,k)) ^ <*((SubFin (X,(k + 1))) . (k + 1))*> by CARD_1:def 7, FINSEQ_3:55;
consider I being Function of [:(product (SubFin (X,k))),(product Y):],(product ((SubFin (X,k)) ^ Y)) such that
A16: ( I is one-to-one & I is onto & ( for x, y being FinSequence st x in product (SubFin (X,k)) & y in product Y holds
I . (x,y) = x ^ y ) ) by PRVECT_3:6;
reconsider I = I as Function of [:(product (SubFin (X,k))),(product Y):],(product (SubFin (X,(k + 1)))) by A15;
deffunc H₁( object , object ) -> object = [(Fk . $1),(J . $2)];
A17: for x, y being object st x in CarProduct (SubFin (X,k)) & y in ElmFin (X,(k + 1)) holds
H₁(x,y) in [:(product (SubFin (X,k))),(product Y):]

proof

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

end;

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

proof

let z1, z2 be object ; :: thesis:
assume A20: ( z1 in dom K & z2 in dom K & K . z1 = K . z2 ) ; :: thesis:
then consider x1, y1 being object such that
A21: ( x1 in CarProduct (SubFin (X,k)) & y1 in ElmFin (X,(k + 1)) & z1 = [x1,y1] ) by ZFMISC_1:def 2;
consider x2, y2 being object such that
A22: ( x2 in CarProduct (SubFin (X,k)) & y2 in ElmFin (X,(k + 1)) & z2 = [x2,y2] ) by A20, ZFMISC_1:def 2;
[(Fk . x1),(J . y1)] = K . (x1,y1) by A18, A21;
then [(Fk . x1),(J . y1)] = K . (x2,y2) by A20, A21, A22;
then [(Fk . x1),(J . y1)] = [(Fk . x2),(J . y2)] by A18, A22;
then A23: ( Fk . x1 = Fk . x2 & J . y1 = J . y2 ) by XTUPLE_0:1;
( x1 in dom Fk & x2 in dom Fk ) by A21, A22, FUNCT_2:def 1;
then A24: x1 = x2 by A7, A23;
( y1 in dom J & y2 in dom J ) by A21, A22, FUNCT_2:def 1;
hence z1 = z2 by A14, A23, A24, A21, A22; :: thesis:

end;

then A25: K is one-to-one ;

now :: thesis:

let z be object ; :: thesis:
assume z in [:(product (SubFin (X,k))),(product Y):] ; :: thesis:
then consider x, y being object such that
A26: ( x in product (SubFin (X,k)) & y in product Y & z = [x,y] ) by ZFMISC_1:def 2;
x in rng Fk by A6, A26, FUNCT_2:def 3;
then consider s being object such that
A27: ( s in dom Fk & x = Fk . s ) by FUNCT_1:def 3;
y in rng J by A14, A26, FUNCT_2:def 3;
then consider t being object such that
A28: ( t in dom J & y = J . t ) by FUNCT_1:def 3;
( [s,t] in dom K & K . (s,t) = [x,y] ) by A18, A19, A27, A28, ZFMISC_1:87;
hence z in rng K by A26, FUNCT_1:3; :: thesis:

end;

then rng K = [:(product (SubFin (X,k))),(product Y):] ;
then A29: K is onto by FUNCT_2:def 3;
reconsider IK = I * K as Function of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],(product (SubFin (X,(k + 1)))) ;
A30: ( IK is one-to-one & IK is onto ) by A15, A16, A25, A29, FUNCT_2:27;
for x, y being object st x in CarProduct (SubFin (X,k)) & y in ElmFin (X,(k + 1)) holds
ex s being FinSequence st
( Fk . x = s & IK . (x,y) = s ^ <*y*> )

proof

let x, y be object ; :: thesis:
assume A31: ( x in CarProduct (SubFin (X,k)) & y in ElmFin (X,(k + 1)) ) ; :: thesis:
then K . (x,y) = [(Fk . x),(J . y)] by A18;
then A32: IK . (x,y) = I . ((Fk . x),(J . y)) by A19, A31, FUNCT_1:13, ZFMISC_1:87;
A33: dom (SubFin (X,k)) = Seg (len (SubFin (X,k))) by FINSEQ_1:def 3;
A34: Fk . x in product (SubFin (X,k)) by A31, FUNCT_2:5;
then ex g being Function st
( Fk . x = g & dom g = dom (SubFin (X,k)) & ( for y being object st y in dom (SubFin (X,k)) holds
g . y in (SubFin (X,k)) . y ) ) by CARD_3:def 5;
then reconsider s = Fk . x as FinSequence by A33, FINSEQ_1:def 2;
take s ; :: thesis:
A35: J . y = <*y*> by A31, A14;
J . y in product Y by A31, FUNCT_2:5;
hence ( Fk . x = s & IK . (x,y) = s ^ <*y*> ) by A16, A32, A34, A35; :: thesis:

end;

hence ex y being set st S₁[n,x,y] by A30, A6; :: thesis:

end;

hence ex y being set st S₁[n,x,y] ; :: thesis:

end;

consider P being FinSequence such that
A36: ( len P = m & ( P . 1 = id1 or m = 0 ) & ( for n being Nat st 1 <= n & n < m holds
S₁[n,P . n,P . (n + 1)] ) ) from RECDEF_1:sch 3(A4);
reconsider P = P as m -element FinSequence by A36, CARD_1:def 7;
defpred S₂[ Nat] means ( 1 <= $1 & $1 <= m implies ex i being non zero Nat ex Fi being Function of (CarProduct (SubFin (X,i))),(product (SubFin (X,i))) st
( i = $1 & Fi = P . i & Fi is bijective ) );
A37: S₂[ 0 ] ;
A38: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis:
assume A39: S₂[n] ; :: thesis:
assume A40: ( 1 <= n + 1 & n + 1 <= m ) ; :: thesis:
A41: n + 0 < n + 1 by XREAL_1:8;

per cases ;

suppose n = 0 ; :: thesis:

hence ex i being non zero Nat ex Fi being Function of (CarProduct (SubFin (X,i))),(product (SubFin (X,i))) st
( i = n + 1 & Fi = P . i & Fi is bijective ) by A3, A36; :: thesis:

end;

suppose n <> 0 ; :: thesis:

then ( 1 <= n & n < m ) by A41, A40, XXREAL_0:2, NAT_1:14;
then consider k being non zero Nat, Fk being Function of (CarProduct (SubFin (X,k))),(product (SubFin (X,k))), IK being Function of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],(product (SubFin (X,(k + 1)))) such that
A42: ( k = n & Fk = P . n & IK = P . (n + 1) & Fk is bijective & IK is bijective & ( for x, y being object st x in CarProduct (SubFin (X,k)) & y in ElmFin (X,(k + 1)) holds
ex s being FinSequence st
( Fk . x = s & IK . (x,y) = s ^ <*y*> ) ) ) by A36, A39;
set Xk1 = SubFin (X,(k + 1));
set Zk = SubFin ((SubFin (X,(k + 1))),k);
A43: CarProduct (SubFin (X,(k + 1))) = [:(CarProduct (SubFin ((SubFin (X,(k + 1))),k))),(ElmFin ((SubFin (X,(k + 1))),(k + 1))):] by MEASUR13:6;
( k <= k + 1 & k + 1 <= m ) by A42, A40, NAT_1:13;
then A44: SubFin ((SubFin (X,(k + 1))),k) = SubFin (X,k) by MEASUR13:7;
ElmFin (X,(k + 1)) = ElmFin ((SubFin (X,(k + 1))),(k + 1)) by A42, A40, MEASUR13:8;
hence ex k1 being non zero Nat ex Fk1 being Function of (CarProduct (SubFin (X,k1))),(product (SubFin (X,k1))) st
( k1 = n + 1 & Fk1 = P . k1 & Fk1 is bijective ) by A42, A43, A44; :: thesis:

end;

A45: for n being Nat holds S₂[n] from NAT_1:sch 2(A37, A38);
1 <= m by NAT_1:14;
then A46: ex k being non zero Nat ex Fk being Function of (CarProduct (SubFin (X,k))),(product (SubFin (X,k))) st
( k = m & Fk = P . k & Fk is bijective ) by A45;
SubFin (X,m) = X | m by MEASUR13:def 5;
then SubFin (X,m) = X | (dom X) by A1, FINSEQ_1:def 3;
then reconsider y = P . m as Function of (CarProduct X),(product X) by A46;

A47: now :: thesis:

let n be non zero Nat; :: thesis:
assume A48: n < m ; :: thesis:
A49: 1 <= n by NAT_1:14;
then A50: S₁[n,P . n,P . (n + 1)] by A36, A48;
ex k being non zero Nat ex Fk being Function of (CarProduct (SubFin (X,k))),(product (SubFin (X,k))) st
( k = n & Fk = P . k & Fk is bijective ) by A48, A49, A45;
hence ex Fn being Function of (CarProduct (SubFin (X,n))),(product (SubFin (X,n))) ex IK being Function of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],(product (SubFin (X,(n + 1)))) st
( Fn = P . n & IK = P . (n + 1) & Fn is bijective & IK is bijective & ( for x, y being object st x in CarProduct (SubFin (X,n)) & y in ElmFin (X,(n + 1)) holds
ex s being FinSequence st
( Fn . x = s & IK . (x,y) = s ^ <*y*> ) ) ) by A50; :: thesis:

end;

take P ; :: thesis:
thus ex id1 being Function of (CarProduct (SubFin (X,1))),(product (SubFin (X,1))) st
( P . 1 = id1 & id1 is bijective & ( for x being object st x in CarProduct (SubFin (X,1)) holds
id1 . x = <*x*> ) ) by A36, A3; :: thesis:
thus for i being non zero Nat st i < m holds
ex Fi being Function of (CarProduct (SubFin (X,i))),(product (SubFin (X,i))) ex IK being Function of [:(CarProduct (SubFin (X,i))),(ElmFin (X,(i + 1))):],(product (SubFin (X,(i + 1)))) st
( Fi = P . i & IK = P . (i + 1) & Fi is bijective & IK is bijective & ( for x, y being object st x in CarProduct (SubFin (X,i)) & y in ElmFin (X,(i + 1)) holds
ex s being FinSequence st
( Fi . x = s & IK . (x,y) = s ^ <*y*> ) ) ) by A47; :: thesis: