let phi, psi be Ordinal-Sequence; :: thesis: ( rng phi = rng psi & phi is increasing & psi is increasing implies for A being Ordinal st A in dom phi holds
( A in dom psi & phi . A = psi . A ) )
assume that
A1: rng phi = rng psi and
A2: phi is increasing ; :: thesis: ( not psi is increasing or for A being Ordinal st A in dom phi holds
( A in dom psi & phi . A = psi . A ) )
defpred S₁[ Ordinal] means ( $1 in dom phi implies ( $1 in dom psi & phi . $1 = psi . $1 ) );
assume A3: for A, B being Ordinal st A in B & B in dom psi holds
psi . A in psi . B ; :: according to ORDINAL2:def 12 :: thesis: for A being Ordinal st A in dom phi holds
( A in dom psi & phi . A = psi . A )
A4: for A being Ordinal st ( for B being Ordinal st B in A holds
S₁[B] ) holds
S₁[A]

proof

let A be Ordinal; :: thesis: ( ( for B being Ordinal st B in A holds
S₁[B] ) implies S₁[A] )
assume that
A5: for B being Ordinal st B in A & B in dom phi holds
( B in dom psi & phi . B = psi . B ) and
A6: A in dom phi ; :: thesis: ( A in dom psi & phi . A = psi . A )
phi . A in rng phi by A6, FUNCT_1:def 3;
then consider x being object such that
A7: x in dom psi and
A8: phi . A = psi . x by A1, FUNCT_1:def 3;
reconsider x = x as Ordinal by A7;

A9: now :: thesis: not A in x

assume A10: A in x ; :: thesis: contradiction
then A11: A in dom psi by A7, ORDINAL1:10;
then psi . A in rng psi by FUNCT_1:def 3;
then consider y being object such that
A12: y in dom phi and
A13: psi . A = phi . y by A1, FUNCT_1:def 3;
reconsider y = y as Ordinal by A12;
psi . A in psi . x by A3, A7, A10;
then not A c= y by A2, A8, A12, A13, ORDINAL1:5, ORDINAL4:9;
then A14: y in A by ORDINAL1:16;
then A15: psi . y = phi . y by A5, A12;
psi . y in psi . A by A3, A11, A14;
hence contradiction by A13, A15; :: thesis: verum

end;

now :: thesis: not x in A

assume A16: x in A ; :: thesis: contradiction
then ( phi . x in phi . A & x in dom phi ) by A2, A6, ORDINAL1:10;
then phi . A in phi . A by A5, A8, A16;
hence contradiction ; :: thesis: verum

end;

hence ( A in dom psi & phi . A = psi . A ) by A7, A8, A9, ORDINAL1:14; :: thesis: verum

end;

thus for A being Ordinal holds S₁[A] from ORDINAL1:sch 2(A4); :: thesis: verum