let X be non empty set ; :: thesis: for s1, s2 being sequence of X
for n being Nat st s1,s2 are_fiberwise_equipotent holds
ex m being Nat ex fs2 being Subset of (Shift ((s2 | (Segm m)),1)) st Shift ((s1 | (Segm (n + 1))),1),fs2 are_fiberwise_equipotent
let s1, s2 be sequence of X; :: thesis: for n being Nat st s1,s2 are_fiberwise_equipotent holds
ex m being Nat ex fs2 being Subset of (Shift ((s2 | (Segm m)),1)) st Shift ((s1 | (Segm (n + 1))),1),fs2 are_fiberwise_equipotent
let n be Nat; :: thesis: ( s1,s2 are_fiberwise_equipotent implies ex m being Nat ex fs2 being Subset of (Shift ((s2 | (Segm m)),1)) st Shift ((s1 | (Segm (n + 1))),1),fs2 are_fiberwise_equipotent )
assume A1: s1,s2 are_fiberwise_equipotent ; :: thesis: ex m being Nat ex fs2 being Subset of (Shift ((s2 | (Segm m)),1)) st Shift ((s1 | (Segm (n + 1))),1),fs2 are_fiberwise_equipotent
A4: ( dom s1 = NAT & dom s2 = NAT ) by FUNCT_2:def 1;
then consider P being Permutation of (dom s1) such that
A2: s1 = s2 * P by A1, CLASSES1:80;
deffunc H₁( set ) -> Element of omega = (P . $1) + 1;
defpred S₁[ set ] means $1 is Nat;
{ H₁(i) where i is Nat : ( i <= n & S₁[i] ) } is finite from FINSEQ_1:sch 6();
then reconsider D = { H₁(i) where i is Nat : ( i <= n & S₁[i] ) } as finite set ;

now :: thesis: for x being object st x in D holds
x is natural

let x be object ; :: thesis: ( x in D implies x is natural )
assume x in D ; :: thesis: x is natural
then consider i being Nat such that
A3: ( x = H₁(i) & i <= n & S₁[i] ) ;
thus x is natural by A3; :: thesis: verum

end;

then reconsider D = D as finite natural-membered set by MEMBERED:def 6;
(P . 0) + 1 in { H₁(i) where i is Nat : ( i <= n & S₁[i] ) } ;
then reconsider D = D as non empty finite natural-membered set ;
reconsider m = max D as Nat by TARSKI:1;
take m ; :: thesis: ex fs2 being Subset of (Shift ((s2 | (Segm m)),1)) st Shift ((s1 | (Segm (n + 1))),1),fs2 are_fiberwise_equipotent
set fs2 = { [(j + 1),(s2 . j)] where j is Nat : j + 1 in D } ;

now :: thesis: for z being object st z in { [(j + 1),(s2 . j)] where j is Nat : j + 1 in D } holds
z in Shift ((s2 | (Segm m)),1)

let z be object ; :: thesis: ( z in { [(j + 1),(s2 . j)] where j is Nat : j + 1 in D } implies z in Shift ((s2 | (Segm m)),1) )
assume z in { [(j + 1),(s2 . j)] where j is Nat : j + 1 in D } ; :: thesis: z in Shift ((s2 | (Segm m)),1)
then consider j being Nat such that
A4: ( z = [(j + 1),(s2 . j)] & j + 1 in D ) ;
( 1 <= j + 1 & j + 1 <= m ) by A4, NAT_1:11, XXREAL_2:def 8;
then j + 1 in Seg m by FINSEQ_1:1;
then A6: j + 1 in dom (Shift ((s2 | (Segm m)),1)) by SH1;
then (Shift ((s2 | (Segm m)),1)) . (j + 1) = s2 . j by SH3;
hence z in Shift ((s2 | (Segm m)),1) by A4, A6, FUNCT_1:def 2; :: thesis: verum

end;

