let A, B, C be Ordinal; :: thesis: ( A c= B implies exp (A,C) c= exp (B,C) )
defpred S1[ 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 S1[C] holds
S1[ succ C]
proof
let C be Ordinal; :: thesis: ( S1[C] implies S1[ 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 ( S1[C] implies S1[ 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
S1[D] ) holds
S1[C]
proof
deffunc H1( 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
S1[D] ) implies S1[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: S1[C]
consider f1 being Ordinal-Sequence such that
A8: ( dom f1 = C & ( for D being Ordinal st D in C holds
f1 . D = H1(D) ) ) from ORDINAL2:sch 3();
 deffunc H2( 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 = H2(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 S1[C] by A8, A9, A13, A10, Th6; :: thesis: verum
end;
exp (A,{}) = 1 by ORDINAL2:43;
then A14: S1[ 0 ] by ORDINAL2:43;
for C being Ordinal holds S1[C] from ORDINAL2:sch 1(A14, A2, A4);
 hence exp (A,C) c= exp (B,C) ; :: thesis: verum