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