let I1, I2 be Function of X2,ExtREAL; :: thesis: ( ( for y being Element of X2 holds I1 . y = Integral (M1,(ProjPMap2 (f,y))) ) & ( for y being Element of X2 holds I2 . y = Integral (M1,(ProjPMap2 (f,y))) ) implies I1 = I2 )
assume that
A1: for y being Element of X2 holds I1 . y = Integral (M1,(ProjPMap2 (f,y))) and
A2: for y being Element of X2 holds I2 . y = Integral (M1,(ProjPMap2 (f,y))) ; :: thesis: I1 = I2

now :: thesis: for y being Element of X2 holds I1 . y = I2 . y

let y be Element of X2; :: thesis: I1 . y = I2 . y
I1 . y = Integral (M1,(ProjPMap2 (f,y))) by A1;
hence I1 . y = I2 . y by A2; :: thesis: verum

end;

hence I1 = I2 by FUNCT_2:63; :: thesis: verum