let f, g be non-increasing FinSequence of REAL ; :: 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 ;
A6: f = (f | n) ^ <*(f . (n + 1))*> by ;
A7: n + 1 in dom g by ;
A8: now :: thesis: not f . (n + 1) <> g . (n + 1)
A9: rng f = rng g by ;
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 ;
case A11: f . (n + 1) > g . (n + 1) ; :: thesis: contradiction
g . (n + 1) in rng f by ;
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 ;
now :: thesis: ( ( m = len f & contradiction ) or ( m <> len f & contradiction ) )
per cases ( m = len f or m <> len f ) ;
end;
end;
hence contradiction ; :: thesis: verum
end;
case A15: f . (n + 1) < g . (n + 1) ; :: thesis: contradiction
f . (n + 1) in rng g by ;
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 ;
now :: thesis: ( ( m = len g & contradiction ) or ( m <> len g & contradiction ) )
per cases ( m = len g or m <> len g ) ;
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:
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
.= card (Coim (g,x)) by A3
.= (card (Coim ((g | n),x))) + (card (<*(f . (n + 1))*> " {x})) by ;
hence card (Coim ((f | n),x)) = card (Coim ((g | n),x)) ; :: thesis: verum
end;
hence f | n,g | n are_fiberwise_equipotent ; :: thesis: verum