let h, g be RFunctional of V; :: thesis: ( ( for v being Element of V holds h . v = sqrt (signnorm (f,v)) ) & ( for v being Element of V holds g . v = sqrt (signnorm (f,v)) ) implies h = g )
assume that
A3: for v being Element of V holds h . v = sqrt (signnorm (f,v)) and
A4: for v being Element of V holds g . v = sqrt (signnorm (f,v)) ; :: thesis: h = g

now :: thesis: for v being Element of V holds h . v = g . v

let v be Element of V; :: thesis: h . v = g . v
thus h . v = sqrt (signnorm (f,v)) by A3
.= g . v by A4 ; :: thesis: verum

end;

hence h = g by FUNCT_2:63; :: thesis: verum