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