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 )
thus ( ( for a being FinSequence holds
( a in p iff a in r ) ) implies p = r ) :: thesis: verum

proof

assume for a being FinSequence holds
( a in p iff a in r ) ; :: thesis: p = r
then for x being set holds
( x in p iff x in r ) ;
hence p = r by TARSKI:1; :: thesis: verum

end;