let A be set ; :: thesis: for C being non empty set
for B being Subset of A
for f, g being Function of A,C st ( for x being Element of A st x in B holds
g . x = f . x ) holds
f +* (g | B) = f
let C be non empty set ; :: thesis: for B being Subset of A
for f, g being Function of A,C st ( for x being Element of A st x in B holds
g . x = f . x ) holds
f +* (g | B) = f
let B be Subset of A; :: thesis: for f, g being Function of A,C st ( for x being Element of A st x in B holds
g . x = f . x ) holds
f +* (g | B) = f
let f, g be Function of A,C; :: thesis: ( ( for x being Element of A st x in B holds
g . x = f . x ) implies f +* (g | B) = f )
assume for x being Element of A st x in B holds
g . x = f . x ; :: thesis: f +* (g | B) = f
then g | B = f | B by Th2;
hence f +* (g | B) = f by Th5, RELAT_1:59; :: thesis: verum