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 }

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

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 Coim (f,t) or x in { w where w is Element of X : f . w = t } )
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;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

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