let S1, S2 be Function of [:the carrier of F,(NonZero F):],the carrier of F; :: thesis: ( ( for x being Element of the carrier of F
for y being Element of NonZero F holds S1 . x,y = (omf F) . x,((revf F) . y) ) & ( for x being Element of the carrier 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 the carrier 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 the carrier of F
for y being Element of NonZero F holds S2 . x,y = (omf F) . x,((revf F) . y) ; :: thesis: S1 = S2

now

let p be set ; :: thesis: ( p in [:the carrier of F,(NonZero F):] implies S1 . p = S2 . p )
assume p in [:the carrier of F,(NonZero F):] ; :: thesis: S1 . p = S2 . p
then consider x, y being set such that
A4: ( x in the carrier of F & y in NonZero F & p = [x,y] ) by ZFMISC_1:def 2;
S1 . x,y = (omf F) . x,((revf F) . y) by A2, A4
.= S2 . x,y by A3, A4 ;
hence S1 . p = S2 . p by A4; :: thesis: verum

end;

hence S1 = S2 by FUNCT_2:18; :: thesis: verum