let a, b be Real; ( 0 <= a & 0 <= b implies sqrt (a * b) = (sqrt a) * (sqrt b) )
assume that
A1:
0 <= a
and
A2:
0 <= b
; sqrt (a * b) = (sqrt a) * (sqrt b)
A3:
0 <= sqrt a
by A1, Def2;
A4:
0 <= sqrt b
by A2, Def2;
(sqrt (a * b)) ^2 =
a * b
by A1, A2, Def2
.=
((sqrt a) ^2) * b
by A1, Def2
.=
((sqrt a) ^2) * ((sqrt b) ^2)
by A2, Def2
.=
((sqrt a) * (sqrt b)) ^2
;
hence sqrt (a * b) =
sqrt (((sqrt a) * (sqrt b)) ^2)
by A1, A2, Def2
.=
(sqrt a) * (sqrt b)
by A3, A4, Def2
;
verum