let A, B, C be Ordinal; :: thesis: ( A c= B implies exp (A,C) c= exp (B,C) )
defpred S₁[ Ordinal] means exp (A,$1) c= exp (B,$1);
assume A1: A c= B ; :: thesis: exp (A,C) c= exp (B,C)
A2: for C being Ordinal st S₁[C] holds
S₁[ succ C]

proof

let C be Ordinal; :: thesis: ( S₁[C] implies S₁[ succ C] )
A3: exp (B,(succ C)) = B *^ (exp (B,C)) by ORDINAL2:44;
exp (A,(succ C)) = A *^ (exp (A,C)) by ORDINAL2:44;
hence ( S₁[C] implies S₁[ succ C] ) by A1, A3, ORDINAL3:20; :: thesis: verum

end;

A4: for C being Ordinal st C <> 0 & C is limit_ordinal & ( for D being Ordinal st D in C holds
S₁[D] ) holds
S₁[C]

proof

deffunc H₁( Ordinal) -> set = exp (A,$1);
let C be Ordinal; :: thesis: ( C <> 0 & C is limit_ordinal & ( for D being Ordinal st D in C holds
S₁[D] ) implies S₁[C] )
assume that
A5: C <> 0 and
A6: C is limit_ordinal and
A7: for D being Ordinal st D in C holds
exp (A,D) c= exp (B,D) ; :: thesis: S₁[C]
consider f1 being Ordinal-Sequence such that
A8: ( dom f1 = C & ( for D being Ordinal st D in C holds
f1 . D = H₁(D) ) ) from ORDINAL2:sch 3();
deffunc H₂( Ordinal) -> set = exp (B,$1);
consider f2 being Ordinal-Sequence such that
A9: ( dom f2 = C & ( for D being Ordinal st D in C holds
f2 . D = H₂(D) ) ) from ORDINAL2:sch 3();

A10: now :: thesis: for D being Ordinal st D in dom f1 holds
f1 . D c= f2 . D

let D be Ordinal; :: thesis: ( D in dom f1 implies f1 . D c= f2 . D )
assume A11: D in dom f1 ; :: thesis: f1 . D c= f2 . D
then A12: f1 . D = exp (A,D) by A8;
f2 . D = exp (B,D) by A8, A9, A11;
hence f1 . D c= f2 . D by A7, A8, A11, A12; :: thesis: verum

end;

A13: exp (A,C) is_limes_of f1 by A5, A6, A8, Th21;
exp (B,C) is_limes_of f2 by A5, A6, A9, Th21;
hence S₁[C] by A8, A9, A13, A10, Th6; :: thesis: verum

end;

exp (A,{}) = 1 by ORDINAL2:43;
then A14: S₁[ 0 ] by ORDINAL2:43;
for C being Ordinal holds S₁[C] from ORDINAL2:sch 1(A14, A2, A4);
hence exp (A,C) c= exp (B,C) ; :: thesis: verum