let F1, F2 be zeroed V161() Function of (measurable_rectangles (S1,S2)),ExtREAL; ( ( 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) )
; F1 = F2
hence
F1 = F2
by FUNCT_2:def 8; verum