let N1, N2 be Measure of S2; :: thesis: ( ( for y being Element of S2 holds N1 . y = M . (F " y) ) & ( for y being Element of S2 holds N2 . y = M . (F " y) ) implies N1 = N2 )

assume A1: for y being Element of S2 holds N1 . y = M . (F " y) ; :: thesis: ( ex y being Element of S2 st not N2 . y = M . (F " y) or N1 = N2 )

assume A2: for y being Element of S2 holds N2 . y = M . (F " y) ; :: thesis: N1 = N2

assume A1: for y being Element of S2 holds N1 . y = M . (F " y) ; :: thesis: ( ex y being Element of S2 st not N2 . y = M . (F " y) or N1 = N2 )

assume A2: for y being Element of S2 holds N2 . y = M . (F " y) ; :: thesis: N1 = N2

now :: thesis: for y being Element of S2 holds N1 . y = N2 . y

hence
N1 = N2
by FUNCT_2:63; :: thesis: verumlet y be Element of S2; :: thesis: N1 . y = N2 . y

thus N1 . y = M . (F " y) by A1

.= N2 . y by A2 ; :: thesis: verum

end;thus N1 . y = M . (F " y) by A1

.= N2 . y by A2 ; :: thesis: verum