let f1, f2 be nonnegative Function of X1,ExtREAL; :: thesis: ( ( for x being Element of X1 holds f1 . x = M2 . (Measurable-X-section (E,x)) ) & ( for V being Element of S1 holds f1 is V -measurable ) & ( for x being Element of X1 holds f2 . x = M2 . (Measurable-X-section (E,x)) ) & ( for V being Element of S1 holds f2 is V -measurable ) implies f1 = f2 )
assume that
A1: ( ( for x being Element of X1 holds f1 . x = M2 . (Measurable-X-section (E,x)) ) & ( for V being Element of S1 holds f1 is V -measurable ) ) and
A2: ( ( for x being Element of X1 holds f2 . x = M2 . (Measurable-X-section (E,x)) ) & ( for V being Element of S1 holds f2 is V -measurable ) ) ; :: thesis: f1 = f2

now :: thesis: for x being Element of X1 holds f1 . x = f2 . x

let x be Element of X1; :: thesis: f1 . x = f2 . x
f1 . x = M2 . (Measurable-X-section (E,x)) by A1;
hence f1 . x = f2 . x by A2; :: thesis: verum

end;

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