let a be real number ; :: thesis: for n, m being Element of NAT st ( ( a >= 0 & n >= 1 & m >= 1 ) or ex m1, m2 being Element of NAT st
( n = (2 * m1) + 1 & m = (2 * m2) + 1 ) ) holds
n -root (m -root a) = (n * m) -root a
let n, m be Element of NAT ; :: thesis: ( ( ( a >= 0 & n >= 1 & m >= 1 ) or ex m1, m2 being Element of NAT st
( n = (2 * m1) + 1 & m = (2 * m2) + 1 ) ) implies n -root (m -root a) = (n * m) -root a )
assume A1: ( ( a >= 0 & n >= 1 & m >= 1 ) or ex m1, m2 being Element of NAT st
( n = (2 * m1) + 1 & m = (2 * m2) + 1 ) ) ; :: thesis: n -root (m -root a) = (n * m) -root a

A2: now

let a be real number ; :: thesis: for n, m being Element of NAT st a >= 0 & n >= 1 & m >= 1 holds
n -root (m -root a) = (n * m) -root a
let n, m be Element of NAT ; :: thesis: ( a >= 0 & n >= 1 & m >= 1 implies n -root (m -root a) = (n * m) -root a )
assume A3: ( a >= 0 & n >= 1 & m >= 1 ) ; :: thesis: n -root (m -root a) = (n * m) -root a
then A4: n * m >= 1 by XREAL_1:161;
m -root a >= 0 by A3, Th8;
then A5: m -Root a >= 0 by A3, Def1;
thus n -root (m -root a) = n -root (m -Root a) by A3, Def1
.= n -Root (m -Root a) by A3, A5, Def1
.= (n * m) -Root a by A3, PREPOWER:34
.= (n * m) -root a by A3, A4, Def1 ; :: thesis: verum

end;

now

given m1, m2 being Element of NAT such that A6: ( n = (2 * m1) + 1 & m = (2 * m2) + 1 ) ; :: thesis: n -root (m -root a) = (n * m) -root a
A7: n >= 0 + 1 by A6, XREAL_1:8;
A8: m >= 0 + 1 by A6, XREAL_1:8;
then A9: n * m >= 1 by A7, XREAL_1:161;
A10: n * m = (2 * (((m1 * (2 * m2)) + m1) + m2)) + 1 by A6;

now

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

suppose a >= 0 ; :: thesis: n -root (m -root a) = (n * m) -root a

hence n -root (m -root a) = (n * m) -root a by A2, A7, A8; :: thesis: verum

end;

suppose A11: a < 0 ; :: thesis: n -root (m -root a) = (n * m) -root a

then A12: - a >= 0 ;
then m -root (- a) >= 0 by A8, Th8;
then A13: m -Root (- a) >= 0 by A8, A12, Def1;
thus n -root (m -root a) = n -root (- (m -Root (- a))) by A6, A11, Def1
.= - (n -root (- (- (m -Root (- a))))) by A6, Th11
.= - (n -Root (m -Root (- a))) by A7, A13, Def1
.= - ((n * m) -Root (- a)) by A7, A8, A12, PREPOWER:34
.= - ((n * m) -root (- a)) by A9, A12, Def1
.= (n * m) -root a by A10, Th11 ; :: thesis: verum

end;

end;

end;

hence n -root (m -root a) = (n * m) -root a ; :: thesis: verum

end;

hence n -root (m -root a) = (n * m) -root a by A1, A2; :: thesis: verum