let a, b, n be Nat; :: thesis: ( n > 0 implies n in dom ((a,b) In_Power n) )
assume n > 0 ; :: thesis: n in dom ((a,b) In_Power n)
then A1: n in Seg n by FINSEQ_1:3;
dom ((a,b) In_Power n) = Seg (len ((a,b) In_Power n)) by FINSEQ_1:def 3
.= Seg (n + 1) by NEWTON:def 4 ;
hence n in dom ((a,b) In_Power n) by A1, FINSEQ_2:8; :: thesis: verum