let f, g be non-increasing 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 that
A1: len f = n + 1 and
A2: len f = len g and
A3: f,g are_fiberwise_equipotent ; :: thesis: ( f . (len f) = g . (len g) & f | n,g | n are_fiberwise_equipotent )
set r = f . (n + 1);
set s = g . (n + 1);
0 < n + 1 by NAT_1:3;
then A4: 0 + 1 <= n + 1 by NAT_1:13;
then A5: n + 1 in dom f by A1, FINSEQ_3:25;
A6: f = (f | n) ^ <*(f . (n + 1))*> by A1, Th20;
A7: n + 1 in dom g by A1, A2, A4, FINSEQ_3:25;

A8: now

A9: rng f = rng g by A3, CLASSES1:75;
assume A10: f . (n + 1) <> g . (n + 1) ; :: thesis: contradiction

now

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

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

g . (n + 1) in rng f by A7, A9, FUNCT_1:def 3;
then consider m being Nat such that
A12: m in dom f and
A13: f . m = g . (n + 1) by FINSEQ_2:10;
A14: m <= len f by A12, FINSEQ_3:25;

now

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

case m = len f ; :: thesis: contradiction

hence contradiction by A1, A11, A13; :: thesis: verum

end;

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

then m < n + 1 by A1, A14, XXREAL_0:1;
hence contradiction by A5, A11, A12, A13, Th32; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

f . (n + 1) in rng g by A5, A9, FUNCT_1:def 3;
then consider m being Nat such that
A16: m in dom g and
A17: g . m = f . (n + 1) by FINSEQ_2:10;
A18: m <= len g by A16, FINSEQ_3:25;

now

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

case m = len g ; :: thesis: contradiction

hence contradiction by A1, A2, A15, A17; :: thesis: verum

end;

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

then m < n + 1 by A1, A2, A18, XXREAL_0:1;
hence contradiction by A7, A15, A16, A17, Th32; :: 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, A2; :: thesis: f | n,g | n are_fiberwise_equipotent
A19: g = (g | n) ^ <*(f . (n + 1))*> by A1, A2, A8, Th20;

now

let x be set ; :: thesis: card (Coim ((f | n),x)) = card (Coim ((g | n),x))
(card (Coim ((f | n),x))) + (card (<*(f . (n + 1))*> " {x})) = card (Coim (f,x)) by A6, FINSEQ_3:57
.= card (Coim (g,x)) by A3, CLASSES1:def 9
.= (card (Coim ((g | n),x))) + (card (<*(f . (n + 1))*> " {x})) by A19, FINSEQ_3:57 ;
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