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 :: according to XBOOLE_0:def 10 :: thesis: dom psi c= dom phi

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom phi or x in dom psi )
assume x in dom phi ; :: thesis: x in dom psi
hence x in dom psi by A1, Lm3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: 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 set st x in dom phi holds
phi . x = psi . x by A1, Lm3;
hence phi = psi by A2, FUNCT_1:2; :: thesis: verum