let S1, S2 be Function of [: the carrier of F,(NonZero F):], the carrier of F; ( ( for x being Element of F
for y being Element of NonZero F holds S1 . (x,y) = (omf F) . (x,((revf F) . y)) ) & ( for x being Element of F
for y being Element of NonZero F holds S2 . (x,y) = (omf F) . (x,((revf F) . y)) ) implies S1 = S2 )
assume that
A2:
for x being Element of F
for y being Element of NonZero F holds S1 . (x,y) = (omf F) . (x,((revf F) . y))
and
A3:
for x being Element of F
for y being Element of NonZero F holds S2 . (x,y) = (omf F) . (x,((revf F) . y))
; S1 = S2
hence
S1 = S2
by FUNCT_2:12; verum