let f, g be Function; :: thesis: for A being set
for F being Function
for x being set 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 set st f | A = g | A holds
(F [;] x,f) | A = (F [;] x,g) | A
let F be Function; :: thesis: for x being set st f | A = g | A holds
(F [;] x,f) | A = (F [;] x,g) | A
let x be set ; :: 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:90
.= (dom g) /\ A by A1, RELAT_1:90 ;
then A2: ((dom f) --> x) | A = ((dom g) /\ A) --> x by Th18
.= ((dom g) --> x) | A by Th18 ;
thus (F [;] x,f) | A = (F .: ((dom f) --> x),f) | A
.= (F .: ((dom f) --> x),g) | A by A1, Th30
.= (F .: ((dom g) --> x),g) | A by A2, Th29
.= (F [;] x,g) | A ; :: thesis: verum