consider s being Element of S * ;
consider T being Subset-Family of (S * ) such that
A1: for A being Subset of (S * ) holds
( A in T iff S₁[A] ) from SUBSET_1:sch 3();
Finseq-EQclass s in T by A1;
hence ex b₁ being non empty Subset-Family of (S * ) st
for A being Subset of (S * ) holds
( A in b₁ iff ex s being FinSequence of S st A = Finseq-EQclass s ) by A1; :: thesis: verum