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