let a be Real; :: 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 Th3
.= 1 * a by Th3
.= a ;
hence 1 -Root a = a by A1, Th19; :: thesis: verum