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) . b1 is Cantor-component )
assume a in dom (A ^ B) ; :: thesis: (A ^ B) . b1 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 ex n being Nat st
( n in dom B & a = (len A) + n ) ; :: thesis: (A ^ B) . b1 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 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 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 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