F . (n,E) in sigma (measurable_rectangles (S1,S2)) ;
hence F . (n,E) is Element of sigma (measurable_rectangles (S1,S2)) ; :: thesis: verum