for k being Nat st k in dom ((a,b) In_Power n) holds

((a,b) In_Power n) . k in NAT by ORDINAL1:def 12;

hence (a,b) In_Power n is NAT -valued by FINSEQ_2:12; :: thesis: verum

((a,b) In_Power n) . k in NAT by ORDINAL1:def 12;

hence (a,b) In_Power n is NAT -valued by FINSEQ_2:12; :: thesis: verum