let A, B, C be Ordinal; :: thesis: ( A c= B implies exp (A,C) c= exp (B,C) )

defpred S_{1}[ 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_{1}[C] holds

S_{1}[ succ C]

S_{1}[D] ) holds

S_{1}[C]

then A14: S_{1}[ 0 ]
by ORDINAL2:43;

for C being Ordinal holds S_{1}[C]
from ORDINAL2:sch 1(A14, A2, A4);

hence exp (A,C) c= exp (B,C) ; :: thesis: verum

defpred S

assume A1: A c= B ; :: thesis: exp (A,C) c= exp (B,C)

A2: for C being Ordinal st S

S

proof

A4:
for C being Ordinal st C <> 0 & C is limit_ordinal & ( for D being Ordinal st D in C holds
let C be Ordinal; :: thesis: ( S_{1}[C] implies S_{1}[ 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_{1}[C] implies S_{1}[ succ C] )
by A1, A3, ORDINAL3:20; :: thesis: verum

end;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

S

S

proof

exp (A,{}) = 1
by ORDINAL2:43;
deffunc H_{1}( 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_{1}[D] ) implies S_{1}[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_{1}[C]

consider f1 being Ordinal-Sequence such that

A8: ( dom f1 = C & ( for D being Ordinal st D in C holds

f1 . D = H_{1}(D) ) )
from ORDINAL2:sch 3();

deffunc H_{2}( 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_{2}(D) ) )
from ORDINAL2:sch 3();

exp (B,C) is_limes_of f2 by A5, A6, A9, Th21;

hence S_{1}[C]
by A8, A9, A13, A10, Th6; :: thesis: verum

end;let C be Ordinal; :: thesis: ( C <> 0 & C is limit_ordinal & ( for D being Ordinal st D in C holds

S

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

consider f1 being Ordinal-Sequence such that

A8: ( dom f1 = C & ( for D being Ordinal st D in C holds

f1 . D = H

deffunc H

consider f2 being Ordinal-Sequence such that

A9: ( dom f2 = C & ( for D being Ordinal st D in C holds

f2 . D = H

A10: now :: thesis: for D being Ordinal st D in dom f1 holds

f1 . D c= f2 . D

A13:
exp (A,C) is_limes_of f1
by A5, A6, A8, Th21;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;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

exp (B,C) is_limes_of f2 by A5, A6, A9, Th21;

hence S

then A14: S

for C being Ordinal holds S

hence exp (A,C) c= exp (B,C) ; :: thesis: verum