thus ( p = r implies for a being FinSequence holds
( a in p iff a in r ) ) ; :: thesis: ( ( for a being FinSequence holds
( a in p iff a in r ) ) implies p = r )
assume for a being FinSequence holds
( a in p iff a in r ) ; :: thesis: p = r
then for x being object holds
( x in p iff x in r ) ;
hence p = r by TARSKI:2; :: thesis: verum