reconsider X = {} as FinSequence-membered set ;
thus f ^^ E c= E :: according to XBOOLE_0:def 10 :: thesis: E c= f ^^ E
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in f ^^ E or a in E )
assume a in f ^^ E ; :: thesis: a in E
then ex p being Element of X st
( a = f ^ p & p in X ) ;
hence a in E ; :: thesis: verum
end;
thus E c= f ^^ E ; :: thesis: verum