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 b1 = b2 )
assume A2: ( x1 in dom A & x2 in dom A & A . x1 = A . x2 ) ; :: thesis: b1 = b2
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: b1 = b2
then A . a2 in A . a1 by A1, A2, ORDINAL5:def 1;
hence x1 = x2 by A2; :: thesis: verum
end;
suppose a1 = a2 ; :: thesis: b1 = b2
hence x1 = x2 ; :: thesis: verum
end;
suppose a2 in a1 ; :: thesis: b1 = b2
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