A1: 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 in dom A & (A | n) . a = A . a ) by RELAT_1:57, FUNCT_1:47;
hence (A | n) . a is Cantor-component by 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 A2: ( a in b & b in dom (A | n) ) ; :: thesis: omega -exponent ((A | n) . b) in omega -exponent ((A | n) . a)
then A3: ( a in dom (A | n) & b in dom A ) by ORDINAL1:10, RELAT_1:57;
then ( (A | n) . a = A . a & (A | n) . b = A . b ) by A2, FUNCT_1:47;
hence omega -exponent ((A | n) . b) in omega -exponent ((A | n) . a) by A2, A3, ORDINAL5:def 11; :: thesis: verum
end;
hence A | n is Cantor-normal-form by A1, ORDINAL5:def 11; :: thesis: verum