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

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