consider IT being Function of X2,ExtREAL such that
A2: ( ( for y being Element of X2 holds IT . y = M1 . (Measurable-Y-section (E,y)) ) & ( for V being Element of S2 holds IT is V -measurable ) ) by A1, Th91;

now :: thesis: for y being Element of X2 holds 0. <= IT . y

let y be Element of X2; :: thesis: 0. <= IT . y
IT . y = M1 . (Measurable-Y-section (E,y)) by A2;
hence 0. <= IT . y by SUPINF_2:51; :: thesis: verum

end;

then reconsider IT = IT as nonnegative Function of X2,ExtREAL by SUPINF_2:39;
take IT ; :: thesis: ( ( for y being Element of X2 holds IT . y = M1 . (Measurable-Y-section (E,y)) ) & ( for V being Element of S2 holds IT is V -measurable ) )
thus ( ( for y being Element of X2 holds IT . y = M1 . (Measurable-Y-section (E,y)) ) & ( for V being Element of S2 holds IT is V -measurable ) ) by A2; :: thesis: verum