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 A5: 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 A6: for x being set holds
( x in F2 iff S₁[x] ) ; :: thesis: F1 = F2
thus F1 = F2 from XFAMILY:sch 2(A5, A6); :: thesis: verum