per cases ( n >= len A or n < len A ) ;
suppose n >= len A ; :: thesis: A /^ n is Cantor-normal-form
hence A /^ n is Cantor-normal-form by AFINSQ_2:6; :: thesis: verum
end;
suppose A1: n < len A ; :: thesis: A /^ n is Cantor-normal-form
A2: now :: thesis: for a being Ordinal st a in dom (A /^ n) holds
(A /^ n) . a is Cantor-component
let a be Ordinal; :: thesis: ( a in dom (A /^ n) implies (A /^ n) . a is Cantor-component )
assume a in dom (A /^ n) ; :: thesis: (A /^ n) . a is Cantor-component
then (A /^ n) . a in rng (A /^ n) by FUNCT_1:3;
then (A /^ n) . a in rng A by AFINSQ_2:9, TARSKI:def 3;
then consider b being object such that
A3: ( b in dom A & A . b = (A /^ n) . a ) by FUNCT_1:def 3;
thus (A /^ n) . a is Cantor-component by A3, ORDINAL5:def 11; :: thesis: verum
end;
now :: thesis: for a, b being Ordinal st a in b & b in dom (A /^ n) holds
omega -exponent ((A /^ n) . b) in omega -exponent ((A /^ n) . a)
let a, b be Ordinal; :: thesis: ( a in b & b in dom (A /^ n) implies omega -exponent ((A /^ n) . b) in omega -exponent ((A /^ n) . a) )
assume A4: ( a in b & b in dom (A /^ n) ) ; :: thesis: omega -exponent ((A /^ n) . b) in omega -exponent ((A /^ n) . a)
then A5: a in dom (A /^ n) by ORDINAL1:10;
then reconsider m = a, k = b as Nat by A4;
( (A /^ n) . a = A . (m + n) & (A /^ n) . b = A . (k + n) ) by A4, A5, AFINSQ_2:def 2;
then A6: ( (A /^ n) . a = A . (a +^ n) & (A /^ n) . b = A . (b +^ n) ) by CARD_2:36;
A7: ((dom A) - n) + n = (len (A /^ n)) + n by A1, AFINSQ_2:7
.= (len (A /^ n)) +^ n by CARD_2:36 ;
m in Segm k by A4;
then m + n < k + n by NAT_1:44, XREAL_1:6;
then m + n in Segm (k + n) by NAT_1:44;
then m + n in b +^ n by CARD_2:36;
then A8: a +^ n in b +^ n by CARD_2:36;
k in Segm (dom (A /^ n)) by A4;
then k + n < (dom (A /^ n)) + n by NAT_1:44, XREAL_1:6;
then k + n in Segm ((dom (A /^ n)) + n) by NAT_1:44;
then b +^ n in (dom (A /^ n)) + n by CARD_2:36;
then b +^ n in dom A by A7, CARD_2:36;
hence omega -exponent ((A /^ n) . b) in omega -exponent ((A /^ n) . a) by A6, A8, ORDINAL5:def 11; :: thesis: verum
end;
hence A /^ n is Cantor-normal-form by A2, ORDINAL5:def 11; :: thesis: verum
end;
end;