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

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

hence
h = g
by FUNCT_2:63; :: thesis: verumlet 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;thus h . v = sqrt (signnorm (f,v)) by A3

.= g . v by A4 ; :: thesis: verum