then { [(j + 1),(s2 . j)] where j is Nat : j + 1 in D } c= Shift ((s2 | (Segm m)),1) ;
then reconsider fs2 = { [(j + 1),(s2 . j)] where j is Nat : j + 1 in D } as Subset of (Shift ((s2 | (Segm m)),1)) ;
take fs2 ; :: thesis: Shift ((s1 | (Segm (n + 1))),1),fs2 are_fiberwise_equipotent
defpred S₂[ object , object ] means ex i being Nat st
( $1 = i + 1 & $2 = (P . i) + 1 );
P1: for x, y1, y2 being object st x in Seg (n + 1) & S₂[x,y1] & S₂[x,y2] holds
y1 = y2 ;
P2: for x being object st x in Seg (n + 1) holds
ex y being object st S₂[x,y]

proof

let x be object ; :: thesis: ( x in Seg (n + 1) implies ex y being object st S₂[x,y] )
assume A7: x in Seg (n + 1) ; :: thesis: ex y being object st S₂[x,y]
then reconsider x = x as Nat ;
( 1 <= x & x <= n + 1 ) by A7, FINSEQ_1:1;
then reconsider i = x - 1 as Element of NAT by NAT_1:21;
A8: x = i + 1 ;
ex y being object st S₂[x,y]

proof

take y = (P . i) + 1; :: thesis: S₂[x,y]
thus S₂[x,y] by A8; :: thesis: verum

end;

hence ex y being object st S₂[x,y] ; :: thesis: verum

end;

now :: thesis: for x being object st x in dom fs2 holds
x in { (i + 1) where i is Nat : i + 1 in D }

let x be object ; :: thesis: ( x in dom fs2 implies x in { (i + 1) where i is Nat : i + 1 in D } )
assume x in dom fs2 ; :: thesis: x in { (i + 1) where i is Nat : i + 1 in D }
then [x,(fs2 . x)] in fs2 by FUNCT_1:def 2;
then consider j being Nat such that
X2: ( [x,(fs2 . x)] = [(j + 1),(s2 . j)] & j + 1 in D ) ;
( x = j + 1 & fs2 . x = s2 . j ) by X2, XTUPLE_0:1;
hence x in { (i + 1) where i is Nat : i + 1 in D } by X2; :: thesis: verum

end;

then X3: dom fs2 c= { (i + 1) where i is Nat : i + 1 in D } ;

now :: thesis: for x being object st x in { (i + 1) where i is Nat : i + 1 in D } holds
x in dom fs2

let x be object ; :: thesis: ( x in { (i + 1) where i is Nat : i + 1 in D } implies x in dom fs2 )
assume x in { (i + 1) where i is Nat : i + 1 in D } ; :: thesis: x in dom fs2
then consider i being Nat such that
X4: ( x = i + 1 & i + 1 in D ) ;
[x,(s2 . i)] in fs2 by X4;
hence x in dom fs2 by XTUPLE_0:def 12; :: thesis: verum

end;

then { (i + 1) where i is Nat : i + 1 in D } c= dom fs2 ;
then X5: dom fs2 = { (i + 1) where i is Nat : i + 1 in D } by X3, XBOOLE_0:def 10;
consider P2 being Function such that
A9: ( dom P2 = Seg (n + 1) & ( for x being object st x in Seg (n + 1) holds
S₂[x,P2 . x] ) ) from FUNCT_1:sch 2(P1, P2);
A10: dom P2 = dom (Shift ((s1 | (Segm (n + 1))),1)) by A9, SH1;

now :: thesis: for y being object st y in rng P2 holds
y in dom fs2

let y be object ; :: thesis: ( y in rng P2 implies y in dom fs2 )
assume y in rng P2 ; :: thesis: y in dom fs2
then consider x being object such that
B1: ( x in dom P2 & y = P2 . x ) by FUNCT_1:def 3;
consider i being Nat such that
B2: ( x = i + 1 & P2 . x = (P . i) + 1 ) by B1, A9;
B5: i <= n by B2, B1, A9, FINSEQ_1:1, XREAL_1:6;
y in D by B5, B1, B2;
hence y in dom fs2 by X5, B1, B2; :: thesis: verum

end;

then B6: rng P2 c= dom fs2 ;

now :: thesis: for y being object st y in dom fs2 holds
y in rng P2

