let F1, F2 be Subset-Family of (S *); :: thesis: ( ( for A being Subset of (S *) holds

( A in F1 iff ex s being FinSequence of S st A = Finseq-EQclass s ) ) & ( for A being Subset of (S *) holds

( A in F2 iff ex s being FinSequence of S st A = Finseq-EQclass s ) ) implies F1 = F2 )

assume that

A1: for A being Subset of (S *) holds

( A in F1 iff S_{1}[A] )
and

A2: for A being Subset of (S *) holds

( A in F2 iff S_{1}[A] )
; :: thesis: F1 = F2

thus F1 = F2 from SUBSET_1:sch 4(A1, A2); :: thesis: verum

( A in F1 iff ex s being FinSequence of S st A = Finseq-EQclass s ) ) & ( for A being Subset of (S *) holds

( A in F2 iff ex s being FinSequence of S st A = Finseq-EQclass s ) ) implies F1 = F2 )

assume that

A1: for A being Subset of (S *) holds

( A in F1 iff S

A2: for A being Subset of (S *) holds

( A in F2 iff S

thus F1 = F2 from SUBSET_1:sch 4(A1, A2); :: thesis: verum