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:49
.= f . x by A1, A2, FUNCT_1:49 ;
:: thesis: verum
end;
reconsider f9 = f | B, g9 = g | B as Function of B,C by FUNCT_2:32;
assume A3: for x being Element of A st x in B holds
g . x = f . x ; :: thesis: f | B = g | B
A4: now :: thesis: for x being object st x in B holds
f9 . x = g9 . x
let x be object ; :: thesis: ( x in B implies f9 . x = g9 . x )
assume A5: x in B ; :: thesis: f9 . x = g9 . x
hence f9 . x = f . x by FUNCT_1:49
.= g . x by A3, A5
.= g9 . x by A5, FUNCT_1:49 ;
:: thesis: verum
end;
thus f | B = f9 | B
.= g9 | B by A4, FUNCT_2:12
.= g | B ; :: thesis: verum