defpred S₁[ Element of measurable_rectangles (S1,S2), Element of ExtREAL ] means ex A being Element of S1 ex B being Element of S2 st
( $1 = [:A,B:] & $2 = (m1 . A) * (m2 . B) );
A1: for C being Element of measurable_rectangles (S1,S2) ex y being Element of ExtREAL st S₁[C,y]

proof

let C be Element of measurable_rectangles (S1,S2); :: thesis: ex y being Element of ExtREAL st S₁[C,y]
C in { [:A,B:] where A is Element of S1, B is Element of S2 : verum } ;
then consider A being Element of S1, B being Element of S2 such that
A2: C = [:A,B:] ;
set y = (m1 . A) * (m2 . B);
take (m1 . A) * (m2 . B) ; :: thesis: S₁[C,(m1 . A) * (m2 . B)]
thus S₁[C,(m1 . A) * (m2 . B)] by A2; :: thesis: verum

end;

consider IT being Function of (measurable_rectangles (S1,S2)),ExtREAL such that
A3: for C being Element of measurable_rectangles (S1,S2) holds S₁[C,IT . C] from FUNCT_2:sch 3(A1);

A6: now :: thesis: for x being object st x in dom IT holds
0 <= IT . x

let x be object ; :: thesis: ( x in dom IT implies 0 <= IT . x )
assume x in dom IT ; :: thesis: 0 <= IT . x
then reconsider C = x as Element of measurable_rectangles (S1,S2) ;
consider A being Element of S1, B being Element of S2 such that
A5: ( C = [:A,B:] & IT . C = (m1 . A) * (m2 . B) ) by A3;
( 0 <= m1 . A & 0 <= m2 . B ) by SUPINF_2:51;
hence 0 <= IT . x by A5; :: thesis: verum

end;

reconsider Z = {} as Element of measurable_rectangles (S1,S2) by SETFAM_1:def 8;
consider A0 being Element of S1, B0 being Element of S2 such that
A7: ( Z = [:A0,B0:] & IT . Z = (m1 . A0) * (m2 . B0) ) by A3;
( A0 = {} or B0 = {} ) by A7;
then ( m1 . A0 = 0 or m2 . B0 = 0 ) by VALUED_0:def 19;
then IT . {} = 0 by A7;
then reconsider IT = IT as zeroed nonnegative Function of (measurable_rectangles (S1,S2)),ExtREAL by A6, SUPINF_2:52, VALUED_0:def 19;
take IT ; :: thesis: for C being Element of measurable_rectangles (S1,S2) ex A being Element of S1 ex B being Element of S2 st
( C = [:A,B:] & IT . C = (m1 . A) * (m2 . B) )
thus for C being Element of measurable_rectangles (S1,S2) ex A being Element of S1 ex B being Element of S2 st
( C = [:A,B:] & IT . C = (m1 . A) * (m2 . B) ) by A3; :: thesis: verum