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