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
now :: thesis: for y being Element of S2 holds N1 . y = N2 . y
let 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;
hence N1 = N2 by FUNCT_2:63; :: thesis: verum