let f, g be real-valued non-increasing FinSequence; :: thesis: for n being 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 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);
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, Th7;
A7: n + 1 in dom g by A1, A2, A4, FINSEQ_3:25;

A8: now :: thesis: not f . (n + 1) <> g . (n + 1)

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

now :: thesis: ( ( f . (n + 1) > g . (n + 1) & contradiction ) or ( f . (n + 1) < g . (n + 1) & contradiction ) )

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 :: thesis: ( ( m = len f & contradiction ) or ( m <> len f & contradiction ) )

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, Th19; :: 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 :: thesis: ( ( m = len g & contradiction ) or ( m <> len g & contradiction ) )

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, Th19; :: 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, Th7;

now :: thesis: for x being object holds card (Coim ((f | n),x)) = card (Coim ((g | n),x))

let x be object ; :: 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
.= (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 ; :: thesis: verum