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

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:113; :: thesis: verum