consider IT being Function of X1,ExtREAL such that
A2: ( ( for x being Element of X1 holds IT . x = M2 . (Measurable-X-section (E,x)) ) & ( for V being Element of S1 holds IT is V -measurable ) ) by A1, Th90;

now :: thesis: for x being Element of X1 holds 0. <= IT . x

let x be Element of X1; :: thesis: 0. <= IT . x
IT . x = M2 . (Measurable-X-section (E,x)) by A2;
hence 0. <= IT . x by SUPINF_2:51; :: thesis: verum

end;

then reconsider IT = IT as nonnegative Function of X1,ExtREAL by SUPINF_2:39;
take IT ; :: thesis: ( ( for x being Element of X1 holds IT . x = M2 . (Measurable-X-section (E,x)) ) & ( for V being Element of S1 holds IT is V -measurable ) )
thus ( ( for x being Element of X1 holds IT . x = M2 . (Measurable-X-section (E,x)) ) & ( for V being Element of S1 holds IT is V -measurable ) ) by A2; :: thesis: verum