let a be real number ; :: thesis: ( a >= 0 implies 1 -Root a = a )
assume A1: a >= 0 ; :: thesis: 1 -Root a = a
a |^ 1 = (a GeoSeq ) . (0 + 1) by Def1
.= ((a GeoSeq ) . 0 ) * a by Th4
.= 1 * a by Th4
.= a ;
hence 1 -Root a = a by A1, Th28; :: thesis: verum