let f, g, h be Function; :: thesis: for A being set

for F being Function st f | A = g | A holds

(F .: (f,h)) | A = (F .: (g,h)) | A

let A be set ; :: thesis: for F being Function st f | A = g | A holds

(F .: (f,h)) | A = (F .: (g,h)) | A

let F be Function; :: thesis: ( f | A = g | A implies (F .: (f,h)) | A = (F .: (g,h)) | A )

assume A1: f | A = g | A ; :: thesis: (F .: (f,h)) | A = (F .: (g,h)) | A

thus (F .: (f,h)) | A = F * (<:f,h:> | A) by RELAT_1:83

.= F * <:(f | A),h:> by Th5

.= F * (<:g,h:> | A) by A1, Th5

.= (F .: (g,h)) | A by RELAT_1:83 ; :: thesis: verum

for F being Function st f | A = g | A holds

(F .: (f,h)) | A = (F .: (g,h)) | A

let A be set ; :: thesis: for F being Function st f | A = g | A holds

(F .: (f,h)) | A = (F .: (g,h)) | A

let F be Function; :: thesis: ( f | A = g | A implies (F .: (f,h)) | A = (F .: (g,h)) | A )

assume A1: f | A = g | A ; :: thesis: (F .: (f,h)) | A = (F .: (g,h)) | A

thus (F .: (f,h)) | A = F * (<:f,h:> | A) by RELAT_1:83

.= F * <:(f | A),h:> by Th5

.= F * (<:g,h:> | A) by A1, Th5

.= (F .: (g,h)) | A by RELAT_1:83 ; :: thesis: verum