let S1, S2 be Function of [: the carrier of F,(NonZero F):], the carrier of F; :: thesis: ( ( 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)) ; :: thesis: S1 = S2

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)) ; :: thesis: S1 = S2

now :: thesis: for p being object st p in [: the carrier of F,(NonZero F):] holds

S1 . p = S2 . p

hence
S1 = S2
by FUNCT_2:12; :: thesis: verumS1 . p = S2 . p

let p be object ; :: 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 object such that

A4: ( x in the carrier of F & y in NonZero F ) and

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

end;assume p in [: the carrier of F,(NonZero F):] ; :: thesis: S1 . p = S2 . p

then consider x, y being object such that

A4: ( x in the carrier of F & y in NonZero F ) and

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