let f, g be non-decreasing FinSequence of REAL ; :: thesis: for n being Element of NAT st len f = n + 1 & len f = len g & f,g are_fiberwise_equipotent holds
( f . (len f) = g . (len g) & f | n,g | n are_fiberwise_equipotent )
let n be Element of NAT ; :: thesis: ( len f = n + 1 & len f = len g & f,g are_fiberwise_equipotent implies ( f . (len f) = g . (len g) & f | n,g | n are_fiberwise_equipotent ) )
assume A1: ( len f = n + 1 & len f = len g & f,g are_fiberwise_equipotent ) ; :: thesis: ( f . (len f) = g . (len g) & f | n,g | n are_fiberwise_equipotent )
0 + 1 <= n + 1 by NAT_1:13;
then A2: ( n + 1 in dom f & n + 1 in dom g ) by A1, FINSEQ_3:27;
set r = f . (n + 1);
set s = g . (n + 1);

A3: now

assume A4: f . (n + 1) <> g . (n + 1) ; :: thesis: contradiction
A5: rng f = rng g by A1, CLASSES1:83;

now

per cases ( f . (n + 1) < g . (n + 1) or f . (n + 1) > g . (n + 1) ) by A4, XXREAL_0:1;

case A6: f . (n + 1) < g . (n + 1) ; :: thesis: contradiction

g . (n + 1) in rng f by A2, A5, FUNCT_1:def 5;
then consider m being Nat such that
A7: ( m in dom f & f . m = g . (n + 1) ) by FINSEQ_2:11;
A8: ( 1 <= m & m <= len f ) by A7, FINSEQ_3:27;

now

per cases ( m = len f or m <> len f ) ;

case m = len f ; :: thesis: contradiction

hence contradiction by A1, A6, A7; :: thesis: verum

end;

case m <> len f ; :: thesis: contradiction

then m < n + 1 by A1, A8, XXREAL_0:1;
hence contradiction by A2, A6, A7, Th17; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

case A9: f . (n + 1) > g . (n + 1) ; :: thesis: contradiction

f . (n + 1) in rng g by A2, A5, FUNCT_1:def 5;
then consider m being Nat such that
A10: ( m in dom g & g . m = f . (n + 1) ) by FINSEQ_2:11;
A11: ( 1 <= m & m <= len g ) by A10, FINSEQ_3:27;

now

per cases ( m = len g or m <> len g ) ;

case m = len g ; :: thesis: contradiction

hence contradiction by A1, A9, A10; :: thesis: verum

end;

case m <> len g ; :: thesis: contradiction

then m < n + 1 by A1, A11, XXREAL_0:1;
hence contradiction by A2, A9, A10, Th17; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence f . (len f) = g . (len g) by A1; :: thesis: f | n,g | n are_fiberwise_equipotent
A12: ( f = (f | n) ^ <*(f . (n + 1))*> & g = (g | n) ^ <*(f . (n + 1))*> ) by A1, A3, RFINSEQ:20;

now

let x be set ; :: thesis: card (Coim (f | n),x) = card (Coim (g | n),x)
(card ((f | n) " {x})) + (card (<*(f . (n + 1))*> " {x})) = card (Coim f,x) by A12, FINSEQ_3:63
.= card (Coim g,x) by A1, CLASSES1:def 9
.= (card ((g | n) " {x})) + (card (<*(f . (n + 1))*> " {x})) by A12, FINSEQ_3:63 ;
hence card (Coim (f | n),x) = card (Coim (g | n),x) ; :: thesis: verum

end;

hence f | n,g | n are_fiberwise_equipotent by CLASSES1:def 9; :: thesis: verum