let A be decreasing Ordinal-Sequence; :: thesis: for n being Nat st len A = n + 1 holds
rng (A | n) = (rng A) \ {(A . n)}
let n be Nat; :: thesis: ( len A = n + 1 implies rng (A | n) = (rng A) \ {(A . n)} )
assume A1: len A = n + 1 ; :: thesis: rng (A | n) = (rng A) \ {(A . n)}
not A . n in rng (A | n)
proof
assume A . n in rng (A | n) ; :: thesis: contradiction
then consider x being object such that
A2: ( x in dom (A | n) & (A | n) . x = A . n ) by FUNCT_1:def 3;
A3: A . x = A . n by A2, FUNCT_1:47;
A4: ( x in dom A & x in n ) by A2, RELAT_1:57;
n + 0 < n + 1 by XREAL_1:8;
then n in dom A by A1, AFINSQ_1:86;
then n in n by A3, A4, FUNCT_1:def 4;
hence contradiction ; :: thesis: verum
end;
then A5: rng (A | n) c= (rng A) \ {(A . n)} by RELAT_1:70, ZFMISC_1:34;
now :: thesis: for y being object st y in (rng A) \ {(A . n)} holds
y in rng (A | n)
let y be object ; :: thesis: ( y in (rng A) \ {(A . n)} implies y in rng (A | n) )
assume y in (rng A) \ {(A . n)} ; :: thesis: y in rng (A | n)
then A6: ( y in rng A & y <> A . n ) by ZFMISC_1:56;
then consider x being object such that
A7: ( x in dom A & A . x = y ) by FUNCT_1:def 3;
dom A = succ n by A1, Lm5;
then x in n by A6, A7, ORDINAL1:8;
hence y in rng (A | n) by A7, FUNCT_1:50; :: thesis: verum
end;
then (rng A) \ {(A . n)} c= rng (A | n) by TARSKI:def 3;
hence rng (A | n) = (rng A) \ {(A . n)} by A5, XBOOLE_0:def 10; :: thesis: verum