let f1, f2 be nonnegative Function of X2,ExtREAL; :: thesis: ( ( for y being Element of X2 holds f1 . y = M1 . (Measurable-Y-section (E,y)) ) & ( for V being Element of S2 holds f1 is V -measurable ) & ( for y being Element of X2 holds f2 . y = M1 . (Measurable-Y-section (E,y)) ) & ( for V being Element of S2 holds f2 is V -measurable ) implies f1 = f2 )
assume that
A1: ( ( for y being Element of X2 holds f1 . y = M1 . (Measurable-Y-section (E,y)) ) & ( for V being Element of S2 holds f1 is V -measurable ) ) and
A2: ( ( for y being Element of X2 holds f2 . y = M1 . (Measurable-Y-section (E,y)) ) & ( for V being Element of S2 holds f2 is V -measurable ) ) ; :: thesis: f1 = f2

now :: thesis: for y being Element of X2 holds f1 . y = f2 . y

let y be Element of X2; :: thesis: f1 . y = f2 . y
f1 . y = M1 . (Measurable-Y-section (E,y)) by A1;
hence f1 . y = f2 . y by A2; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:63; :: thesis: verum