let n be Element of NAT ; :: thesis: ( n >= 1 implies n -Root 1 = 1 )
assume A1: n >= 1 ; :: thesis: n -Root 1 = 1
1 |^ n = 1 by NEWTON:15;
hence n -Root 1 = 1 by A1, Def3; :: thesis: verum