let a, b, m, n be Nat; :: thesis: ( m in dom ((((a,b) In_Power n) | n) /^ 1) implies ((((a,b) In_Power n) | n) /^ 1) . m = ((a,b) In_Power n) . (m + 1) )
A1: ( n = 0 implies ((a,b) In_Power n) | n = {} ) ;
( n > 0 implies n in dom ((a,b) In_Power n) ) by Th43;
hence ( m in dom ((((a,b) In_Power n) | n) /^ 1) implies ((((a,b) In_Power n) | n) /^ 1) . m = ((a,b) In_Power n) . (m + 1) ) by A1, Th29; :: thesis: verum