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 holds
( f | B = g | B iff for x being Element of A st x in B holds
g . x = f . x )
let C be non empty set ; :: thesis: for B being Subset of A
for f, g being Function of A,C holds
( f | B = g | B iff for x being Element of A st x in B holds
g . x = f . x )
let B be Subset of A; :: thesis: for f, g being Function of A,C holds
( f | B = g | B iff for x being Element of A st x in B holds
g . x = f . x )
let f, g be Function of A,C; :: thesis: ( f | B = g | B iff for x being Element of A st x in B holds
g . x = f . x )
thus ( f | B = g | B implies for x being Element of A st x in B holds
g . x = f . x ) :: thesis: ( ( for x being Element of A st x in B holds
g . x = f . x ) implies f | B = g | B )

proof

assume A1: f | B = g | B ; :: thesis: for x being Element of A st x in B holds
g . x = f . x
let x be Element of A; :: thesis: ( x in B implies g . x = f . x )
assume A2: x in B ; :: thesis: g . x = f . x
hence g . x = (g | B) . x by FUNCT_1:72
.= f . x by A1, A2, FUNCT_1:72 ;
:: thesis: verum

end;

assume A3: for x being Element of A st x in B holds
g . x = f . x ; :: thesis: f | B = g | B
reconsider f' = f | B, g' = g | B as Function of B,C by FUNCT_2:38;

A4: now

let x be set ; :: thesis: ( x in B implies f' . x = g' . x )
assume A5: x in B ; :: thesis: f' . x = g' . x
hence f' . x = f . x by FUNCT_1:72
.= g . x by A3, A5
.= g' . x by A5, FUNCT_1:72 ;
:: thesis: verum

end;

thus f | B = f' | B by RELAT_1:101
.= g' | B by A4, FUNCT_2:18
.= g | B by RELAT_1:101 ; :: thesis: verum