let Y be set ; for f being Function holds Y |` f = f | (f " Y)
let f be Function; Y |` f = f | (f " Y)
A1:
Y |` f c= f | (f " Y)
by RELAT_1:188;
f | (f " Y) c= Y |` f
proof
let x,
y be
object ;
RELAT_1:def 3 ( not [x,y] in f | (f " Y) or [x,y] in Y |` f )
assume A2:
[x,y] in f | (f " Y)
;
[x,y] in Y |` f
then A3:
x in f " Y
by RELAT_1:def 11;
A4:
[x,y] in f
by A2, RELAT_1:def 11;
f . x in Y
by A3, Def7;
then
y in Y
by A4, Th1;
hence
[x,y] in Y |` f
by A4, RELAT_1:def 12;
verum
end;
hence
Y |` f = f | (f " Y)
by A1; verum