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

for F being Function

for x being object st f | A = g | A holds

(F [;] (x,f)) | A = (F [;] (x,g)) | A

let A be set ; :: thesis: for F being Function

for x being object st f | A = g | A holds

(F [;] (x,f)) | A = (F [;] (x,g)) | A

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

(F [;] (x,f)) | A = (F [;] (x,g)) | A

let x be object ; :: thesis: ( f | A = g | A implies (F [;] (x,f)) | A = (F [;] (x,g)) | A )

assume A1: f | A = g | A ; :: thesis: (F [;] (x,f)) | A = (F [;] (x,g)) | A

(dom f) /\ A = dom (f | A) by RELAT_1:61

.= (dom g) /\ A by A1, RELAT_1:61 ;

then A2: ((dom f) --> x) | A = ((dom g) /\ A) --> x by Th12

.= ((dom g) --> x) | A by Th12 ;

thus (F [;] (x,f)) | A = (F .: (((dom f) --> x),f)) | A

.= (F .: (((dom f) --> x),g)) | A by A1, Th24

.= (F .: (((dom g) --> x),g)) | A by A2, Th23

.= (F [;] (x,g)) | A ; :: thesis: verum

for F being Function

for x being object st f | A = g | A holds

(F [;] (x,f)) | A = (F [;] (x,g)) | A

let A be set ; :: thesis: for F being Function

for x being object st f | A = g | A holds

(F [;] (x,f)) | A = (F [;] (x,g)) | A

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

(F [;] (x,f)) | A = (F [;] (x,g)) | A

let x be object ; :: thesis: ( f | A = g | A implies (F [;] (x,f)) | A = (F [;] (x,g)) | A )

assume A1: f | A = g | A ; :: thesis: (F [;] (x,f)) | A = (F [;] (x,g)) | A

(dom f) /\ A = dom (f | A) by RELAT_1:61

.= (dom g) /\ A by A1, RELAT_1:61 ;

then A2: ((dom f) --> x) | A = ((dom g) /\ A) --> x by Th12

.= ((dom g) --> x) | A by Th12 ;

thus (F [;] (x,f)) | A = (F .: (((dom f) --> x),f)) | A

.= (F .: (((dom f) --> x),g)) | A by A1, Th24

.= (F .: (((dom g) --> x),g)) | A by A2, Th23

.= (F [;] (x,g)) | A ; :: thesis: verum