let X be non empty set ; :: thesis: for t being object
for f being Function st dom f = X holds
{ w where w is Element of X : f . w = t } = Coim (f,t)

let t be object ; :: thesis: for f being Function st dom f = X holds
{ w where w is Element of X : f . w = t } = Coim (f,t)

let f be Function; :: thesis: ( dom f = X implies { w where w is Element of X : f . w = t } = Coim (f,t) )
assume AA: dom f = X ; :: thesis: { w where w is Element of X : f . w = t } = Coim (f,t)
set A = { w where w is Element of X : f . w = t } ;
A0: t in {t} by TARSKI:def 1;
thus { w where w is Element of X : f . w = t } c= Coim (f,t) :: according to XBOOLE_0:def 10 :: thesis: Coim (f,t) c= { w where w is Element of X : f . w = t }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { w where w is Element of X : f . w = t } or x in Coim (f,t) )
assume x in { w where w is Element of X : f . w = t } ; :: thesis: x in Coim (f,t)
then ex w being Element of X st
( x = w & f . w = t ) ;
then [x,t] in f by ;
hence x in Coim (f,t) by ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Coim (f,t) or x in { w where w is Element of X : f . w = t } )
assume x in Coim (f,t) ; :: thesis: x in { w where w is Element of X : f . w = t }
then consider y being object such that
A1: [x,y] in f and
A2: y in {t} by RELAT_1:def 14;
A4: y = t by ;
A3: x in dom f by ;
f . x = t by ;
hence x in { w where w is Element of X : f . w = t } by AA, A3; :: thesis: verum