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 AA, FUNCT_1:1;
hence x in Coim (f,t) by A0, RELAT_1:def 14; :: 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 A2, TARSKI:def 1;
A3: x in dom f by A1, XTUPLE_0:def 12;
f . x = t by A1, A4, FUNCT_1:1;
hence x in { w where w is Element of X : f . w = t } by AA, A3; :: thesis: verum