let phi be Ordinal-Sequence; :: thesis: ( phi is increasing implies phi is one-to-one )
assume A1: for A, B being Ordinal st A in B & B in dom phi holds
phi . A in phi . B ; :: according to ORDINAL2:def 12 :: thesis: phi is one-to-one
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom phi or not y in dom phi or not phi . x = phi . y or x = y )
assume that
A2: ( x in dom phi & y in dom phi ) and
A3: phi . x = phi . y ; :: thesis: x = y
reconsider A = x, B = y as Ordinal by A2;
A4: ( A in B or A = B or B in A ) by ORDINAL1:14;
not phi . A in phi . B by A3;
hence x = y by A1, A2, A3, A4; :: thesis: verum