let x, y be object ; :: thesis: for X being set
for f being Function holds (Ext (f,x,y)) | X = Ext ((f | X),x,y)
let X be set ; :: thesis: for f being Function holds (Ext (f,x,y)) | X = Ext ((f | X),x,y)
let f be Function; :: thesis: (Ext (f,x,y)) | X = Ext ((f | X),x,y)
thus (Ext (f,x,y)) | X = (Ext (f,x,y)) * (id X) by RELAT_1:65
.= Ext ((f * (id X)),x,y) by Th25
.= Ext ((f | X),x,y) by RELAT_1:65 ; :: thesis: verum