let y be object ; :: thesis: ( y in dom fs2 implies y in rng P2 )
assume y in dom fs2 ; :: thesis: y in rng P2
then consider i being Nat such that
C1: ( y = i + 1 & i + 1 in D ) by X5;
consider j being Nat such that
C2: ( i + 1 = (P . j) + 1 & j <= n & j is Nat ) by C1;
C3: ( 1 <= j + 1 & j + 1 <= n + 1 ) by C2, NAT_1:11, XREAL_1:6;
then ex k being Nat st
( j + 1 = k + 1 & P2 . (j + 1) = (P . k) + 1 ) by A9, FINSEQ_1:1;
hence y in rng P2 by C1, C2, C3, A9, FUNCT_1:3, FINSEQ_1:1; :: thesis: verum

end;

then dom fs2 c= rng P2 ;
then A11: rng P2 = dom fs2 by B6, XBOOLE_0:def 10;

now :: thesis: for x1, x2 being object st x1 in dom P2 & x2 in dom P2 & P2 . x1 = P2 . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom P2 & x2 in dom P2 & P2 . x1 = P2 . x2 implies x1 = x2 )
assume D1: ( x1 in dom P2 & x2 in dom P2 & P2 . x1 = P2 . x2 ) ; :: thesis: x1 = x2
then consider i1 being Nat such that
D3: ( x1 = i1 + 1 & P2 . x1 = (P . i1) + 1 ) by A9;
consider i2 being Nat such that
D4: ( x2 = i2 + 1 & P2 . x2 = (P . i2) + 1 ) by D1, A9;
dom P = NAT by A4, FUNCT_2:def 1;
then ( i1 in dom P & i2 in dom P ) by ORDINAL1:def 12;
hence x1 = x2 by D1, D3, D4, FUNCT_1:def 4; :: thesis: verum

end;

then A12: P2 is one-to-one by FUNCT_1:def 4;
E0: dom (fs2 * P2) = dom P2 by B6, RELAT_1:27;
then E1: dom (fs2 * P2) = dom (Shift ((s1 | (Segm (n + 1))),1)) by A9, SH1;
for x being object st x in dom (Shift ((s1 | (Segm (n + 1))),1)) holds
(Shift ((s1 | (Segm (n + 1))),1)) . x = (fs2 * P2) . x

proof

let x be object ; :: thesis: ( x in dom (Shift ((s1 | (Segm (n + 1))),1)) implies (Shift ((s1 | (Segm (n + 1))),1)) . x = (fs2 * P2) . x )
assume E4: x in dom (Shift ((s1 | (Segm (n + 1))),1)) ; :: thesis: (Shift ((s1 | (Segm (n + 1))),1)) . x = (fs2 * P2) . x
then E2: x in Seg (n + 1) by SH1;
reconsider i = x as Nat by E4;
( 1 <= i & i <= n + 1 ) by E2, FINSEQ_1:1;
then reconsider j = i - 1 as Element of NAT by NAT_1:21;
i = j + 1 ;
then E11: (Shift ((s1 | (Segm (n + 1))),1)) . x = (s2 * P) . j by A2, E4, SH3;
j in NAT ;
then j in dom P by A4, FUNCT_2:def 1;
then E12: (s2 * P) . j = s2 . (P . j) by FUNCT_1:13;
consider k being Nat such that
E6: ( i = k + 1 & P2 . i = (P . k) + 1 ) by E2, A9;
P2 . x in dom fs2 by A11, E4, E1, E0, FUNCT_1:3;
then [(P2 . x),(fs2 . (P2 . x))] in fs2 by FUNCT_1:def 2;
then consider l being Nat such that
E7: ( [(P2 . x),(fs2 . (P2 . x))] = [(l + 1),(s2 . l)] & l + 1 in D ) ;
( P2 . i = l + 1 & fs2 . (P2 . i) = s2 . l ) by E7, XTUPLE_0:1;
hence (Shift ((s1 | (Segm (n + 1))),1)) . x = (fs2 * P2) . x by E11, E12, E6, E4, E1, FUNCT_1:12; :: thesis: verum

end;

hence Shift ((s1 | (Segm (n + 1))),1),fs2 are_fiberwise_equipotent by A10, A11, A12, E0, FUNCT_1:def 11, CLASSES1:77; :: thesis: verum