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

A1: now

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

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

thus 1 -root a = 1 -Root a by A2, Def1
.= a by A2, PREPOWER:30 ; :: thesis: verum

end;

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

A4: 1 = (2 * 0 ) + 1 ;
thus 1 -root a = - (1 -Root (- a)) by A3, A4, Def1
.= - (- a) by A3, PREPOWER:30
.= a ; :: thesis: verum

end;

end;

end;

thus 1 -root a = a by A1; :: thesis: verum