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

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