let A be FinSequence-membered set ; :: thesis: {} ^^ A c= A
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {} ^^ A or x in A )
assume x in {} ^^ A ; :: thesis: x in A
then ex p being Element of {} ex q being Element of A st
( x = p ^ q & p in {} & q in A ) ;
hence x in A ; :: thesis: verum