let F1, F2 be Subset of (product F); :: thesis: ( ( for x being set holds
( x in F1 iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) ) & ( for x being set holds
( x in F2 iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) ) implies F1 = F2 )
defpred S₁[ set ] means ex g being Element of (F . i) st $1 = (1_ (product F)) +* (i,g);
assume A7: for x being set holds
( x in F1 iff S₁[x] ) ; :: thesis: ( ex x being set st
( ( x in F2 implies ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) implies ( ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) & not x in F2 ) ) or F1 = F2 )
assume A8: for x being set holds
( x in F2 iff S₁[x] ) ; :: thesis: F1 = F2
thus F1 = F2 from XBOOLE_0:sch 2(A7, A8); :: thesis: verum