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