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:61;
exp A,(succ C) = A *^ (exp A,C) by ORDINAL2:61;
hence ( S₁[C] implies S₁[ succ C] ) by A1, A3, ORDINAL3:23; :: thesis: verum

end;

A4: for C being Ordinal st C <> {} & 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 <> {} & C is limit_ordinal & ( for D being Ordinal st D in C holds
S₁[D] ) implies S₁[C] )
assume that
A5: C <> {} 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

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:60;
then A14: S₁[ {} ] by ORDINAL2:60;
for C being Ordinal holds S₁[C] from ORDINAL2:sch 1(A14, A2, A4);
hence exp A,C c= exp B,C ; :: thesis: verum