let A, B be set ; :: thesis: for F, G being Function of A,B
for X being set st F | X = G | X holds
for x being Element of A st x in X holds
F . x = G . x
let F, G be Function of A,B; :: thesis: for X being set st F | X = G | X holds
for x being Element of A st x in X holds
F . x = G . x
let X be set ; :: thesis: ( F | X = G | X implies for x being Element of A st x in X holds
F . x = G . x )
assume A1: F | X = G | X ; :: thesis: for x being Element of A st x in X holds
F . x = G . x
let x be Element of A; :: thesis: ( x in X implies F . x = G . x )
assume A2: x in X ; :: thesis: F . x = G . x
hence F . x = (G | X) . x by A1, FUNCT_1:49
.= G . x by A2, FUNCT_1:49 ;
:: thesis: verum