let f, g, h be Function; :: thesis: for A being set
for F being Function st f | A = g | A holds
(F .: h,f) | A = (F .: h,g) | A
let A be set ; :: thesis: for F being Function st f | A = g | A holds
(F .: h,f) | A = (F .: h,g) | A
let F be Function; :: thesis: ( f | A = g | A implies (F .: h,f) | A = (F .: h,g) | A )
assume A1: f | A = g | A ; :: thesis: (F .: h,f) | A = (F .: h,g) | A
thus (F .: h,f) | A = F * (<:h,f:> | A) by RELAT_1:112
.= F * <:h,(f | A):> by Th11
.= F * (<:h,g:> | A) by A1, Th11
.= (F .: h,g) | A by RELAT_1:112 ; :: thesis: verum