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_{1}[ 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_{1}[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_{1}[x] )
; :: thesis: F1 = F2

thus F1 = F2 from XFAMILY:sch 2(A5, A6); :: thesis: verum

( 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

assume A5: for x being set holds

( x in F1 iff S

( ( 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

thus F1 = F2 from XFAMILY:sch 2(A5, A6); :: thesis: verum