let A, B be Ordinal-Sequence; :: thesis: ( A ^ B is Cantor-normal-form implies ( A is Cantor-normal-form & B is Cantor-normal-form ) )
set AB = A ^ B;
assume that
A1: for a being Ordinal st a in dom (A ^ B) holds
(A ^ B) . a is Cantor-component and
A2: 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) ; :: according to ORDINAL5:def 11 :: thesis: ( A is Cantor-normal-form & B is Cantor-normal-form )
A3: dom (A ^ B) = (dom A) +^ (dom B) by ORDINAL4:def 1;
then A4: dom A c= dom (A ^ B) by ORDINAL3:24;
thus A is Cantor-normal-form :: thesis: B is Cantor-normal-form

proof

hereby :: according to ORDINAL5:def 11 :: thesis: for a, b being Ordinal st a in b & b in dom A holds
omega -exponent (A . b) in omega -exponent (A . a)

let a be Ordinal; :: thesis: ( a in dom A implies A . a is Cantor-component )
assume a in dom A ; :: thesis: A . a is Cantor-component
then ( A . a = (A ^ B) . a & a in dom (A ^ B) ) by A4, ORDINAL4:def 1;
hence A . a is Cantor-component by A1; :: thesis: verum

end;

let a, b be Ordinal; :: thesis: ( a in b & b in dom A implies omega -exponent (A . b) in omega -exponent (A . a) )
assume A5: ( a in b & b in dom A ) ; :: thesis: omega -exponent (A . b) in omega -exponent (A . a)
then a in dom A by ORDINAL1:10;
then ( A . a = (A ^ B) . a & A . b = (A ^ B) . b & b in dom (A ^ B) ) by A4, A5, ORDINAL4:def 1;
hence omega -exponent (A . b) in omega -exponent (A . a) by A2, A5; :: thesis: verum

end;

hereby :: according to ORDINAL5:def 11 :: thesis: for a, b being Ordinal st a in b & b in dom B holds
omega -exponent (B . b) in omega -exponent (B . a)

let a be Ordinal; :: thesis: ( a in dom B implies B . a is Cantor-component )
assume a in dom B ; :: thesis: B . a is Cantor-component
then ( B . a = (A ^ B) . ((dom A) +^ a) & (dom A) +^ a in dom (A ^ B) ) by A3, ORDINAL3:17, ORDINAL4:def 1;
hence B . a is Cantor-component by A1; :: thesis: verum

end;

let a, b be Ordinal; :: thesis: ( a in b & b in dom B implies omega -exponent (B . b) in omega -exponent (B . a) )
assume A6: ( a in b & b in dom B ) ; :: thesis: omega -exponent (B . b) in omega -exponent (B . a)
then a in dom B by ORDINAL1:10;
then ( B . a = (A ^ B) . ((dom A) +^ a) & B . b = (A ^ B) . ((dom A) +^ b) & (dom A) +^ b in dom (A ^ B) & (dom A) +^ a in (dom A) +^ b ) by A3, A6, ORDINAL3:17, ORDINAL4:def 1;
hence omega -exponent (B . b) in omega -exponent (B . a) by A2; :: thesis: verum