let A be set ; :: thesis: for C being non empty set
for f, g being Function of A,C
for B being Element of Fin A 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 f, g being Function of A,C
for B being Element of Fin A 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 B being Element of Fin A st ( for x being Element of A st x in B holds
g . x = f . x ) holds
f +* (g | B) = f
let B be Element of Fin A; :: thesis: ( ( for x being Element of A st x in B holds
g . x = f . x ) implies f +* (g | B) = f )
reconsider C = B as Subset of A by FINSUB_1:16;
( ( for x being Element of A st x in C holds
g . x = f . x ) implies f +* (g | C) = f ) by Th7;
hence ( ( for x being Element of A st x in B holds
g . x = f . x ) implies f +* (g | B) = f ) ; :: thesis: verum