let a be real number ; :: thesis: 1 -root a = a

now

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:30 ;
:: thesis: verum

end;

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

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

end;

end;

end;

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