let A, B be non empty Cantor-normal-form Ordinal-Sequence; :: thesis: ( omega -exponent (B . 0) in omega -exponent (last A) implies A ^ B is Cantor-normal-form )
assume A1: omega -exponent (B . 0) in omega -exponent (last A) ; :: thesis: A ^ B is Cantor-normal-form

A2: now :: thesis: for a being Ordinal st a in dom (A ^ B) holds
(A ^ B) . a is Cantor-component

let a be Ordinal; :: thesis: ( a in dom (A ^ B) implies (A ^ B) . b₁ is Cantor-component )
assume a in dom (A ^ B) ; :: thesis: (A ^ B) . b₁ is Cantor-component

per cases then ( a in dom A or ex n being Nat st
( n in dom B & a = (len A) + n ) ) by AFINSQ_1:20;

suppose A3: a in dom A ; :: thesis: (A ^ B) . b₁ is Cantor-component

then A . a = (A ^ B) . a by AFINSQ_1:def 3;
hence (A ^ B) . a is Cantor-component by A3, ORDINAL5:def 11; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom B & a = (len A) + n ) ; :: thesis: (A ^ B) . b₁ is Cantor-component

then consider n being Nat such that
A4: ( n in dom B & a = (len A) + n ) ;
B . n = (A ^ B) . a by A4, AFINSQ_1:def 3;
hence (A ^ B) . a is Cantor-component by A4, ORDINAL5:def 11; :: thesis: verum

end;

end;

end;

for a, b being Ordinal st a in b & b in dom (A ^ B) holds
omega -exponent ((A ^ B) . b) in omega -exponent ((A ^ B) . a)

proof

let a, b be Ordinal; :: thesis: ( a in b & b in dom (A ^ B) implies omega -exponent ((A ^ B) . b) in omega -exponent ((A ^ B) . a) )
assume A5: ( a in b & b in dom (A ^ B) ) ; :: thesis: omega -exponent ((A ^ B) . b) in omega -exponent ((A ^ B) . a)

per cases then ( b in dom A or ex n being Nat st
( n in dom B & b = (len A) + n ) ) by AFINSQ_1:20;

suppose A6: b in dom A ; :: thesis: omega -exponent ((A ^ B) . b) in omega -exponent ((A ^ B) . a)

then A7: ( (A ^ B) . b = A . b & a in dom A ) by A5, ORDINAL1:10, AFINSQ_1:def 3;
then (A ^ B) . a = A . a by AFINSQ_1:def 3;
hence omega -exponent ((A ^ B) . b) in omega -exponent ((A ^ B) . a) by A5, A6, A7, ORDINAL5:def 11; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom B & b = (len A) + n ) ; :: thesis: omega -exponent ((A ^ B) . b) in omega -exponent ((A ^ B) . a)

then consider n being Nat such that
A8: ( n in dom B & b = (len A) + n ) ;
a in dom (A ^ B) by A5, ORDINAL1:10;

per cases then ( a in dom A or ex m being Nat st
( m in dom B & a = (len A) + m ) ) by AFINSQ_1:20;

suppose A9: a in dom A ; :: thesis: omega -exponent ((A ^ B) . b) in omega -exponent ((A ^ B) . a)

then omega -exponent (last A) c= omega -exponent (A . a) by Th31;
then A10: omega -exponent (B . 0) in omega -exponent (A . a) by A1;
omega -exponent (B . n) c= omega -exponent (B . 0) by A8, Th32;
then omega -exponent (B . n) in omega -exponent (A . a) by A10, ORDINAL1:12;
then omega -exponent ((A ^ B) . b) in omega -exponent (A . a) by A8, AFINSQ_1:def 3;
hence omega -exponent ((A ^ B) . b) in omega -exponent ((A ^ B) . a) by A9, AFINSQ_1:def 3; :: thesis: verum

end;

suppose ex m being Nat st
( m in dom B & a = (len A) + m ) ; :: thesis: omega -exponent ((A ^ B) . b) in omega -exponent ((A ^ B) . a)

then consider m being Nat such that
A11: ( m in dom B & a = (len A) + m ) ;
m in n

proof

assume not m in n ; :: thesis: contradiction
then (len A) +^ n c= (len A) +^ m by ORDINAL1:16, ORDINAL2:33;
then b c= (len A) +^ m by A8, CARD_2:36;
then b c= a by A11, CARD_2:36;
then a in a by A5;
hence contradiction ; :: thesis: verum

end;

then omega -exponent (B . n) in omega -exponent (B . m) by A8, ORDINAL5:def 11;
then omega -exponent ((A ^ B) . b) in omega -exponent (B . m) by A8, AFINSQ_1:def 3;
hence omega -exponent ((A ^ B) . b) in omega -exponent ((A ^ B) . a) by A11, AFINSQ_1:def 3; :: thesis: verum

end;

end;

end;

end;

end;

hence A ^ B is Cantor-normal-form by A2, ORDINAL5:def 11; :: thesis: verum