let f be Function; :: thesis: for A being set
for F being Function
for x being object holds (F [;] (x,f)) * (id A) = F [;] (x,(f | A))
let A be set ; :: thesis: for F being Function
for x being object holds (F [;] (x,f)) * (id A) = F [;] (x,(f | A))
let F be Function; :: thesis: for x being object holds (F [;] (x,f)) * (id A) = F [;] (x,(f | A))
let x be object ; :: thesis: (F [;] (x,f)) * (id A) = F [;] (x,(f | A))
thus (F [;] (x,f)) * (id A) = F [;] (x,(f * (id A))) by Th34
.= F [;] (x,(f | A)) by RELAT_1:65 ; :: thesis: verum