let x be object ; :: thesis: for X being non empty set
for S being SigmaField of X
for E being Element of S
for f being PartFunc of X,REAL st f is nonnegative holds
(f . x) to_power (1 / 2) = sqrt (f . x)
let X be non empty set ; :: thesis: for S being SigmaField of X
for E being Element of S
for f being PartFunc of X,REAL st f is nonnegative holds
(f . x) to_power (1 / 2) = sqrt (f . x)
let S be SigmaField of X; :: thesis: for E being Element of S
for f being PartFunc of X,REAL st f is nonnegative holds
(f . x) to_power (1 / 2) = sqrt (f . x)
let E be Element of S; :: thesis: for f being PartFunc of X,REAL st f is nonnegative holds
(f . x) to_power (1 / 2) = sqrt (f . x)
let f be PartFunc of X,REAL; :: thesis: ( f is nonnegative implies (f . x) to_power (1 / 2) = sqrt (f . x) )
assume f is nonnegative ; :: thesis: (f . x) to_power (1 / 2) = sqrt (f . x)
then A1: 0 <= f . x by MESFUNC6:51;
hence (f . x) to_power (1 / 2) = 2 -root (f . x) by POWER:45
.= 2 -Root (f . x) by A1, POWER:def 1
.= sqrt (f . x) by A1, PREPOWER:32 ;
:: thesis: verum