let phi, psi be Ordinal-Sequence; :: thesis: ( rng phi = rng psi & phi is increasing & psi is increasing implies phi = psi )
assume A1: ( rng phi = rng psi & phi is increasing & psi is increasing ) ; :: thesis: phi = psi
A2: dom phi = dom psi
proof
thus dom phi c= dom psi by A1, Lm3; :: according to XBOOLE_0:def 10 :: thesis: dom psi c= dom phi
let x be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not x in dom psi or x in dom phi )
assume x in dom psi ; :: thesis: x in dom phi
hence x in dom phi by A1, Lm3; :: thesis: verum
end;
for x being object st x in dom phi holds
phi . x = psi . x by A1, Lm3;
hence phi = psi by A2; :: thesis: verum