take a = 1 *^ (exp omega ,1); :: thesis: a is Cantor-component
take b = 1; :: according to ORDINAL5:def 9 :: thesis: ex n being natural number st
( 0 in n & a = n *^ (exp omega ,b) )
take n = 1; :: thesis: ( 0 in n & a = n *^ (exp omega ,b) )
thus ( 0 in n & a = n *^ (exp omega ,b) ) by NAT_1:45; :: thesis: verum