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

proof

let C be Ordinal; :: thesis: ( S₁[C] implies S₁[ succ C] )
( exp A,(succ C) = A *^ (exp A,C) & exp B,(succ C) = B *^ (exp B,C) ) by ORDINAL2:61;
hence ( S₁[C] implies S₁[ succ C] ) by A1, 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

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 <> {} & C is limit_ordinal ) and
A6: for D being Ordinal st D in C holds
exp A,D c= exp B,D ; :: thesis: S₁[C]
deffunc H₁( Ordinal) -> set = exp A,$1;
consider f1 being Ordinal-Sequence such that
A7: ( 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
A8: ( dom f2 = C & ( for D being Ordinal st D in C holds
f2 . D = H₂(D) ) ) from ORDINAL2:sch 3();
A9: ( exp A,C is_limes_of f1 & exp B,C is_limes_of f2 ) by A5, A7, A8, Th21;

now

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

end;

hence S₁[C] by A7, A8, A9, Th6; :: thesis: verum

end;

for C being Ordinal holds S₁[C] from ORDINAL2:sch 1(A2, A3, A4);
hence exp A,C c= exp B,C ; :: thesis: verum