let A, B be Ordinal-Sequence; :: thesis: ( A ^ B is Cantor-normal-form implies rng (omega -exponent A) misses rng (omega -exponent B) )
assume A1: A ^ B is Cantor-normal-form ; :: thesis: rng (omega -exponent A) misses rng (omega -exponent B)
(rng (omega -exponent A)) /\ (rng (omega -exponent B)) = {}

proof

assume (rng (omega -exponent A)) /\ (rng (omega -exponent B)) <> {} ; :: thesis: contradiction
then consider y being object such that
A2: y in (rng (omega -exponent A)) /\ (rng (omega -exponent B)) by XBOOLE_0:def 1;
A3: ( y in rng (omega -exponent A) & y in rng (omega -exponent B) ) by A2, XBOOLE_0:def 4;
then consider x1 being object such that
A4: ( x1 in dom (omega -exponent A) & (omega -exponent A) . x1 = y ) by FUNCT_1:def 3;
consider x2 being object such that
A5: ( x2 in dom (omega -exponent B) & (omega -exponent B) . x2 = y ) by A3, FUNCT_1:def 3;
reconsider x1 = x1, x2 = x2 as Ordinal by A4, A5;
A6: x1 in dom A by A4, Def1;
then A7: A . x1 = (A ^ B) . x1 by ORDINAL4:def 1;
A8: x2 in dom B by A5, Def1;
then A9: B . x2 = (A ^ B) . ((dom A) +^ x2) by ORDINAL4:def 1;
dom A c= (dom A) +^ x2 by ORDINAL3:24;
then A10: x1 in (dom A) +^ x2 by A6;
(dom A) +^ x2 in (dom A) +^ (dom B) by A8, ORDINAL2:32;
then (dom A) +^ x2 in dom (A ^ B) by ORDINAL4:def 1;
then omega -exponent ((A ^ B) . ((dom A) +^ x2)) in omega -exponent ((A ^ B) . x1) by A1, A10, ORDINAL5:def 11;
then (omega -exponent B) . x2 in omega -exponent (A . x1) by A7, A8, A9, Def1;
then (omega -exponent B) . x2 in (omega -exponent A) . x1 by A6, Def1;
hence contradiction by A4, A5; :: thesis: verum

end;

hence rng (omega -exponent A) misses rng (omega -exponent B) by XBOOLE_0:def 7; :: thesis: verum