let n be Nat; :: thesis: ( n >= 1 implies n -Root 1 = 1 )
A1: 1 |^ n = 1 ;
assume n >= 1 ; :: thesis: n -Root 1 = 1
hence n -Root 1 = 1 by A1, Def2; :: thesis: verum