let I1, I2 be Function of X1,ExtREAL; :: thesis: ( ( for x being Element of X1 holds I1 . x = Integral (M2,(ProjPMap1 (f,x))) ) & ( for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x))) ) implies I1 = I2 )
assume that
A1: for x being Element of X1 holds I1 . x = Integral (M2,(ProjPMap1 (f,x))) and
A2: for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x))) ; :: thesis: I1 = I2

now :: thesis: for x being Element of X1 holds I1 . x = I2 . x

let x be Element of X1; :: thesis: I1 . x = I2 . x
I1 . x = Integral (M2,(ProjPMap1 (f,x))) by A1;
hence I1 . x = I2 . x by A2; :: thesis: verum

end;

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