let A be Ordinal-Sequence; :: thesis: ( A is decreasing implies A is one-to-one )
assume A1: A is decreasing ; :: thesis: A is one-to-one

now :: thesis: for x1, x2 being object st x1 in dom A & x2 in dom A & A . x1 = A . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom A & x2 in dom A & A . x1 = A . x2 implies b₁ = b₂ )
assume A2: ( x1 in dom A & x2 in dom A & A . x1 = A . x2 ) ; :: thesis: b₁ = b₂
then reconsider a1 = x1, a2 = x2 as Ordinal ;

per cases ( a1 in a2 or a1 = a2 or a2 in a1 ) by ORDINAL1:14;

suppose a1 in a2 ; :: thesis: b₁ = b₂

then A . a2 in A . a1 by A1, A2, ORDINAL5:def 1;
hence x1 = x2 by A2; :: thesis: verum

end;

suppose a1 = a2 ; :: thesis: b₁ = b₂

hence x1 = x2 ; :: thesis: verum

end;

suppose a2 in a1 ; :: thesis: b₁ = b₂

then A . a1 in A . a2 by A1, A2, ORDINAL5:def 1;
hence x1 = x2 by A2; :: thesis: verum

end;

end;

end;

hence A is one-to-one by FUNCT_1:def 4; :: thesis: verum