let F1, F2 be zeroed nonnegative Function of (measurable_rectangles (S1,S2)),ExtREAL; :: 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:] & F1 . C = (m1 . A) * (m2 . B) ) ) & ( 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:] & F2 . C = (m1 . A) * (m2 . B) ) ) implies F1 = F2 )
assume that
A1: 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:] & F1 . C = (m1 . A) * (m2 . B) ) and
A2: 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:] & F2 . C = (m1 . A) * (m2 . B) ) ; :: thesis: F1 = F2

now :: thesis: for C being Element of measurable_rectangles (S1,S2) holds F1 . C = F2 . C

let C be Element of measurable_rectangles (S1,S2); :: thesis: F1 . b₁ = F2 . b₁
consider A1 being Element of S1, B1 being Element of S2 such that
A3: ( C = [:A1,B1:] & F1 . C = (m1 . A1) * (m2 . B1) ) by A1;
consider A2 being Element of S1, B2 being Element of S2 such that
A4: ( C = [:A2,B2:] & F2 . C = (m1 . A2) * (m2 . B2) ) by A2;

per cases ( A1 = {} or B1 = {} or ( A1 <> {} & B1 <> {} ) ) ;

suppose A5: ( A1 = {} or B1 = {} ) ; :: thesis: F1 . b₁ = F2 . b₁

then ( A2 = {} or B2 = {} ) by A3, A4;
then ( ( m1 . A1 = 0 or m2 . B1 = 0 ) & ( m1 . A2 = 0 or m2 . B2 = 0 ) ) by A5, VALUED_0:def 19;
hence F1 . C = F2 . C by A3, A4; :: thesis: verum

end;

suppose ( A1 <> {} & B1 <> {} ) ; :: thesis: F1 . b₁ = F2 . b₁

then ( A1 = A2 & B1 = B2 ) by A3, A4, ZFMISC_1:110;
hence F1 . C = F2 . C by A3, A4; :: thesis: verum

end;

end;

end;

hence F1 = F2 by FUNCT_2:def 8; :: thesis: verum