let h, g be Function; :: thesis: ( dom h = dom f & ( for x being object st x in dom h holds

h . x = sqrt (f . x) ) & dom g = dom f & ( for x being object st x in dom g holds

g . x = sqrt (f . x) ) implies h = g )

assume that

A1: dom h = dom f and

A2: for c being object st c in dom h holds

h . c = sqrt (f . c) and

A3: dom g = dom f and

A4: for c being object st c in dom g holds

g . c = sqrt (f . c) ; :: thesis: h = g

h . x = sqrt (f . x) ) & dom g = dom f & ( for x being object st x in dom g holds

g . x = sqrt (f . x) ) implies h = g )

assume that

A1: dom h = dom f and

A2: for c being object st c in dom h holds

h . c = sqrt (f . c) and

A3: dom g = dom f and

A4: for c being object st c in dom g holds

g . c = sqrt (f . c) ; :: thesis: h = g

now :: thesis: for x being object st x in dom h holds

h . x = g . x

hence
h = g
by A1, A3, FUNCT_1:2; :: thesis: verumh . x = g . x

let x be object ; :: thesis: ( x in dom h implies h . x = g . x )

assume A5: x in dom h ; :: thesis: h . x = g . x

hence h . x = sqrt (f . x) by A2

.= g . x by A1, A3, A4, A5 ;

:: thesis: verum

end;assume A5: x in dom h ; :: thesis: h . x = g . x

hence h . x = sqrt (f . x) by A2

.= g . x by A1, A3, A4, A5 ;

:: thesis: verum