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

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