let a be Real; :: thesis: 1 -root a = a

now :: thesis: 1 -root a = a

per cases ( a >= 0 or a < 0 ) ;

suppose A1: a >= 0 ; :: thesis: 1 -root a = a

hence 1 -root a = 1 -Root a by Def1
.= a by A1, PREPOWER:21 ;
:: thesis: verum

end;

suppose A2: a < 0 ; :: thesis: 1 -root a = a

1 = (2 * 0) + 1 ;
hence 1 -root a = - (1 -Root (- a)) by A2, Def1
.= - (- a) by A2, PREPOWER:21
.= a ;
:: thesis: verum

end;

end;

end;

hence 1 -root a = a ; :: thesis: verum